First Epigram meeting of the New Year saw all of the above, and in an attempt to get as many of the faces in a position to hack Epigram2. We started at the start. By the end of the hour the black-board carried a (PTS) fragment of the new representation of terms that separates into two syntactic categories — the types that have types that can be inferred and the types that can only be checked in a known type:
Simply typed programs have seen the distinction between Church- or Currystyle lambda expressions (although probably not in *one* program), but the first seem not to have been needed so much as this here for dependent types.
Since typings may involve computations: It now looks as if λ’s now not only got /body’s/ but also /heads/.