Update on PiSigma

December 15th, 2008 by Thorsten

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.

2 Responses to “Update on PiSigma”

  1. Luke Palmer Says:

    Hi, I just looked over your paper while considering PiSigma as a core language for my latest project. I have to say that, so far, it looks very attractive. I found the paper understandable and the definitions reasonable and not too abstract, and in particular I love how you handle case expressions by adding equivalences. When I was first getting into dependent types this is what I expected to happen, but was met with disappointment as I discovered the complicated motive construction necessary.

    It might need a few tweaks here and there to fit my purpose — but another attractive thing about PiSigma is that I can understand it well enough to tweak it! :-)

    Thanks for the great work!

  2. Russell O'Connor Says:

    I tried

    test3 : Nat.
    test3 = (\ n -> n) zero.

    but I got the error

    Scopett.hs:(14,18)-(28,93): Non-exhaustive patterns in case

    What’s the deal with not having type annotated variables for lambda terms?

Leave a Reply