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