You could make use of the equality data type[1,2]:
newtype Equal a b = Eq (forall f . f a - f b)
cast :: Equal a b - (a - b)
cast (Equal f) = f id
Your data type would be:
data Term a = Lit Int (Equal Int a)
| Inc (Term Int) (Equal Int a)
| ...
| forall b c . Pair (Term b) (Term c) (Equal (b,c) a)
eval :: Term a - a
eval (Lit x eq) = cast x eq
eval ... = ...
A value of type 'Equal a b' serves as a proof that 'a' and 'b' are
equal. Its use is described in [1] and [2]. Pasalic [3] makes use of
this type to implement typed abstract syntax. This paper describes what
you are trying to achieve with your 'Term' data type.
Arthur
[1]Typing Dynamic Typing, Arthur Baars and Doaitse Swierstra. ICFP 2002.
http://www.cs.uu.nl/~arthurb/dynamic.html
[2]A lightweight implementation of generics and dynamics, James Cheney
and Ralf Hinze. Haskell Workshop 2002, Pittsburgh, PA, 2002.
http://www.cs.cornell.edu/people/jcheney/papers/Dynamic-final.pdf
[3]Emir Pasalic: Meta-Programming with Typed Object-Language
Representations.
http://www.cse.ogi.edu/~pasalic/
On 22-jul-04, at 18:06, Jim Apple wrote:
I tried to post this to gmane.comp.lang.haskell.general, but it never
got there - it may belong here anyway.
Abraham Egnor wrote:
Is there any closer approximation [of GADTs] possible?
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
data Term a = forall b . (EqType a b, EqType b Int) = Lit Int
| forall b . (EqType a b, EqType b Int) = Inc (Term Int)
| forall b . (EqType a b, EqType b Bool) = IsZ (Term Int)
| If (Term Bool) (Term a) (Term a)
| forall b . Fst (Term (a,b))
| forall b . Snd (Term (b,a))
| forall b c . (EqType a (b,c))= Pair (Term b) (Term c)
class EqType a b | a-b, b-a
instance EqType a a
Unfortunately, I can't seem to write an eval function:
eval (Lit a) = a
gives
Inferred type is less polymorphic than expected
Quantified type variable `b' is unified with `Int'
When checking an existential match that binds
The pattern(s) have type(s): Term Int
The body has type: Int
In the definition of `eval': eval (Lit x) = x
Any ideas?
Jim
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
