{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
-- Encoding of GADTs with typeclasses,
-- using the `poster' GADT example, tagless interpreter.
-- The example is described in any GADT paper.
-- This file shows that the example can trivially be encoded with
-- the typeclasses.
-- The advantage of the type-class encoding is that the term
-- syntax is extensible.
-- This code was written and shown to several people in Sep 2004.
module TaglessInterp where
class Term c a | c->a
-- The syntax of our terms
newtype Lit a = Lit a
newtype Inc a = Inc a
newtype IsZ a = IsZ a
newtype If a b c = If (a,b,c)
newtype Fst a = Fst a
newtype Snd a = Snd a
newtype Pair a b = Pair (a,b)
-- well-formedness rules
instance Term (Lit Int) Int
instance Term a Int => Term (Inc a) Int
instance Term a Int => Term (IsZ a) Bool
instance (Term t Bool, Term b1 a, Term b2 a) => Term (If t b1 b2) a
instance (Term t1 a, Term t2 b) => Term (Pair t1 t2) (a,b)
instance Term t (a,b) => Term (Fst t) a
instance Term t (a,b) => Term (Snd t) b
-- The tagless interpreter (evaluator). There are no algebraic
-- data types, hence no run-time tag checking. The code is just as
-- efficient as the GADT code
class Term t a => Eval t a | t->a where
eval:: t -> a
instance Term (Lit a) a => Eval (Lit a) a where
eval (Lit i) = i
instance Eval t Int => Eval (Inc t) Int where
eval (Inc t) = eval t + 1
instance Eval t Int => Eval (IsZ t) Bool where
eval (IsZ t) = eval t == 0
instance (Eval t Bool, Eval b1 a, Eval b2 a) => Eval (If t b1 b2) a where
eval (If (t,b1,b2)) = if eval t then eval b1 else eval b2
instance (Eval t1 a, Eval t2 b) => Eval (Pair t1 t2) (a,b) where
eval (Pair (t1,t2)) = (eval t1, eval t2)
instance Eval t (a,b) => Eval (Fst t) a where
eval (Fst t) = fst (eval t)
instance Eval t (a,b) => Eval (Snd t) b where
eval (Snd t) = snd (eval t)
t1 = If ( (IsZ (Fst (Pair (Lit (0::Int), Lit (1::Int)))))
, (Inc (Fst (Pair (Lit (0::Int), Lit (1::Int)))))
, (Inc (Snd (Pair (Lit (0::Int), Lit (1::Int))))) )
et1 = eval t1
-- Unlike GADTs, our term syntax is extensible.
-- We can add a decrement operator, for example.
newtype Dec a = Dec a
instance Term a Int => Term (Dec a) Int
instance Eval t Int => Eval (Dec t) Int where
eval (Dec t) = eval t - 1
t2 = If ( (IsZ (Fst (Pair (Lit (1::Int), Lit (1::Int)))))
, (Inc (Fst (Pair (Lit (0::Int), Lit (1::Int)))))
, (Dec (Snd (Pair (Lit (0::Int), Lit (1::Int))))) )
et2 = eval t2