Edward Kmett ekmett at gmail.com
Fri Jun 25 15:55:34 EDT 2010

I've obtained permission to repost Gershom's slides on how to deserialize
source file, that he was rendering to slides. Consequently, I've just pasted
the content below as a literate email.

-Edward Kmett

-
Deserializing strongly typed values

Gershom Bazerman

-
prior art:
Oleg (of course)
http://okmij.org/ftp/tagless-final/course/course.html

...but also
Stephanie Weirich
http://www.comlab.ox.ac.uk/projects/gip/school/tc.hs

=
Ahem...
\begin{code}
{-# LANGUAGE DeriveDataTypeable,
ExistentialQuantification,
FlexibleContexts,
FlexibleInstances,
FunctionalDependencies,
RankNTypes,
ScopedTypeVariables
#-}
\end{code}
=
ahem.
\begin{code}
import Data.Typeable
import Data.Maybe
import Control.Applicative
import qualified Data.Map as M
import Unsafe.Coerce
\end{code}
=

\begin{code}
data SimpleExpr = SOpBi String SimpleExpr SimpleExpr
| SOpUn String SimpleExpr
| SDbl Double
| SBool Bool deriving (Read, Show, Typeable)

\end{code}
Yawn.
=

\begin{code}
data Expr a where
EDbl  :: Double -> Expr Double
EBool :: Bool -> Expr Bool
EBoolOpBi :: BoolOpBi -> Expr Bool -> Expr Bool -> Expr Bool
ENumOpBi  :: NumOpBi -> Expr Double -> Expr Double -> Expr Double
ENumOpUn  :: NumOpUn -> Expr Double -> Expr Double
deriving Typeable

data NumOpBi = Add | Sub deriving (Eq, Show)
data NumOpUn = Log | Exp deriving (Eq, Show)
data BoolOpBi = And | Or deriving (Eq, Show)
\end{code}

The GADT is well typed. It cannot go wrong.
-
It also cannot derive show.
=
But we can write show...

\begin{code}
showIt :: Expr a -> String
showIt (EDbl d) = show d
showIt (EBool b) = show b
showIt (EBoolOpBi op x y) = "(" ++ show op
++ " " ++ showIt x
++ " " ++ showIt y ++ ")"
showIt (ENumOpBi op x y)  = "(" ++ show op
++ " " ++ showIt x
++ " " ++ showIt y ++ ")"
showIt (ENumOpUn op x) = show op ++ "(" ++ showIt x ++ ")"
\end{code}
=
And eval is *much nicer*.
It cannot go wrong --> no runtime typechecks.

\begin{code}
evalIt :: Expr a -> a
evalIt (EDbl x) = x
evalIt (EBool x) = x
evalIt (EBoolOpBi op expr1 expr2)
| op == And = evalIt expr1 && evalIt expr2
| op == Or  = evalIt expr2 || evalIt expr2

evalIt (ENumOpBi op expr1 expr2)
| op == Add = evalIt expr1 + evalIt expr2
| op == Sub = evalIt expr1 - evalIt expr2
\end{code}
=
But how do we write read!?

read "EBool False" = Expr Bool
read "EDbl 12" = Expr Double

The type being read depends on the content of the string.

Even worse, we want to read not from a string that looks obvious
to Haskell (i.e. a standard showlike instance) but from
something that looks pretty to the user -- we want to *parse*.

So we parse into our simple ADT.

-
But how?

How do we go from untyped... to typed?

[And in general -- not just into an arbitrary GADT,
but an arbitrary inhabitant of a typeclass.]

[i.e. tagless final, etc]

=
Take 1:
Even if we do not know what type we are creating,
we eventually will do something with it.

So we paramaterize our typechecking function over
an arbitrary continuation.

\begin{code}
mkExpr :: (forall a. (Show a, Typeable a) => Expr a -> r) -> SimpleExpr -> r
mkExpr k expr = case expr of
SDbl d  -> k $EDbl d SBool b -> k$ EBool b
SOpUn op expr1 -> case op of
"log" -> k $mkExpr' (ENumOpUn Log) expr1 "exp" -> k$ mkExpr' (ENumOpUn Exp) expr1
_ -> error "bad unary op"
SOpBi op expr1 expr2 -> case op of
"add" -> k $mkExprBi (ENumOpBi Add) expr1 expr2 "sub" -> k$ mkExprBi (ENumOpBi Sub) expr1 expr2
\end{code}
=
Where's the typechecking?

\begin{code}
mkExpr' k expr = mkExpr (appCast $k) expr mkExprBi k expr1 expr2 = mkExpr' (mkExpr' k expr1) expr2 appCast :: forall a b c r. (Typeable a, Typeable b) => (c a -> r) -> c b -> r appCast f x = maybe err f$ gcast x
where err = error $"Type error. Expected: " ++ show (typeOf (undefined::a)) ++ ", Inferred: " ++ show (typeOf (undefined::b)) \end{code} ... We let Haskell do all the work! = Hmmm... the continuation can be anything. So let's just make it an existential constructor. \begin{code} data ExprBox = forall a. Typeable a => ExprBox (Expr a) appExprBox :: (forall a. Expr a -> res) -> ExprBox -> res appExprBox f (ExprBox x) = f x tcCast :: forall a b c. (Typeable a, Typeable b) => Expr a -> Either String (Expr b) tcCast x = maybe err Right$ gcast x
where err = Left $"Type error. Expected: " ++ show (typeOf (undefined::a)) ++ ", Inferred: " ++ show (typeOf (undefined::b)) \end{code} Now we can delay deciding what to apply until later. Typecheck once, execute repeatedly! = One more trick -- monadic notation lets us extend the context of unpacked existentials to the end of the do block \begin{code} retBox x = return (ExprBox$ x, typeOf x)

typeCheck :: SimpleExpr -> Either String (ExprBox, TypeRep)
typeCheck (SDbl d) = retBox (EDbl d)
typeCheck (SBool b) = retBox (EBool b)
typeCheck (SOpBi op s1 s2) = case op of
"sub" -> tcBiOp (ENumOpBi Sub)
"and" -> tcBiOp (EBoolOpBi And)
"or"  -> tcBiOp (EBoolOpBi Or)
where
tcBiOp constr = do
(ExprBox e1, _) <- typeCheck s1
(ExprBox e2, _) <- typeCheck s2
e1' <- tcCast e1
e2' <- tcCast e2
retBox $constr e1' e2' \end{code} = So that's fine for *very* simple expressions. How does it work for interesting GADTs? (like, for example, HOAS)? (The prior art doesn't demonstrate HOAS -- it uses DeBruijn.) = Our simple world \begin{code} type Ident = String type TypeStr = String data STerm = SNum Double | SApp STerm STerm | SVar Ident | SLam Ident TypeRep STerm \end{code} Note.. terms are Church style -- each var introduced has a definite type. Determining this type is left as an exercise. = Over the rainbow in well-typed land. \begin{code} data Term a where TNum :: Double -> Term Double TApp :: Term (a -> b) -> Term a -> Term b TLam :: Typeable a => (Term a -> Term b) -> Term (a -> b) TVar :: Typeable a => Int -> Term a deriving Typeable \end{code} Wait! DeBrujin (TVar) *and* HOAS (TLam)! The worst of both worlds. Don't worry. In the final product all TVars are eliminated by construction. Exercise to audience: rewrite the code so that TVar can be eliminated from the Term type. = Show and eval... \begin{code} showT :: Int -> Term a -> String showT c (TNum d) = show d showT c (TApp f x) = "App (" ++ showT c f ++ ") (" ++ showT c x ++ ")" showT c (TLam f) = "Lam " ++ ("a"++show c) ++ " -> " ++ (showT (succ c)$ f (TVar c))
showT c (TVar i)   = "a"++show i

runT :: Term a -> Term a
runT (TNum d) = (TNum d)
runT (TLam f) = (TLam f)
runT (TApp f x) = case runT f of TLam f' -> runT (f' x)
runT (TVar i) = error (show i)
\end{code}
=
The existential

