[Template-haskell] Types as first-class values

[Claus Reinke]

Hi,

probably, I missed part of your problem, and there are quite a few concepts in
your email, so I'll take it slowly. embedding untyped lambda into Haskell is fairly 
simple, as long as you don't want to print terms, or visualise reductions:

data U = In { out :: U -> U } deriving Show

this gives you a universal type, an embedding of unary functions into that type, 
and a projection of unary functions out of that type. so you can keep your haskell
implementation busy evaluating embedded lambda terms like this one:

(\x-> (out x) x) (In (\x-> (out x) x)) -- keep ready to hit ctrl-c

as you say that you also want to represent the application structure, the type
gets a little more complex (using the part of your Term type that is the image of
correct sentences, implicitly encoding the types as well):

-- just local quantification, no GADTs needed
-- the type parameter encodes the type of the semantic object represented
data SemTerm a = forall b .  App (SemTerm (b->a)) (SemTerm b)
               | Sem a

Unlike your Term type, this SemTerm type only holds type-correct applications 
and other semantic objects, such as primitive functions from your lexicon. there 
is no need to distinguish functions of different arities or to encode types explicitly
(Z, U??, B??, ..), thanks to currying and embedded typing. so there is no need for 
an explosion of cases, either in the SemTerm type or in its application. just use 
Sem to inject your predefined functions/words, and App to apply them to 
arguments, and evaluation becomes simply:

eval :: SemTerm a -> a
eval (App f e) = (eval f) (eval e)
eval (Sem e)   = e

so can can have your cake (representation) and eat it (embedded typing and
evaluation):

rv = Sem (reverse::String->String)
tl = Sem tail
pp = Sem (++)
dot = Sem (.)
hi = Sem "hi "
there = Sem "there!"
x = App rv (App (App (App dot tl) rv)
                (App (App pp hi) there))

main = print $ (x ,eval x)

*Main> main
((<function> (((<function> <function>) <function>) ((<function> "hi ") "there!")
)),"hi there")

if you actually wanted to have representations of the function types as well, 
you could use Typeable, but typeOf only works for non-polymorphic types 
(so you can ask for 'typeOf x' or 'typeOf rv' in the attached code, but you 
would need to specialise the other function types to disambiguate the 
computation of type representations, as already done for rv).

there are probably other requirements that stand against this representation (?),
but at least it solves some of the issues you mentioned. and it uses fewer 
features (no GADTs, no template haskell).

cheers,
claus

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Sem.hs
Type: application/octet-stream
Size: 1512 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/template-haskell/attachments/20050524/a58e4801/Sem.obj