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