Dependently Typed Programming

Conor's materials

Lecture 1

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 vector and matrix part of the lecture.
• The filing monad demo.
• Just to show that the filing monad makes you check.

The slides are here, now that I've photographed them.

Further reading:

• Applicative programming with effects (McBride, Paterson)
• The essence of the ITERATOR pattern (Gibbons, Oliveira)

Lecture 2

Agda basics: some vectors, at a less crazy pace; some examples of improved hygiene; views; simply typed lambda calculus.

• The starting configuration of the file, so you can try to redo the lecture yourself!
• My crib for the finished product.

Humourless Marxism alert: there's quite a lot of boilerplate here. Hopefully, on Friday, we'll see the method in this madness.

Further reading:

• The view from the left (McBride, McKinna)

Lecture 3

...was the back end of lecture 2.

Lecture 4

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

---

Last modified: Fri Jun 25 21:33:44 BST 2010