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

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.


comments powered by Disqus