## The HM system does not have principal typings for all terms

...so do not all the PLs based on it, do they? Which systems do have them? Read on:

This paper presents a new general definition of principal typings which does not depend on the details of any particular type system. This paper shows that the new general definition correctly generalizes previous system-dependent definitions. This paper explains why the new definition is the right one. Furthermore, the new definition is used to prove that certain polymorphic type systems using for all-quantifiers, namely System F and the Hindley/Milner system, do not have principal typings.
Am I just overly enthusiastic of finding a new source of interesting reading, or are these 12 pages really a worth reading for anybody designing a new PL?

## Comment viewing options

...a previous reference to Jim's paper on LtU (the link there is broken :-().

### "What are principal typings and what are they good for?"

If you feel intrigued by the previous paper, you might enjoy this one:

We demonstrate the pragmatic value of the principal typing property, a property distinct from ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection types and is closely related to ML. Its principal typing property provides elegant support for separate compilation, including â€œsmartest recompilation'' and incremental type inference, and for accurate type error messages. Moreover, it motivates a new rule for typing recursive definitions that can type some interesting examples of polymorphic recursion.
By Trevor Jim.

### A Polar Type System

A Polar Type System
An extension of P2 promised in the previous Jim's paper.

### Polar type inference with intersection types and omega

Polar type inference with intersection types and omega

We present a type system featuring intersection types and omega, a type constant which is assigned to unused terms. We exploit and extend the technology of expansion variables from the recently developed System I, with which we believe our system shares many interesting properties, such as strong normalization, principal typings, and compositional analysis. Our presentation emphasizes a polarity discipline and shows its benefits. We syntactically distinguish positive and negative types, and give them different interpretations. We take the point of view that the interpretation of a type is intrinsic to it, and should not change implicitly when it appears at the opposite polarity. Our system is the result of a process which started with an extension of Trevor Jim's Polar Type System.

I seem to approach a limit of posts per day... Just could not help... Besides, it's just a forum topic, not a story :-)

### Yes, this is an important result

Simple, useful, idea that more people should be aware of. It should be a story, I think.

### All of them?

If we create a story, I personally prefer the "What are principal typings and what are they good for?" paper as a foundational one. Carlier's results are more impressive and up to date, though (but lacking any proofs - I still have to check http://www.macs.hw.ac.uk/~sebc/ for latest papers).

### This one, I think

I guess the striking result is the best way of leading a front-page story.

### Go for it

There's no limit!

### Jim Trevor's type system

I had a quick glance over Jim Trevor's papers (now planning to dive deeper) and found no translation mechanism for languages with his type system into something useful. I think it is great omission.

### found no translation mechan

found no translation mechanism for languages with his type system into something useful.

Do you mean presenting inferred typings in a more user-friendly manner?

### I compare it to system CT

Authors of System CT present translation of their language into ML. I expected something along those lines in Jim Trevor's work.

### Confused

Authors of System CT present translation of their language into ML.
I feel lost. Jim did not define a language, neither did the authors of System CT (as far as I can tell). They defined type systems for basically the same language. It is not uncommon in type theory to have two type systems that type exactly the same set of programs (meaning they type the same language), but differ in "non-functional" (cliche from business world) respects: existence of principle typings being one of them.

I agree that seeing more practical examples in Jim papers would be nice, if that's what you meant. Otherwise I am confused.

BTW, is Jim his first or last name?

### What are the types, anyway

As far as I can recall, types are interconnected with underlying semantics of programming language. Semantics describe how calculation goes and types ensure that well-typed program cannot go wrong (with respect to the semantics).

System CT is connected, albeit through translation and somewhat informally because of this, with semantics of ML. Trevor's (or Jim's) work is not.

And, of course, I also like to see more practical examples.

### Will need to search later

Semantics describe how calculation goes and types ensure that well-typed program cannot go wrong (with respect to the semantics).

This does not contradict my point that there may be multiple (in fact, infinitely many) type systems for the same language. This means it's possible to have multiple principal typings for the same program (one or less principal typing per type system). And often intersection-based type systems are applied to the same language as quantifier-based type systems - to some variant of lambda calculus. I therefore see no need for translation between languages (people who know ML should know lambda calculus anyway, right?), though examples of translation between inferred typings of different systems for the same program are, of course, useful. And in fact I remember some papers in the thread showing them side by side. I have to search them later, and will provide quotations.

### Comparing System S to HM&forall;

Ah, I didn't post this reference before, mea culpa.

Check section 3 onwards for examples of types inferred by SML/NJ, GHC, HM and System S.

My favorite is:

System S:

map1 : ((int list â†’ int) â†’ int list list â†’ int list) âˆ§ ((int list â†’ int list) â†’ int list list â†’ int list list)
map2 : (((int list â†’ int) â†’ int list list â†’ int list) âˆ§ ((int list â†’ int list) â†’ int list list â†’ int list list)) â†’ int list list â†’ int list list

SML:

Error: operator and operand donâ€™t agree [circularity] operator domain: â€™Z list -> â€™Z operand: â€™Z list -> â€™Z list in expression: f tl

### You can't do that with System F

One example that helped me understand what intersection type systems can do that others can't is λf.λx. f (f x).

HM and System F type this as (α → α) → α → &alpha, which means we can't pass it a function like π1 : α × β → α.

Using intersection types, we get (α → β ∧ β → γ) → α → γ. Using this system, we can type (λf.λx. f (f x)) π1 : (α × β) × γ → α.

The paper mentions that all examples typable in S are typable with higher-rank polymorphism, but I don't see it here.

y' :: (forall b c. f b c -> b) -> f (f a d) e -> a y' g = g . g

 f = y' fst 

--uhoh! --y = y' snd 

### I don't think so

I think the paper only claimed that the examples it provided were typeable with higher-rank polymorphism.

Here's a variation that might be clearer: Given head : List α → α, we can type (λf.λx. f (f x)) head : List (List α) → α in a system with intersection types, but not in Fω (so far as I know).

We can write, however,
 y :: (forall b . f b -> b) -> f (f a) -> a y f = f . f

 

caar :: [[a]] -> a caar = y hd 
I don't think I understand your example.

### It's less general

In a system with intersection types, if I declare:

twice :: (a -> b ∧ b -> c) -> a -> b
twice f = f . f


Then I can write:

caar :: [[a]] -> a

fst2 :: ((a,b),c) -> a
fst2 = twice fst

snd2 :: (a,(b,c)) -> c
snd2 = twice snd


I can even do:

fourtimes :: (a -> b ∧ b -> c ∧ c -> d ∧ d -> e) -> a -> e
fourtimes = twice twice


There's an on-line type inferencer for System E. I entered (\f x -> f (f x)) (\g y -> g (g y)), and it produced essentially the type I wrote above for fourtimes.

### But must it be?

The type given by the E inferencer is certainly more general than the one I give for y. What we want for the y I gave is a whole class of types. Is there some way we can unify them using Haskell's classes? I mention these because I thought they were syntax for some existing part of Fomega.

### Jim provided some examples as well

Also, Table 1 in "A Polar Type System" has three lambda calculus terms typed in System P, ML, and System I2.