I admire the elegancy of your code which makes the changes to add new data types minimum. There is one question I want to ask: Does this technique extend to polymophic types?
Let's say we have the following type: > data D a = C | D a Is it possible to index the type D a? Or there is some fundmental limitations which make it not achievable by Haskell type classes? -W-M- @ @ | \_/ On Thu, 31 Jul 2003 [EMAIL PROTECTED] wrote: > > This message describes functions safeCast and sAFECoerce implemented > in Haskell98 with common, pure extensions. The functions can be used > to 'escape' from or to existential quantification and to make > existentially-quantified datatypes far easier to deal with. Unlike > Dynamic, the present approach is pure, avoids unsafeCoerce and > unsafePerformIO, and permits arbitrary multiple user-defined typeheaps > (finite maps from types to integers and values). > > An earlier message [1] introduced finite type maps for > purely-functional conversion of monomorphic types to unique > integers. The solution specifically did not rely on Dynamic and > therefore is free from unsafePerformIO. This message shows that the > type maps can be used for a safe cast, in particular, for laundering > existential types. The code in this message does NOT use > unsafePerformIO or unsafeCoerce. To implement safe casts, we define a > function sAFECoerce -- which works just like its impure > counterpart. However the former is pure and safe. sAFECoerce is a > library function expressed in Haskell with common extension. The > safety of sAFECoerce is guaranteed by the typechecker itself. > > This whole message is self-contained, and can be loaded as it is in > GHCi, given the flags > -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances > > This message was inspired by Amr Sabry's problem on existentials. In > fact, it answers an unstated question in Amr Sabry's original message. > > > It has been observed on this list that existentially-quantified > datatypes are not easy to deal with [2]. For example, suppose we have > a value of a type > > > data EV = forall a. (TypeRep a TI)=> EV a > > (please disregard the second argument of TypeRep for a moment). > > The constructor EV wraps a value. Suppose we can guess that the > wrapped value is actually a boolean. Even if our guess is correct, we > *cannot* pass that value to any function of booleans: > > *> *Main> case (EV False) of (EV x) -> not x > *> > *> <interactive>:1: > *> Inferred type is less polymorphic than expected > *> Quantified type variable `a' is unified with `Bool' > *> When checking an existential match that binds > *> x :: a > *> and whose type is EV -> Bool > *> In a case alternative: (EV x) -> not x > > A quantified type variable cannot be unified with any regular type -- > or with another quantified type variable. Values of existentially > quantified types cannot be passed to monomorphic functions, or to > constrained polymorphic functions (unless all their constrains have > been mentioned in the declaration of the existential). That limitation > guarantees safety -- on the other hand, it significantly limits the > convenience of existential datatypes [2]. > > To overcome the limitation, it _seemed_ that we had to sacrifice > purity. If we are positive that a particular existentially quantified > value has a specific type (e.g., Bool), we can use unsafeCoerce to > cast the value into the type Bool [3]. This approach is one of the > foundations of the Dynamic library. The other foundation is an ability > to represent a type as a unique run-time value, provided by the > methods of the class like TypeRep. Given an existentially quantified > value and a value of the desired type, Dynamic compares type > representations of the two values. If they are the same, we can > confidently use unsafeCoerce to cast the former into the type of the > latter. > > This works, yet leaves the feeling of dissatisfaction. For one thing, > we had to resort to an impure feature. More importantly, we placed our > trust in something like TypeRep and its members, that they give an > accurate and unique representation of types. But what if they lie to > us, due to a subtle bug in their implementation? What if they give the > same representation for two different types? unsafeCoerce will do its > dirty work nevertheless. Using the result would lead to grave > consequences, however. > > This message describes sAFECoerce and the corresponding safe cast. > Both functions convert the values of one type into the target type. > One or both of these types may be existentially quantified. When the > source and the target types are the same, both functions act as the > identity function. The safe cast checks that the type representations > of the source and the target types are the same. If they are, it > invokes sAFECoerce. Otherwise, we monadically fail. The function > sAFECoerce does the conversion without any type checking. It always > returns the value of the target type. If the source type was the same > as the target type, the return value has the same "bit pattern" as the > argument. If the types differ, the return value is just some default > value of the right type. The user can specify the default value as he > wishes. > > Therefore, we can now write > > *> *Main> case (EV False) of (EV x) -> not $ sAFECoerce x > *> True > > We can also try > > *> *Main> case (EV 'a') of (EV x) -> not $ sAFECoerce x > *> *** Exception: Prelude.undefined > > The default value was 'undefined'. > > The function safeCast is actually trivial > > > safeCast::(Monad m, TypeRep b TI, TypeRep a TI) => a -> m b > > safeCast a :: m b > > = if tr_index a (undefined::TI) == tr_index (undefined::b) (undefined::TI) > > then return $ sAFECoerce a > > else fail "miscast" > > *> *Main> case (EV False) of (EV x) -> (safeCast x)::Maybe Bool > *> Just False > *> *Main> case (EV False) of (EV x) -> (safeCast x)::Maybe Int > *> Nothing > > The above examples cast the value of an existentially quantified type > into a regular type. As we shall see at the end, we can just as well > cast _into_ an existentially quantified type. > > Some of the code in this message is similar to the code posted here > earlier. However, there are many small and subtle changes. It seemed > more convenient to include all the code, to make this message > self-contained. > > > We start with the polymorphic list as a base data structure, as > before: > > > data Nil t r = Nil > > data Cons t r = Cons t r > > > > class PList ntype vtype cdrtype where > > cdr:: ntype vtype cdrtype -> cdrtype > > empty:: ntype vtype cdrtype -> Bool > > value:: ntype vtype cdrtype -> vtype > > > > instance PList Nil vtype cdrtype where > > empty = const True > > > > instance (PList n v r) => PList Cons v' (n v r) where > > empty = const False > > value (Cons v r) = v > > cdr (Cons v r) = r > > > We use the polymorphic list to define a finite type map. The map in > this message has two additional operations: fetch and alter. > > > class TypeSeq t s where > > type_index:: t -> s -> Int > > fetch:: t -> s -> t > > alter:: t -> s -> s > > > > instance (PList Cons t r) => TypeSeq t (Cons t r) where > > type_index _ _ = 0 > > fetch _ (Cons v _) = v > > alter newv (Cons v r) = Cons newv r > > > > instance (PList Cons t' r', TypeSeq t r') => TypeSeq t (Cons t' r') where > > type_index v s = 1 + (type_index v $ cdr s) > > fetch v s = fetch v $ cdr s > > alter newv (Cons v' r') = Cons v' $ alter newv r' > > TypeSeq is an associative map between types, values, and integers. > The operation type_index takes a value and a typemap and returns the > index of the type of the value in the map. The operation alter takes a > value and a typemap and returns a new typemap which stores the given > value. The value can be retrieved either by its index -- or by its > type. Here we need only the latter: the operation fetch. > > We can build the initial typemap > > > init_typeseq = Cons (undefined::Char) $ > > Cons (undefined::Int) $ > > Cons (undefined::Bool) $ > > Cons (undefined::String) $ > > Cons (undefined::Maybe Char) $ > > Nil > > We also need the type of init_typeseq, to be used in a type-expression > context. Alas, there does not seem to be an easy way to take a type of > a variable in a that context. In the expression context, we can write > init_typeseq::u and then use the type variable 'u' as needed. In the > type-expression context (in the context of data and instance > declarations), this trick does not work. I couldn't find a better > solution than loading the above definition into GHCi, entering ":t > init_typeseq" and cutting and pasting GHCi's answer back into the > code: > > > type TI > > = Cons > > Char > > (Cons Int (Cons Bool (Cons String (Cons (Maybe Char) (Nil Bool Bool))))) > > > We can test the typemap as follows > > *> *Main> type_index True init_typeseq > *> 2 > *> *Main> fetch (undefined::Bool) $ alter True init_typeseq > *> True > > > testmap = > > let tp1 = alter True init_typeseq > > tp2 = alter 'a' tp1 > > tp3 = alter False tp2 -- updating the previously-stored value > > in (fetch (undefined::Bool) tp3, fetch 'x' tp3) > > *> *Main> testmap > *> (False,'a') > > As before, to deal with existentials, we need to extend the above > compile-time type-mapping to run-time > > > class (TypeSeq t u) => TypeRep t u where > > tr_index:: t -> u -> Int > > tr_index = type_index > > inj:: t -> u -> u > > inj = alter > > prj:: t -> u -> t > > prj = fetch > > > > instance TypeRep Bool TI > > instance TypeRep Char TI > > instance TypeRep String TI > > instance TypeRep Int TI > > > We can use any TypeSeq -- init_typeseq or any other TypeSeq. We can > define a number of suitable TypeSeq values in various modules and > import the most suitable one. > > The function sAFECoerce is trivial: > > > sAFECoerce a = sAFECoerce' a (init_typeseq::TI) > > > > sAFECoerce' (a::a) tenv ::b > > = prj (undefined::b) $ inj a tenv > > It stores its argument into the type environment, and then retrieves it > given the target type as the index. If the source and the target types > are the same, the retrieved value is identical to the argument of > sAFECoerce'. Otherwise, sAFECoerce' returns whatever value has been > stored in the typenv under the target type (the default value). > > > We have remarked earlier that this message was intended to solve an > unstated question in Amr Sabry's original message. The unstated > question is the need to cast into an existentially quantified > datatype. Here's the description of the problem and the stated > question: > > > data F a b = > > forall c. (TypeRep c TI) => PushF (a -> c) (F c b) > > | Bottom (a -> b) > > > > f1 :: Char -> Bool > > f1 'a' = True > > f1 _ = False > > > > f2 :: Bool -> String > > f2 True = "true" > > f2 False = "false" > > > > f3 :: String -> Int > > f3 = length > > > > fs = PushF f1 (PushF f2 (PushF f3 (Bottom id))) > > ] Is it possible to write a function > ] f :: F a b -> T c -> F c b > ] where (T c) is some type for values of type 'c' or values representing > ] the type 'c' or whatever is appropriate. Thus if given the > ] representation of Bool, the function should return: > ] PushF f2 (PushF f3 (Bottom id)) > ] and if given the representation of String the function should return > ] PushF f3 (Bottom id) > ] and so on. > > The solution given earlier is: > > > data HF = forall a b. (TypeRep a TI,TypeRep b TI) => HF (F a b) > > show_fn_type:: (TypeRep a TI, TypeRep b TI) => (a->b) -> String > > show_fn_type (g::a->b) > > = "(" ++ (show (tr_index (undefined::a) (undefined::TI) )) ++ > > "->"++(show (tr_index (undefined::b) (undefined::TI))) ++ ")" > > > > instance (TypeRep a TI, TypeRep b TI) => Show (F a b) where > > show = show . hsf_to_lst . HF > > where > > hsf_to_lst (HF (Bottom g)) = [show_fn_type g] > > hsf_to_lst (HF (PushF g next)) = (show_fn_type g):(hsf_to_lst$HF next) > > > > > f':: (TypeRep c TI) => (F a b) -> c -> F a b > > f' here@(PushF g next::(F a b)) v = > > if tr_index v (undefined::TI) == tr_index (g undefined) (undefined::TI) > > then here > > else case next of > > PushF g1 next' -> f' (PushF (g1.g) next') v > > Bottom g1 -> f' (Bottom (g1.g)) v > > > > f fs v = f' (PushF id fs) v > > > > flatten:: (TypeRep a TI, TypeRep b TI) => F a b -> (a -> b) > > flatten fs :: (a->b) > > = case f fs (undefined::b) of > > PushF g (Bottom g1) -> g1.g > > In short, the function f' takes a data structure F a b and a value of > type c and returns another data structure F a b, but of a different > structure > PushF g next > here 'next' has the type F c b -- which is the answer to Amr Sabry's > question. The function g::a->c is a composition of all previously > occurring functions. This is a neat "side-effect" of the function f': > we partially compose the given F a b structure up to the given type. > > Technically, the function f' answers Amr Sabry's question. Alas, the > answer, until now, was useless. The answer, the second field in the > structure returned by f', is existentially quantified. We can do > preciously little with it -- until now. > > Now we can write > > > t1 v = case f fs v of > > PushF _ (next::F c b) -> flatten next $ sAFECoerce v > > Here we cast into an existential type. > > *> *Main> t1 'a' > *> 4 > *> *Main> t1 False > *> 5 > *> *Main> t1 "xyz" > *> 3 > > > > [1] Previous message > Pure functional TypeRep [Was: Existentials...] > http://www.haskell.org/pipermail/haskell/2003-July/012330.html > > [2] escape from existential quantification > http://www.haskell.org/pipermail/haskell/2003-February/011288.html > > [3] Re: escape from existential quantification > http://www.haskell.org/pipermail/haskell/2003-February/011293.html > _______________________________________________ > Haskell mailing list > [EMAIL PROTECTED] > http://www.haskell.org/mailman/listinfo/haskell > _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell