## Fully Inferable Languages

With the latest release of the Cat language inference of equirecursive function types (in Cat they are called "self" types) is now implemented. This means that in theory (this is not yet proven unfortunately) all valid Cat programs can be inferred. I was wondering what other languages with non-trivial type systems (e.g. they are able to discriminate higher order functions and different arities of functions) also have this property?

## Comment viewing options

### Hindley Milner

It depends what you mean by "valid". In the plain Hindley-Milner type system the straightforward inference algorithms finds the type of any program that can be given valid types. I think this extends to SML, if don't complain about declaring data types and module signatures. On the other hand, most operational definitions like "not actually raising exceptions on any input" pretty trivially reduce to the halting problem.

Hindley-Milner seems to be about as powerful as a type system based on polymorphism can be without requiring some type annotations. I don't know much about systems based intersection types, or subtyping.

### You might find it worth

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.

Even stronger property would be to have (and be able to infer) the principal typing for any term of the language.
HM does not posses this property, for example.

### That's right...

...but Standard ML can!

### Principal Type vs Principal Typings

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

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.

### Even stronger

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

### Slight typo(ing)

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).

### Clarity

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.

### Just maybe

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.