Nottingham FP Lab Blog

Update on PiSigma

by Thorsten on December 15, 2008.
Tagged as: Lunches.

Last Friday I gave an update on $\Pi\Sigma$ a dependently typed core language which Nicolas Oury and I are working on. We wrote a paper (you can also play with it) earlier this year which didn’t make it into ICFP and have revised the language definition considerably. Basically we got rid of some features (namely constraints) which were – in our view – to clever for a core language.

$\Pi\Sigma$ is a core language, hence the emphasis is on small leaving out lots of syntactic sugar which makes languages like Coq’s CIC, Agda, Epigram or Cayenne actually usable. The idea is that these features can be recovered by a syntactic translation (or elaboration as we say) as part of the compiler. Having a small core langauge is nice for compiler writers but also for theoretical analysis. The aim here is similar as Fc for Haskell but directed at dependent functional programming.

Unlike most of the DTP languages mentioned above, with the exception of Cayenne, $\Pi\Sigma$ is partial, i.e. programs may fail to terminate. On the other hand it is full blown, which means that type-checking is partial too. We think this isn’t such a big issue for programming if the only reason for the type checker to diverge is that you have anon-terminating expression within a type. On the other hand it is an issue for using $\Pi\Sigma$ for verification and it also rules out important optimisations. Hence we plan to define a total fragment but we think it is a good idea to specify the partial language first. Indeed, even when using Agda (or Epigram) we find it often more convenient to start developing in a non-total langauge and address the totality issue later (or never, depending on demand).

Here is a summary of the essential features of $\Pi\Sigma$

Very few type formers : $\Pi$ types, $\Sigma$ -types , Type:Type, finite types (enumerations) as sets of labels, lifted types for recursion and coinduction.
Depedently typed pattern matching can be derived using the primitive eliminator and equality
Full recursion via let rec (mutual) , used to define recursive types (like Nat) and recursive values. Recursion is controlled via lifted types and boxes.
Inductive families can be encoded using an extensional equality
Coinductive types and families can be encoded using lifted types, overcoming some issues present in Agda and CIC

Currently we are working on a new implementation and on a revised language definition. I’ll put this up as soon as it is in a reasonable state.