Attendees: Wang Meng, Kenny Lu, Greg Duck, Martin Sulzmann
Today we discussed about the similarity and differences between Chameleon
and GRDT(Guarded Recursive Data Types).
Write up (from Wang Meng):
Let's consider an data type for a AST:
> data Exp = I Int
> | Val String
> | App Exp Exp
> | Abs Exp Exp
> | Fix Exp
It is obvious that the above encoding is not type safe.
GRDT parametric the type declaration in a way similar to
phantom type.
In phantom type we can have:
> data Exp' a = E Exp
> eval :: Exp' a -> a
However, we can never prevent sth like:
> eval (E (App (I 1) (I 1)))
In GRDT, guards are inposed on the clauses of the data type declaration:
> data Exp a = I Int where a = Int
> | Var String
> | App (Exp a' -> Exp b' , Exp a') where a = b'
> | Abs (Exp a' -> Exp b') where a = a' -> b'
> | Fix (Exp a -> Exp a)
Here, the type correctness is enforced by the guards. And static type
matching is replaced by dynamic value matching.
The eval function can be defined as:
> eval :: Exp a -> a
> eval (I i) = i
> eval (Val v) = v
> eval (App (e1, e2)) = (eval e1) (eval e2)
> eval (Abs f) = \x -> eval (f (Var x))
> eval e@(Fix f) = eval (f e)
The success of dynamic value matching is ensured by type checking.
What interesting is that non-inductive definitions like Fix can be typed
here. In Haskell this will result in a cycle:
Here's an attempt.
-- we need to turn value matching into type matching
-- hence we need to introduce singleton types
data Fix f = Fix f
class Eval a where eval :: a
instance ??? => Eval (Fix f -> b) where
eval (Fix f) = eval (f (Fix f))
Question, how does the instance context look like?
Let's perform type inference for
eval (Fix f) = eval (f (Fix f))
The following type equations arise
f = Fix f -> a Unfication failure!
Hence, we cannot provide an instance for fix.
We conclude:
GRDTS: type-safe, tag-full, evidence construction at run-time
Haskell/Chameleon: type-safe, tag-free, evidence construction at compile-time
Note that it's not obvious how to provide a typed semantics for GRDTs.
Martin also mentioned evidence free translation of chameleon. The basic
idea is to adding tags to a close set of types to avoid the additional
evidence parameter. We will discuss more details on this topic next Wed.