[Haskell] Conditional typechecking with GADTs

[oleg at pobox.com]

Tomasz Zielonka wrote:
> The papers on GADTs have an example showing how you can transform,
> traverse and evaluate ASTs (or terms) with more type safety. I've
> used such an approach in one of my applications and it works remarkably
> well.
>
> However, I would like to be able to "turn off" that type-safety
> in some parts of code, for example to separate parsing from typing.
> I thought I found a way to do this, because I was able to create Typed
> (with all consistency checking) and Untyped (without consistency
> checking) terms. Unfortunately I seem to be unable to write any useful
> function on such terms - GHC complains that there are type errors.

The present message shows what seems to be a more fruitful approach to
writing terms whose typechecking can be `postponed', perhaps
indefinitely. The approach tries to play to the strengths of GADTs and
avoid their weaknesses. The key is the accumulation of constraints. The term
|Term cs a| is a term whose type is |a| _provided_ all
pre-conditions in the list |cs| are satisfied. That is, instead of
producing a ``well-typed'' term, we produce a term with a list of
preconditions. If all pre-conditions (which are of the form of type
equality) are indeed satisfied, the term is well-typed. We may chose
to test for that at any point in the computation. The test is static,
of course. We may chose to process a term regardless of its
pre-conditions (that is, if we elected not to care about the term
being well-typed).

Here's the example: the term

ex1 =
    If  (IsZero (Succ (Lit 0)))
        (Lit 1)
        (Lit 2)

has the type

*T> :t ex1
ex1 :: Term ((:+:) ((:=:) Int Int)
		   ((:+:) ((:=:) Bool Bool)
			  ((:@:) ((:@:) ((:+:) ((:=:) Int Int) ((:+:) ((:=:) Int Int) Nil))
					Nil)
				 Nil)))
	    Int

and the definition
	ex1' = well'typed'is ex1

types (meaning that the term is assuredly well-typed). OTH, when we
try to do the same for

ex2 =
    If  (IsZero (Succ (Lit 0)))
        (Lit 1)
        (IsZero (Lit 2))
ex2' = well'typed'is ex2

we get:

/tmp/t1.hs:45:7:
    No instance for (WellTyped ((:+:) ((:=:) Int Bool)
				      ((:+:) ((:=:) Bool Bool)
					     ((:@:) ((:@:) ((:+:) ((:=:) Int Int) ((:+:) ((:=:) Int Int) Nil)) Nil)
						    ((:+:) ((:=:) Int Int) Nil)))))
      arising from use of `well'typed'is' at /tmp/t1.hs:45:7-19

As we can see, we could hardly expect the pre-condition ((:=:) Int Bool)
to be satisfied. One might wish for GHC to print out type lists
prettier...


Here's the complete code

{-# OPTIONS -fglasgow-exts #-}

module T where

data Nil
data a  :=: b				-- Assertion that a equals b
data a  :+: bb				-- Conj assertion a and assertions bb
data aa :@: bb				-- Conjunction of assertions aa and bb

-- Type variable cs is the list of pre-conditions for the term to be
-- well-typed (that is, cs is \Gamma, the assumptions)

data Term cs a where
    Lit     :: Int -> Term Nil Int
    Succ    :: Term cs int -> Term ((int :=: Int) :+: cs) Int
    IsZero  :: Term cs int -> Term ((int :=: Int) :+: cs) Bool
    If      :: Term cs1 bool -> Term cs2 a2 -> Term cs3 a3 -> 
	       Term ((a2 :=: a3) :+: ((bool :=: Bool) :+: 
		     (cs1 :@: cs2 :@: cs3)))
		    a2


ex1 =
    If  (IsZero (Succ (Lit 0)))
        (Lit 1)
        (Lit 2)

-- This type constraints verifies that all pre-conditions are satisfied.
class WellTyped a
instance WellTyped Nil
instance WellTyped cs => WellTyped ((a :=: a) :+: cs)
instance (WellTyped cs1, WellTyped cs2) => WellTyped (cs1 :@: cs2)

well'typed'is :: WellTyped cs => Term cs a -> Term cs a
well'typed'is = id

ex1' = well'typed'is ex1

ex2 =
    If  (IsZero (Succ (Lit 0)))
        (Lit 1)
        (IsZero (Lit 2))

-- That is not well-typed
-- ex2' = well'typed'is ex2


mapChildren :: (forall f a. Term f a -> Term f a) -> Term f b -> Term f b
mapChildren _ t@(Lit x) = t
mapChildren fun (IsZero t) = IsZero (fun t)
mapChildren fun (Succ t) = Succ (fun t)
mapChildren fun (If c t e) = If (fun c) (fun t) (fun e)


showt :: Term f a -> String
showt (Lit x) = show x
showt (Succ x) = "(S " ++ (showt x) ++ ")"
showt (IsZero x) = "(Z? " ++ (showt x) ++ ")"
showt (If t c a) = unwords ["(If",showt t, showt c, showt a, ")"]

-- Ralf's famous example: incrementing the salary
inct :: Term f a -> Term f a
inct (Lit x)  = Lit (x+1)
inct x        = x

testm = showt $ mapChildren inct ex1'