[Haskell-cafe] An example of dependent types [was: Simple GADT parser for the eval example]

[oleg at pobox.com]

Greg Buchholz has posed an interesting problem of writing a
typechecker. Given untyped terms of the form

> data Expr = ELit Int
>           | EInc Expr
>           | EIsZ Expr
            ....

we are to compute typed terms:

> data Term a where
>     Lit  :: Int -> Term Int
>     Inc  :: Term Int -> Term Int
>     IsZ  :: Term Int -> Term Bool

That is, we need to write a function 

> 	typecheck :: Expr -> Term a

Actually, Greg Buchholz posed a simpler example, of a function my_read
>	my_read :: Expr -> Term a

Although it has the same signature, the intent is different. When the
user writes "my_read exp", the user is supposed to *specify* the type
of the desired result. Just as when we write "read 1", we are supposed
to specify the type of the expected value: Int, Integer, etc. The
function typecheck has a different intent: it *computes* the result
type. It is indeed the typechecker: given the expression, we 
compute its type -- or report a failure if the expression is
ill-typed. That is, the result *type* "Term a" is a function of the
*value* Expr. Thus is truly a problem of dependent types. And Haskell
is up to it: Haskell is genuinely a dependently typed language.

We show the solution that uses no GADTs and no representation types.
We retain however the eval function in the previous message that uses
GADT. Our solution uses type classes. It seems to some the
type-checking rules stated as instances of the TypeCheck class take a
particular natural form. Indeed:

> -- given term e, compute its type t
> class TypeCheck e t | e -> t where
>     typecheck :: e -> Term t

> instance TypeCheck FLit Int where
>     typecheck (FLit x) = Lit x

> instance TypeCheck e Int => TypeCheck (FInc e) Int where
>     typecheck (FInc e) = Inc (typecheck e)

> instance TypeCheck e Int => TypeCheck (FIsZ e) Bool where
>     typecheck (FIsZ e) = IsZ (typecheck e)

> instance (TypeCheck e1 Bool, TypeCheck e2 t, TypeCheck e3 t) 
>     => TypeCheck (FIf e1 e2 e3) t where
>     typecheck (FIf e1 e2 e3) = If (typecheck e1) (typecheck e2)(typecheck e3)

> instance (TypeCheck e1 t1, TypeCheck e2 t2) 
>     => TypeCheck (FPair e1 e2) (t1,t2) where
>     typecheck (FPair e1 e2) = Pair (typecheck e1) (typecheck e2)

> instance TypeCheck e (t1,t2) => TypeCheck (FFst e) t1 where
>     typecheck (FFst e) = Fst (typecheck e)

> instance TypeCheck e (t1,t2) => TypeCheck (FSnd e) t2 where
>     typecheck (FSnd e) = Snd (typecheck e)


In the paper, the IsZ rule would have been written as
	|- e : int
       ---------------
	|- IsZ e : bool

(We don't need the environment Gamma as our language has no
variables). I submit the typeclass notation takes less space. 

The typechecking rules above operate on `lifted' terms: FLit, FInc,
etc:

> newtype FLit = FLit Int
> newtype FInc e = FInc e
> newtype FIsZ e = FIsZ e

rather than the original terms Exp. The conversion is straightforward,
via Template Haskell:

> type F = Q TH.Exp
> parse :: Expr -> F
> parse (ELit x) = [e| FLit $(litE . integerL . fromIntegral $ x) |]
> parse (EInc x) = [e| FInc $(parse x) |]
> parse (EIsZ x) = [e| FIsZ $(parse x) |]

The only inconvenience of using the Template Haskell is the necessity
of splitting the whole code into two modules.

we can then write:

> e1 = "EIf (ELit 1) (ELit 2) (ELit 3)"
> e2 =         "(EIf (EIsZ (ELit 0))          " ++
>              "     (EInc (ELit 1))          " ++
>              "     (EFst (EPair (ELit 42)   " ++
>              "                  (ELit 43))))"
>
> t1' = $(parse . read $ e1)
> t2' = $(parse . read $ e2)

*G> :t t1'
t1' :: FIf FLit FLit FLit
*G> :t t2'
t2' :: FIf (FIsZ FLit) (FInc FLit) (FFst (FPair FLit FLit))

> -- Causes the typechecking error: cannot match Int against the Bool
> -- tt1 = typecheck t1'
> tt2 = typecheck t2'

*G> :t tt2
tt2 :: Term Int

Obviously, e1 is ill-formed and so cannot be typechecked. The term e2
is well-typed, and the typechecker has figured out its type, which is
Term Int. There was no need for any type annotation.

The term tt2 can then be evaluated.

The code: file GP.hs
{-# OPTIONS -fglasgow-exts #-}

module GP where

import Language.Haskell.TH hiding (Exp)
import qualified Language.Haskell.TH as TH (Exp)
import Language.Haskell.TH.Ppr

-- untyped terms, at Level 0
data Expr = ELit Int
	  | EInc Expr
	  | EIsZ Expr
	  | EPair Expr Expr
	  | EIf Expr Expr Expr
	  | EFst Expr
	  | ESnd Expr
	    deriving (Read,Show)

-- Untyped terms, at Level 1
type F = Q TH.Exp
newtype FLit = FLit Int
newtype FInc e = FInc e
newtype FIsZ e = FIsZ e
data FPair e1 e2 = FPair e1 e2
data FIf e1 e2 e3 = FIf e1 e2 e3
newtype FFst e = FFst e
newtype FSnd e = FSnd e

parse :: Expr -> F
parse (ELit x) = [e| FLit $(litE . integerL . fromIntegral $ x) |]
parse (EInc x) = [e| FInc $(parse x) |]
parse (EIsZ x) = [e| FIsZ $(parse x) |]
parse (EFst x) = [e| FFst $(parse x) |]
parse (ESnd x) = [e| FSnd $(parse x) |]
parse (EPair x y) = [e| FPair $(parse x) $(parse y) |]
parse (EIf x y z) = [e| FIf $(parse x) $(parse y) $(parse z) |]


show_code cde = runQ cde >>= putStrLn . pprint

t0 = show_code . parse . read $ "EInc (EInc (ELit 1))"

-- ill-typed expression
e1 = "EIf (ELit 1) (ELit 2) (ELit 3)"
e2 =         "(EIf (EIsZ (ELit 0))          " ++
             "     (EInc (ELit 1))          " ++
             "     (EFst (EPair (ELit 42)   " ++
             "                  (ELit 43))))"

t1 = show_code . parse . read $ e1


File g2.hs
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

module G where

import GP

-- Typed terms
data Term a where
	    Lit  :: Int -> Term Int
	    Inc  :: Term Int -> Term Int
	    IsZ  :: Term Int -> Term Bool
	    If   :: Term Bool -> Term a -> Term a -> Term a
	    Pair :: Term a -> Term b -> Term (a,b)
	    Fst  :: Term (a,b) -> Term a
	    Snd  :: Term (a,b) -> Term b

-- Typed evaluator [elided]

-- Figure out the type of the expression e
-- The type-checking rules are written in the natural notation
[see the TypeCheck class and instances above. Elided to save space]

t0' = $(parse . read $ "EInc (EInc (ELit 1))")
t1' = $(parse . read $ e1)
t2' = $(parse . read $ e2)

tt0 = typecheck t0'
-- Causes the typechecking error: cannot match Int against the Bool
-- tt1 = typecheck t1'
tt2 = typecheck t2'

ttt0 = eval tt0
ttt2 = eval tt2