Lambda the Ultimate

You might find it worth reading up on HM(X) as a generalisation of Hindley-Milner - there are certainly some directions you can push it in.

...but Standard ML can!

I started going through the principal typing papers and I find I am struglling to grasp the implications of the distinction made in http://www.church-project.org/reports/electronic/Jim:MIT-LCS-1995-532.pdf between:

Principal Type Property:
Given a term M typable in a type environment A, there exists a type t that representing all possible types for M in A.

Principal Typing Property:
Given a typable term M, there exists a judgement A |- M : t representing all possible typings of M.

I don't know whether Cat has the principal typing property or not. Any hints on how we can identify languages without this property? There are some clues with regards to the description of the principal typing property in the linked paper that suggest Cat indeed has this property. The Cat type system for example is compositional:

Consider:

  define f { [a b c] }
  define g { [a b] [c] compose }
  define h { [a] [b c] compose }

The types of "f", "g" and "h" are the same.

A typing is a derivation/proof of a term's type. If there's a principal typing, it subsumes all other ways of proving that the term in question has the relevant type.

A principal typing subsumes all other ways of proving that the term in question has any type.

Principal Typing Property in fact should read:
Given a typable term M, there exists a typing A |- M : t representing all possible typings of M.

Where inference of principal type gives you a type t given both A and M, inference of principal typing gives you both A and t, given M.

These properties almost coincide for closed terms (programs), but otherwise inference of typings is more powerful (and probably useful).

I've made the fix. Looking at: http://www.macs.hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typings:slightly-longer.pdf I see that they use the word "judgement" where you use "typing". I assume the terms are fully interchangeable?

Where inference of principal type gives you a type t given both A and M, inference of principal typing gives you both A and t, given M.

Nice, now that is something I can get my head around! Thanks for the clarification.

So then Cat clearly does infer principal typings.

So then Cat clearly does infer principal typings.

I am not an expert, so take this with a grain of salt - the fact that you have (meta)function of (meta)type CatTerm -> CatEnvironmentAssumptions x CatType does not mean it infers principal typings of Cat terms.

It does not even mean Cat type system has principal typings.
This existence or absence of principal typings can be proven for a type system ignoring the implementation. Then you could prove that specific function indeed calculates what you proved to be principal typing for the type system.