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
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