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