[Haskell] Re: Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[Conor T McBride]

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