[Haskell-cafe] The "Exp -> Term a" problem (again), how to dynamically create (polymorphic) typed terms in Haskell ??

[Pasqualino 'Titto' Assini]

Hi, 

I am trying to write an interpreter for a little functional language but I am 
finding very problematic to dynamically create a typed representations of the 
language terms.
 
I have googled around and found a few solutions but none seem to solve the 
problem.
 

This is the example code: 

> {-# OPTIONS -fglasgow-exts #-}
> module Eval where 

These are my untyped terms (what I get from my parser):

> data Exp =  EDouble Double | EString String | EPrim String | EApp Exp Exp 
deriving (Show)

And these are the typed terms:

> data Term a where
>   Num :: Double -> Term Double
>   Str :: String -> Term String
>   App :: Term (a->b) -> Term a -> Term b    
>   Fun :: (a->b) -> Term (a->b)  

The problem is to write a function that converts between Exp and Term t as in:

> test :: Term Double
> test = typecheck $ EApp (EPrim "inc") (EDouble 10.0)

So this is the conversion function:

> class TypeCheck t where
>    typecheck :: Exp -> Term t

A few primitives:

> instance TypeCheck (String->String) where
>    typecheck (EPrim "rev")  = Fun reverse
>    typecheck (EPrim "show")  = Fun show  

> instance TypeCheck (Double->Double) where
>    typecheck (EPrim "inc")   = Fun ((+1) :: Double -> Double) 

> instance TypeCheck (Double->String) where
>    typecheck (EPrim "show")  = Fun show  

> instance TypeCheck Double where
>    typecheck (EDouble x) = Num x 

> instance TypeCheck String where
>    typecheck (EString x) = Str x

The problem arises in the conversion of the function application (EApp). 

It does not seem to be possible to define "typecheck" on EApp in a generic way
and is also not possible to distinguish between the different cases:          

>    typecheck (EApp f a) = App (typecheck f :: Term (String->String)) 
(typecheck a:: Term String)

The following pattern overlaps the previous one:

 >   typecheck (EApp f a) = App (typecheck f :: Term (Double->String)) 
(typecheck a:: Term Double)


To avoid this problem I could split my untyped terms in different data types 
as in:

data EDouble = EDouble Double
data App a b c = App a b c 
...

and define TypeCheck separetely on every data type.

However, in that case what would be the type of my parser??

parser :: String -> ?? 


Any suggestion woud be very welcome indeed,

       titto