\begin{code}
data TermBox = forall a. Typeable a => TermBox (Term a)
appTermBox :: (forall a. Typeable a => Term a -> res) -> TermBox -> res
appTermBox f (TermBox x) = f x
\end{code}
=
The typechecker returns a box *and* a typeRep.

Cast is the usual trick.

\begin{code}
retTBox :: Typeable a => Term a -> Either String (TermBox, TypeRep)
retTBox x = return (TermBox $x, typeOf x) type Env = M.Map Ident (TermBox, TypeRep) trmCast :: forall a b c. (Typeable a, Typeable b) => Term a -> Either String (Term b) trmCast x = maybe err Right$ gcast x
where err = Left $"Type error. Expected: " ++ show (typeOf (undefined::a)) ++ ", Inferred: " ++ show (typeOf (undefined::b)) \end{code} = \begin{code} typeCheck' :: STerm -> Env -> Either String (TermBox, TypeRep) typeCheck' t env = go t env 0 where go (SNum d) _ idx = retTBox (TNum d) go (SVar i) env idx = do (TermBox t, _) <- maybe (fail$ "not in scope: " ++ i)
return $M.lookup i env retTBox$ t
\end{code}

Nums and vars are easy.
=
App and Lam... less so.

\begin{code}
go (SApp s1 s2) env idx = do
(TermBox e1, tr1) <- go s1 env idx
(TermBox e2, _) <- go s2 env idx
TermBox rt <- return $mkTerm$ head $tail$
typeRepArgs $head$ typeRepArgs $tr1 -- TypeReps have their... drawbacks. e1' <- trmCast e1 retTBox$ TApp e1' e2 asTypeOf rt
go (SLam i tr s) env idx = do
TermBox et <- return $mkTerm tr (TermBox e, _) <- go s (M.insert i (TermBox (TVar idx asTypeOf et),tr) env ) (idx + 1) retTBox$ TLam (\x -> subst (x asTypeOf et) idx e)
\end{code}
=
How does mkTerm work?

