•data V
s t
• = ex m . Z where s =
(t,m)
• | ex m x . S (V m t) where s =
(x,m)
•
•data
Exp s t
• = IntC Int where t = Int
• | BoolC Bool where t =
Bool
• | Plus (Exp s Int) (Exp s Int) where t = Int
• | Lteq (Exp s Int) (Exp s Int) where t =
Bool
• | Var (V s t)
•
•Example
Type:
•
•Plus :: forall s t . (t=Int) =>
• Exp s Int -> Exp s Int
-> Exp s t