On Fri, Dec 23, 2005 at 12:10:07PM +0100, Tomasz Zielonka wrote:

On Fri, Dec 23, 2005 at 03:34:40AM -0000, oleg@pobox.com wrote:

...

[Sorry for possible duplication, our DNS server seems to be broken, and the sysadm is on vacation]

I don't think that is the problem with GADTs. The following works

...

untype :: Term f a -> Term Untyped () untype (Lit x) = Lit x untype (Succ t) = Succ (untype t) untype (IsZero t) = IsZero ((untype t)::Term Untyped ()) untype (If c t e) = If ((untype c)::Term Untyped ()) ((untype t)::Term Untyped ()) ((untype e)::Term Untyped ())

I just checked that the only required change is the one in type signature. But I can't explain it at this moment.

I tried to implement another function: mapChildren :: (forall a. Term f a -> Term f a) -> Term f b -> Term f b mapChildren fun 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) It is supposed to be similar to gmapT from Data.Generics - apply 'fun' to every immediate Expr child of the node. Unfortunately, I don't know how to make it compile. I tried a couple of different type signatures. Best regards Tomasz -- I am searching for a programmer who is good at least in some of [Haskell, ML, C++, Linux, FreeBSD, math] for work in Warsaw, Poland

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'

On 12/27/05, oleg@pobox.com <oleg@pobox.com> wrote:

data a :+: bb -- Conj assertion a and assertions bb data aa :@: bb -- Conjunction of assertions aa and bb

Why is the difference here?

class WellTyped a instance WellTyped Nil instance WellTyped cs => WellTyped ((a :=: a) :+: cs) instance (WellTyped cs1, WellTyped cs2) => WellTyped (cs1 :@: cs2)

Could one not write: instance WellTyped (a :=: a) and do away with (:+:)? -- Taral <taralx@gmail.com> "Computer science is no more about computers than astronomy is about telescopes." -- Edsger Dijkstra