This message shows how to map _types_ to integers at compile time -- and then extend this facility to run-time so it can be used with existentially-quantified types. It is statically guaranteed that different types receive different integer labels. Unlike TyCons of Dynamics, our mapping does NOT rely on unsafePerformIO. We use the typechecker itself to compare types. It seems our typemap can also be used for _safe_ casts, in particular, for casting away the existential blemish.

This message was inspired by Amr Sabry's problem on existentials. Unlike Hal Daume's solution posted here earlier, we do not use Dynamics nor GMap -- therefore, we completely avoid unsafePerformIO and unsafeCoerce. Our solution is purely functional and assuredly type-safe (to the extent the typechecker can be trusted). Extensions used: -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances First, the compile-time mapping from types to integers. Polytypic list: > 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 and the finite map from types to integers > class TypeSeq t s where > type_index:: t -> s -> Int > > instance (PList Cons t r) => TypeSeq t (Cons t r) where > type_index _ _ = 0 > > instance (PList Cons t' r', TypeSeq t r') => TypeSeq t (Cons t' r') where > type_index v s = 1 + (type_index v $ cdr s) Let us build some finite map > init_typeseq = Cons (undefined::Char) $ > Cons (undefined::Int) $ > Cons (undefined::Bool) $ > Cons (undefined::String) $ > Cons (undefined::Maybe Char) $ > Nil A typeseq maps a type to an integer -- which is the type's position in the polytypic list. We are satisfied with the first occurrence of the type in the list. It is plain that a typeseq maps different types to different integers. Let us see how it works: -- *Main> type_index True init_typeseq -- 2 -- *Main> type_index 'a' init_typeseq -- 0 -- *Main> type_index "a" init_typeseq -- 3 -- *Main> type_index (1::Int) init_typeseq -- 1 -- *Main> type_index (Just 'a') init_typeseq -- 4 -- *Main> type_index (Just True) init_typeseq -- <interactive>:1: -- No instance for (TypeSeq (Maybe Bool) (Nil t r)) -- arising from use of `type_index' at <interactive>:1 -- In the definition of `it': type_index (Just True) init_typeseq We call this mapping compile-time because the translation from a type to the corresponding encoding (1+1+...1) is done at compile time, when the appropriate instance of the TypeSeq class is chosen. A sufficiently smart compiler can just as well fold the constant expression (1+1...+1) down to a single integer. Also, errors in the translation are reported at compile-time. However, to apply the mapping to existential types, we need to extend the former to run-time. > class TypeRep t where > tr_index:: t -> Int > > -- All of the following are almost the same. > -- The Template Haskell can really help us here > instance TypeRep Char where > tr_index x = type_index x init_typeseq > > instance TypeRep Int where > tr_index x = type_index x init_typeseq > > instance TypeRep Bool where > tr_index x = type_index x init_typeseq > > instance TypeRep String where > tr_index x = type_index x init_typeseq > > instance TypeRep (Maybe Char) where > tr_index x = type_index x init_typeseq Now, Amr Sabry's Problem > data F a b = > forall c. (TypeRep c) => 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))) First, we make fs an instance of class Show. It is jolly convenient. > data HF = forall a b. (TypeRep a,TypeRep b) => HF (F a b) > show_fn_type (g::(a->b)) > = "(" ++ (show (tr_index (undefined::a))) ++ > "->"++(show (tr_index (undefined::b))) ++ ")" > > instance (TypeRep a, TypeRep b) => 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) Now, Amr Sabry's question: ] 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. First, we prepend to the given F a b structure the identity composition. We see the meaning of it below. > f fs v = f' (PushF id fs) v > f':: (TypeRep c) => (F a b) -> c -> F a b > f' here@(PushF g next) (v::tv) = > if tr_index v == tr_index (g undefined) > then here > else case next of > PushF g1 next' -> f' (PushF (g1.g) next') v > Bottom g1 -> f' (Bottom (g1.g)) v 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 Sambry'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. Let us see how it works: *Main> fs ["(0->2)","(2->3)","(3->1)","(1->1)"] *Main> f fs 'a' ["(0->0)","(0->2)","(2->3)","(3->1)","(1->1)"] *Main> f fs True ["(0->2)","(2->3)","(3->1)","(1->1)"] *Main> f fs "a" ["(0->3)","(3->1)","(1->1)"] *Main> f fs (1::Int) ["(0->1)","(1->1)"] Because f is capable of producing any partial composition, it can do the full composition just as easily: > flatten:: (TypeRep a, TypeRep b) => F a b -> (a -> b) > flatten fs :: (a->b) > = case f fs (undefined::b) of > PushF g (Bottom g1) -> g1.g And it indeed works: *Main> flatten fs 'a' 4 -- the length of the word true *Main> flatten fs 'b' 5 -- the length of the word false Again, I can't seem to write any Haskell code that doesn't explicitly use undefined. _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell