[Haskell] Conditional typechecking with GADTs
oleg at pobox.com
oleg at pobox.com
Tue Dec 27 23:07:39 EST 2005
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'
More information about the Haskell
mailing list