This is basically a magic show, more about sketching the
possibilities which advanced type systems open, than about
communicating technical material. At the same time, it's a
demo of the
Strathclyde
Haskell Enhancement. If you have Haskell (and cabal), you can try
this kit with cabal install she
.
The slides are here, now that I've photographed them.
Further reading:
Agda basics: some vectors, at a less crazy pace; some examples of improved hygiene; views; simply typed lambda calculus.
Humourless Marxism alert: there's quite a lot of boilerplate here. Hopefully, on Friday, we'll see the method in this madness.
Further reading:
...was the back end of lecture 2.
Universes, Ornaments, Algebras is based on my unfinshed draft Ornamental Algebras, Algebraic Ornaments. It's an exploration of incremental design of datatypes.
Starting Configuration | Crib file |
L4Basics.agda | |
L4Desc.agda | L4DescCrib.agda |
L4Nat.agda | L4NatCrib.agda |
L4Orn.agda | L4OrnCrib.agda |
L4List.agda | L4ListCrib.agda |
L4AlgOrn.agda | L4AlgOrnCrib.agda |
L4Le.agda | |
L4Vec.agda | L4VecCrib.agda |
L4Hutton.agda | L4HuttonCrib.agda |