Hi Martin Martin Sulzmann wrote:
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.
[..]
We'd like to statically guarantee that the sum of the output list is the sum of the two input lists.
A lovely old chestnut. I think I wrote that program (in Lego plus programming gadgets) back in 1998. [..]
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?]
It's basic stuff. Here's the Epigram source, ab initio, which I knocked up in about 30 seconds (the precise layout is the responsibility of my suboptimal prettyprinter): ---------------------------------------------------------------------- ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) ---------------------------------------------------------------------- ( n, m : Nat ! let !----------------! ! plus n m : Nat ) plus n m <= rec n { plus x m <= case x { plus zero m => m plus (suc n) m => suc (plus n m) } } ---------------------------------------------------------------------- ( X : * ! ! ! ! n : Nat ! ( x : X ; xs : Vec X n ! data !---------! where (--------------! ; !-----------------------! ! Vec X n ! ! vnil : ! ! vcons x xs : ! ! : * ) ! Vec X zero ) ! Vec X (suc n) ) ---------------------------------------------------------------------- ( xs : Vec X n ; ys : Vec X m ! let !----------------------------------! ! vappend xs ys : Vec X (plus n m) ) vappend xs ys <= rec xs { vappend x ys <= case x { vappend vnil ys => ys vappend (vcons x xs) ys => vcons x (vappend xs ys) } } ---------------------------------------------------------------------- These programs were developed interactively: I only had to write the type signatures and the right-hand sides. Under those circumstances, <= rec xs and <= case x are rather less effort than typing the left-hand sides by hand. Moreover they provide guarantees of totality (structural recursion & exhaustiveness of patterns). I'm sorry I can only send this program in black-and-white. The editor uses foreground colour to indicate the status of each identifier and background colour to indicate the typechecker's opinion of each subexpression. You'll notice (or perhaps you won't) that there's rather a lot of type inference going on, both in figuring out indices, and in figuring out which variables should be implicitly quantified. You may also notice the number of fingers I need to lift to convince the machine that the arithmetic condition is satisfied. The definition of plus is sufficient: the marvellous thing about computation is that computers do it. You get partial evaluation for free, but if the constraints require more complex algebra, you have to do the work. Or teach a computer to do the work, hence the project to implement a certified Presburger Arithmetic solver in Epigram: that seems a worthy occupation for the other ten fingers. Or a PhD student.
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.
Not half. See `The view from the left' by myself and James McKinna for a typechecker (for simply-typed lambda-calculus) whose output is the result of checking _its input_. [..]
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.
This observation dates back to Henry Ford: `you can have any colour you like as long as it's black'. In a more technical context, it's certainly a lot older than me. Of course, it's a no-brainer to turn constraint-by-instantiation into constraint-by-equation if you have the right notion of equality. You have to deal somehow with the situation where things of apparently different types must be equal, but where the types will be identified if prior constraints are solved. One approach can be found in my thesis.
To me it seems rather tedious to use (plain) Haskell for dependent types programming.
Absolutely. But the fact that it's to some extent possible suggests that we could, if we put our minds to it, make it less tedious without fundamentally messing up anything under the bonnet. Cheers Conor