Hi, Inspired by Conor's and Oleg's discussion let's see which dependent types properties can be expressed in Haskell (and extensions). I use a very simple running example.
-- append.hs -- append in Haskell data List a = Nil | Cons a (List a) append :: List a -> List a -> List a append (Cons x xs) ys = Cons x (append xs ys) append Nil ys = Nil We'd like to statically guarantee that the sum of the output list is the sum of the two input lists. In Hongwei Xi's DML or index types a la Christoph Zenger, we can write the following. -- append in DML/index types -- I use a slightly different syntax compared to DML data List a n = Nil where n=0 | Cons a (List a m) where n=m+1 append :: List a l -> List a m -> List a (l+m) append (Cons x xs) ys = Cons x (append xs ys) append Nil ys = Nil Each list carries now some information about its length. The type annotation states that the sum of the output list is the sum of the two input lists. [Conor: I don't know whether in Epigram you can specify the above property?] I like DML/index types but both systems are rather special-purpose. There might be other program properties which cannot be captured by index types. In the latest Chameleon version, we can encode the above DML/index types program as follows. [Side note: I encode dependent types in terms of singleton types] -- append.ch -- Chameleon encoding of append in DML/index types -- encoding of arithmetic data Zero data Succ x -- we introduce a ternary predicate symbol Add l m n -- which models l+m=n -- in my encoding I assume that l and m are given hconstraint Add rule Add l m n, Add l m n' ==> n=n' rule Add Zero m n <==> m=n rule Add (Succ l) m n <==> Add l m n', n=Succ n' -- type indexed data type -- we keep track of the length of the list data List a n = (n= Zero) => Nil | forall m. Add (Succ Zero) m n => Cons a (List a m) append :: Add l m n => List a l -> List a m -> List a n append (Cons x xs) ys = Cons x (append xs ys) append Nil ys = Nil Tim Sheard argues that no predicates other than equality are necessary. Here's an adaptation of a Omega example I found in one of his recent papers. -- append2.ch -- we introduce terms to represent addition data Z data S n data Sum w x y = (w=Z, x=y) => Base | forall m n. (w=S m, y=S n) => Step (Sum m x n) data Seq a n = (n=Z) => Nil | forall m. (n=S m) => Cons a (Seq a m) app :: Sum n m p -> Seq a n -> Seq a m -> Seq a p app Base Nil ys = ys app (Step p) (Cons x xs) ys = Cons x (app p xs ys) Well, now that we have "compiled" away arithmetic, why not get rid of equality? I rely on encoding trick used by Cheney, Hinze, Weirich, Xi and most likely many others. -- append3.hs -- we introduce terms to represent equality data E a b = E (a->b,b->a) -- a silent assumption is that for each monomorphic value E (g,h) -- functions g and h represent the identity -- can't be enforced by Haskell, must be guaranteed by the programmer data Z = Z data S n = S n data Sum w x y = Base (E w Z) (E x y) | forall m n. Step (Sum m x n) (E w (S m)) (E y (S n)) data Seq a n = Nil (E n Z) | forall m. Cons a (Seq a m) (E n (S m)) app :: Sum n m p -> Seq a n -> Seq a m -> Seq a p app (Base (E (g1,h1)) (E (g2,h2))) (Nil (E (g3,h3))) ys = cast2 (E (g2,h2)) ys app (Step p' (E (g1,h1)) (E (g2,h2))) (Cons x xs (E (g3,h3))) ys = Cons x (app p' (cast2 (E (cast1 (g1.h3),cast1 (g3.h1))) xs) ys) (E (g2,h2)) -- some magic, gs, hs and casts refer to term operations to mimic -- type-level equality operations. Note that if we erase all Es, gs, -- hs and casts we obtain append2.ch cast1 :: (S a->S b)->a->b cast1 f a = let S b = f (S a) in b cast2 :: E m p -> Seq a m -> Seq a p cast2 (E (g1,h1)) (Nil (E (g2,h2))) = (Nil (E (g2.h1, g1.h2))) cast2 (E (g1,h1)) (Cons x xs (E (g2,h2))) = (Cons x xs (E (g2.h1,g1.h2))) Conclusion: Note that append3.hs runs under Haskell. append2.ch runs under Omega, Haskell extension with generalized data types and Chameleon (note that append2.ch uses Chameleon syntax for data type definitions!). append.ch runs under Chameleon. To me it seems rather tedious to use (plain) Haskell for dependent types programming. Martin _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell