Re: [Haskell-cafe] The Exp - Term a problem (again), how to dynamically create (polymorphic) typed terms in Haskell ??
On 10/4/07, Pasqualino 'Titto' Assini [EMAIL PROTECTED] wrote: 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: You want to pattern-match on types and the easiest way to do it is to introduce a witness GADT for types, something like: data Type a where TString :: Type String TFun :: Type a - Type b - Type (a - b) ... It will be useful to write function: termType :: Term a - Type a You'll probably have to decorate Term constructors with Type's in a few places. As for the typecheck function - it has to be able to return any Term type, dynamically. Existentially quantificated data constructors will be handy here. Here's what I use: data Dyn c = forall a. Dyn (c a) withDyn :: Dyn c - (forall a. c a - b) - b withDyn (Dyn e) f = f e Your typecheck function can have type: typecheck :: Exp - Dyn Term or rather typecheck :: Exp - Maybe (Dyn Term) You define it recursively, getting Dyn Term for subexpressions, checking their types, building bigger Dyn Terms, and so on. You'll probably need some other support functions for working with Dyn and Type - at least I did. I think something similar is presented in Hinze's paper, recommended by Dominic. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Exp - Term a problem (again), how to dynamically create (polymorphic) typed terms in Haskell ??
Hello Tomasz, thank you very much for your advice. Just a quick question, why using your own Dyn rather than Data.Dynamic? Regards, titto On Thursday 04 October 2007 08:57:11 Tomasz Zielonka wrote: On 10/4/07, Pasqualino 'Titto' Assini [EMAIL PROTECTED] wrote: 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: You want to pattern-match on types and the easiest way to do it is to introduce a witness GADT for types, something like: data Type a where TString :: Type String TFun :: Type a - Type b - Type (a - b) ... It will be useful to write function: termType :: Term a - Type a You'll probably have to decorate Term constructors with Type's in a few places. As for the typecheck function - it has to be able to return any Term type, dynamically. Existentially quantificated data constructors will be handy here. Here's what I use: data Dyn c = forall a. Dyn (c a) withDyn :: Dyn c - (forall a. c a - b) - b withDyn (Dyn e) f = f e Your typecheck function can have type: typecheck :: Exp - Dyn Term or rather typecheck :: Exp - Maybe (Dyn Term) You define it recursively, getting Dyn Term for subexpressions, checking their types, building bigger Dyn Terms, and so on. You'll probably need some other support functions for working with Dyn and Type - at least I did. I think something similar is presented in Hinze's paper, recommended by Dominic. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Exp - Term a problem (again), how to dynamically create (polymorphic) typed terms in Haskell ??
On Thu, Oct 04, 2007 at 05:05:23PM +0100, Pasqualino 'Titto' Assini wrote: Hello Tomasz, thank you very much for your advice. Just a quick question, why using your own Dyn rather than Data.Dynamic? Well, it's a bit different from Data.Dynamic. You have a guarantee that (Dyn Term) contains (Term t) for some t. Besides, making Term an instance of Typeable wouldn't buy us anything. You would have to define Type GADT anyway. Best regards Tomek ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] The Exp - Term a problem (again), how to dynamically create (polymorphic) typed terms in Haskell ??
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