\begin{code}
mkTerm :: TypeRep -> TermBox
mkTerm tr = go tr TermBox
where
go :: TypeRep -> (forall a. (Typeable a) => Term a -> res) -> res
go tr k
| tr == typeOf (0::Double) = k (TNum 0)
| typeRepTyCon tr == arrCon =
go (head $typeRepArgs tr)$ \xt -> go (head $tail$ typeRepArgs tr)
$\y -> k (TLam$ \x -> const y (x asTypeOf xt))

arrCon = typeRepTyCon $typeOf (undefined::Int -> String) \end{code} Same principle -- but can build arrows directly. Doing so requires staying cps... I think. = And this is how we get rid of the DeBruijn terms. \begin{code} subst :: (Typeable a) => Term a -> Int -> Term b -> Term b subst t i trm = go trm where go :: Term c -> Term c go (TNum d) = (TNum d) go (TApp f x) = TApp (go f) (go x) go (TLam f) = TLam (\a -> go (f a)) go (TVar i') | i == i' = either error id$ trmCast t
| otherwise = (TVar i')
\end{code}

Q: Now you see why DeBruijn is handy -- substitution
is otherwise a pain.

=
But note -- all functions must be monotyped.
This is the simply typed lambda calculus.

How do we represent TLam (\a -> a)?

The masses demand HM polymorphism.
-

Take 4:

A damn dirty hack.

=
All hacks begin with Nats.

\begin{code}
data Z = Z deriving (Show, Typeable)
data S a = S a deriving (Show, Typeable)
\end{code}
=
typeCheck is almost the same.

\begin{code}
typeCheck'' :: STerm -> Env -> Either String (TermBox, TypeRep)
typeCheck'' t env = go t env 0
where
go :: STerm -> Env -> Int -> Either String (TermBox, TypeRep)
go (SNum d) _ idx = retTBox (TNum d)
go (SVar i) env idx = do
(TermBox t, _) <- maybe (fail $"not in scope: " ++ i) return$ M.lookup i env
retTBox $t \end{code} = \begin{code} go (SApp s1 s2) env idx = do (TermBox e1, tr1) <- go s1 env idx (TermBox e2, _) <- go s2 env idx TermBox rt <- unifyAppRet e1 e2 e1' <- unifyAppFun e1 e2 retTBox$ TApp e1' e2 asTypeOf rt
go (SLam i tr s) env idx = do
TermBox et <- return $mkTerm'$ tr
(TermBox e, _) <- go s (M.insert i
(TermBox (TVar idx asTypeOf et),tr)
env)
(idx + 1)
retTBox $TLam (\x -> subst (x asTypeOf et) idx e) \end{code} It looks like we just factored on the nasty arrow code. = mkTerm is almost the same... we just extended it to deal with Nats. \begin{code} mkTerm' :: TypeRep -> TermBox mkTerm' tr = go tr TermBox where go :: TypeRep -> (forall a. (Typeable a) => Term a -> res) -> res go tr k | tr == typeOf (0::Double) = k (TNum 0) | tr == typeOf Z = k (TVar 0 :: Term Z) | typeRepTyCon tr == succCon = go (head$ typeRepArgs tr)
$\t -> k$ succTerm t
| isArr tr =
go (head $typeRepArgs tr)$ \xt -> go (head $tail$ typeRepArgs tr)
$\y -> k (TLam$ \x -> const y (x asTypeOf xt))
| otherwise = error $show tr succCon = typeRepTyCon$ typeOf (S Z)
succTerm :: Typeable b => Term b -> Term (S b)
succTerm _ = TVar 0
\end{code}
=
Some utilities
\begin{code}
isArr :: TypeRep -> Bool
isArr x = typeRepTyCon x == (typeRepTyCon $typeOf (undefined::Int -> String)) splitArrCon :: TypeRep -> Either String (TypeRep, TypeRep) splitArrCon x | isArr x = case typeRepArgs x of [a,b] -> Right (a,b) _ -> Left$ "Expected function, inferred: " ++ show x
| otherwise = Left $"Expected function, inferred: " ++ show x \end{code} = Give an arrow term we unify it with its argument... and return a witness. \begin{code} unifyAppRet :: forall a b. (Typeable a, Typeable b) => Term a -> Term b -> Either String TermBox unifyAppRet x y = do tr <- unifyAppTyps (head$ typeRepArgs $typeOf x) (head$ typeRepArgs $typeOf y) return$ mkTerm' tr

\end{code}
=
Yes. Actual unification.
(although this is unification of a type template,
so at least it is local)
\begin{code}
unifyAppTyps :: TypeRep -> TypeRep -> Either String TypeRep
unifyAppTyps trf trx = do
(fl,fr) <- splitArrCon trf
env <- go M.empty fl trx
subIt env fr
where
-- go yields a substitution environment.
go :: M.Map String TypeRep -> TypeRep ->
TypeRep -> Either String (M.Map String TypeRep)
go env x y
| isFree x = case M.lookup (show x) env of
Just x' -> if x' == y then return env else Left
(error "a")
Nothing -> return $M.insert (show x) y env | isArr x = do (lh,rh) <- splitArrCon x (lh',rh') <- splitArrCon y env' <- go env lh lh' go env' rh rh' | otherwise = if x == y then return env else Left (error "b") \end{code} = \begin{code} -- subIt applies it subIt :: M.Map String TypeRep -> TypeRep -> Either String TypeRep subIt env x | isFree x = case M.lookup (show x) env of Just x' -> return x' Nothing -> Left (error "c") | isArr x = do (lh,rh) <- splitArrCon x lh' <- subIt env lh rh' <- subIt env rh return$ mkTyConApp arrCon [lh',rh']
| otherwise = return x
succCon = typeRepTyCon $typeOf (S Z) zCon = typeRepTyCon$ typeOf Z
isFree x = typeRepTyCon x elem [zCon, succCon]
arrCon = (typeRepTyCon $typeOf (undefined::Int -> String)) \end{code} = And now, we just have to convince GHC that they unify! \begin{code} unifyAppFun :: forall a b c. (Typeable a, Typeable b, Typeable c) => Term a -> Term b -> Either String (Term c) unifyAppFun x y = do unifyAppTyps (head$ typeRepArgs $typeOf x) (head$ typeRepArgs $typeOf y) return$ unsafeCoerce x
\end{code}
=
Problem solved.

On Fri, Jun 25, 2010 at 2:03 PM, Edward Kmett <ekmett at gmail.com> wrote:

> It turns out that defining Read is somewhat tricky to do for a GADT.
>
> Gershom Bazerman has some very nice slides on how to survive the process by
> manual typechecking (much in the spirit of Oleg's meta-typechecking code
> referenced by Stephen's follow up below)
>
> He presented them at hac-phi this time around.
>
> I will check with him to see if I can get permission to host them somewhere
> and post a link to them here.
>
> -Edward Kmett
>
>
> On Fri, Jun 25, 2010 at 5:04 AM, <corentin.dupont at ext.mpsa.com> wrote:
>
>>
>>
>> I'm having trouble writing a Read Instance for my GATD.
>> Arg this GATD!! It causes me more problems that it solves ;)
>> Especially with no automatic deriving, it adds a lot of burden to my code.
>>
>> >data Obs a where
>> >    ProposedBy :: Obs Int       -- The player that proposed the tested
>> rule
>> >    Turn       :: Obs Turn      -- The current turn
>> >    Official   :: Obs Bool      -- whereas the tested rule is official
>> >    Equ        :: (Eq a, Show a, Typeable a) => Obs a -> Obs a -> Obs
>> Bool
>> >    Plus       :: (Num a) => Obs a -> Obs a -> Obs a
>> >    Time       :: (Num a) => Obs a -> Obs a -> Obs a
>> >    Minus      :: (Num a) => Obs a -> Obs a -> Obs a
>> >    And        :: Obs Bool -> Obs Bool -> Obs Bool
>> >    Or         :: Obs Bool -> Obs Bool -> Obs Bool
>> >    Not        :: Obs Bool -> Obs Bool
>> >    Konst      :: a -> Obs a
>>
>>
>> > readPrec = (prec 10 $do >> > Ident "ProposedBy" <- lexP >> > return (ProposedBy)) >> > +++ >> > (prec 10$ do
>> >        Ident "Official" <- lexP
>> >        return (Official))
>> >  (etc...)
>>
>> Observable.lhs:120:8:
>>    Couldn't match expected type Int' against inferred type Bool'
>>      Expected type: ReadPrec (Obs Int)
>>      Inferred type: ReadPrec (Obs Bool)
>>
>>
>> Indeed "ProposedBy" does not have the same type that "Official".
>> Mmh how to make it all gently mix altogether?
>>
>>
>> Best,
>> Corentin
>>
>>
>> _______________________________________________