Existentials...

Amr A Sabry sabry@cs.indiana.edu
Mon, 28 Jul 2003 16:21:59 -0500


Hi, 

I believe this can be done with enough type hacking but I am not sure
how...

Consider the use existentials to implement a list of composable
functions using something like:

data F a b = 
              forall c. PushF (a -> c) (F c b) 
            | Bottom (a -> b)

For example:

f1 :: Char -> Bool
f1 'a' = True
f1 _ = False

f2 :: Bool -> String
f2 True = "true"
f2 False = "false"

f3 :: String -> Int
f3 = length

fs :: F Char Int
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. 

I hope the question makes sense. Thanks. --Amr