Lambda the Ultimate

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

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

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

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

There's no limit!

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?

Here's a link: System CT.

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

Authors of System CT present translation of their language into ML.

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?

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.

Programming examples needing polymorphic recursion

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

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 π₁ : α × β → α.

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

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

--uhoh!
--y = y' snd


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.

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
caar = twice head

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.

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.

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