Pure functional TypeRep [Was: Existentials...]

[oleg@pobox.com]

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.