New subject: Manual Type-Checking to provide Read instances for GADTs. (was Re: Read instance for GATD)

25 Jun 2010

      I've obtained permission to repost Gershom's slides on how to deserialize
GADTs by typechecking them yourself, which are actually a literate haskell
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

(four easy pieces about typechecking)

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,
             GADTs,
             RankNTypes,
             ScopedTypeVariables
 #-}
\end{code}
=
ahem.
\begin{code}
import Data.Typeable
import Data.Maybe
import Control.Monad.Error
import Control.Applicative
import qualified Data.Map as M
import Unsafe.Coerce
\end{code}
=
A simple ADT.

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

\end{code}
Yawn.
=
An awesome GADT!

\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.

Then we turn our simple ADT into our nice GADT.
-
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
           "add" -> tcBiOp (ENumOpBi Add)
           "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  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,  wrote:
...
Hello Haskellers,
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
...
instance Read a => Read (Obs a) where
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Manual Type-Checking to provide Read instances for GADTs. (was Re: [Haskell-cafe] Read instance for GATD)

Edward Kmett

Dupont Corentin

tags

participants (2)