Gabriel439/Haskell-Morte-Library — pull request #2 by Gabriel439 (2014-11-27 06:00:06+00:00)
Title: First draft of DeBruijn indices and substitution

This is my first draft of using DeBruijn-like indices for efficient substitution as part of work on issue #1. This is not quite the same as the original proposal because I'm trying to preserve names and reduce the number of explicit index annotations, so it's highly like to have mistakes.

I think substitution and normalization work correctly, but type-checking still fails in certain cases. The following example which used to successfully type-check now fails to type-check (but still normalizes correctly if you skip type-checking). I believe the issue is due to the fact that the context is not updated to reflect changes in variable indices when normalizing expressions:

```
-- mapcomp2.mt

( \(List : * -> *)
-> \(map : forall (a : *) -> forall (b : *) -> (a -> b) -> List a -> List b)
-> \( (.)
: forall (a : *)
-> forall (b : *)
-> forall (c : *)
-> (b -> c)
-> (a -> b)
-> (a -> c)
)
-> \(a : *)
-> \(b : *)
-> \(c : *)
-> \(f : b -> c)
-> \(g : a -> b)
-> (.) (List a) (List b) (List c) (map b c f) (map a b g)
)

-- List
(\(a : *) -> forall (x : *) -> (a -> x -> x) -> x -> x)

-- map
( \(a : *)
-> \(b : *)
-> \(f : a -> b)
-> \(l : forall (x : *) -> (a -> x -> x) -> x -> x)
-> \(x : *)
-> \(Cons : b -> x -> x)
-> \(Nil: x)
-> l x (\(va : a) -> \(vx : x) -> Cons (f va) vx) Nil
)

-- (.)
( \(a : *)
-> \(b : *)
-> \(c : *)
-> \(f : b -> c)
-> \(g : a -> b)
-> \(va : a)
-> f (g va)
)
```