[Haskell] Dependent Types in Haskell [was: Eliminating Array Bound
Checking through Non-dependent] types
Martin Sulzmann
sulzmann at comp.nus.edu.sg
Wed Aug 11 00:17:06 EDT 2004
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
More information about the Haskell
mailing list