dependent-types-talk

Last updated: 2013-08-20 22:50:59 +0000

Upstream URL: git clone http://chriswarbo.net/git/dependent-types-talk.git

Repo

View repository

View issue tracker

Contents of README follows


This repository contains materials from a talk I (Chris Warburton) originally gave at Lambda Lounge Manchester on 19th August 2013.

The talk is an introduction to dependent types, using the dependently-typed language Idris. The files are as follows:

pres.org : Source code of the presentation, an Emacs Org-Mode file pres.pdf : pres.org rendered as PDF (for those without Emacs/Org-Mode) sort.idr : Idris example showing powerful types; namely sorted lists

NOTE: Many implementation details have been left out in sort.idr, using “holes” as type-checkable placeholders. The focus is on the types, and how they might be circumvented, rather than the implementation. Also, it was spotted during the talk that the “Permutation” type defined at the end of sort.idr is not strong enough: it is not sufficient to show that every element of list1 is in list2, since that would make [1, 1, 1, 1, 2, 3] a permutation of [1, 1, 2, 2, 3, 3] (note that they must still have the same length!).