That's really nice. Very interesting. Thank you. On Fri, Jun 25, 2010 at 9:55 PM, Edward Kmett <ekm...@gmail.com> wrote:
> 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 <ekm...@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.dup...@ext.mpsa.com> 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 >>> >> >> > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
