[Haskell] Re: Dependent Types in Haskell

2004-08-14 Thread oleg
Martin Sulzmann stated the goal of the append exercise as follows: ] 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. I'd like to give a Haskell implementation of such an append function, wh

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

2004-08-11 Thread 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 i