\a.aa

I notice that SML 98 and F# can't infer the type (e.g. let M a = a a ).
What languages can infer the type? What language features are required
to express the type?

Why don't the type systems to those languages simply output something
like:

M : 'a.('a -> 'b) -> 'b

Mark.

type intlist = Cons of int * intlist | Nil

and need explicit conversions between the types (fold/unfold) by
constructing (Cons 4 Nil) and deconstructing
(match l1 with Cons _ l2).

There is a chapter comparing the two in TaPL and some more
details are available in [1].

Benedikt

   forall b. (forall a. a -> b) -> b

This is indeed (one) possible solution, but with its nested quantifier,
it is a so-called higher-rank polymorphic type. Plain ML does not allow
such types, because type inference for them is undecidable in general.
Some extensions to ML - i.e. Le Botlan/Remy's MLF, or Haskell with GHC
extensions - allow it if you supply sufficient type annotations. But the
meta-theory of such extensions is pretty involved, and more or less an
open research area.

Plain ML only supports prenex polymorphism, where all quantifiers are in
front. This is said to hit a "sweet spot" in type system design, because
it is expressive enough for most practical problems but still allows
complete type inference.

To type self application of an argument x in that system, you have to
solve the type equation

   a = a->a'

To see why, assume x:t for some type t.
Because we apply something to x, we know t=t1->t2.
And because the argument also has type t, we need t1=t, i.e. t1=t1->t2.

The only solution is a recursive type, a fixed point of the above
equation. Usually this is written mu a.a->a'.

Such so-called equi-recursive types are not hard to add to ML, but the
thing is: You Do Not Want Them. Just recently, Andrew Bromage gave a
nice illustration why, on the Haskell-Cafe list:

http://www.haskell.org/pipermail/haskell-cafe/2006-December/020074.html

OCaml used to have recursive type inference in its very first versions,
but it was quickly banned to an explicit switch by popular demand.
Whenever you really need recursive types in ML, you can always express
them by explicit wrapping into an auxiliary algebraic datatype.

I have a perhaps naive inquiry given my new understanding: would you
destabilize a type-system if you pulled the qualifier to the front and
expressed the type using an overly general type? e.g. instead of

  forall b. (forall a. a -> b) -> b

?

Also is the first solution not Rank-2 polymorphism? Pierce says in the
TaPL that rank-2 polymorphism is in fact decidable and rank-3 and
higher polymorphism is undecidable. Is the type inference of rank-2
polymorphism particularly hard I wonder? It seems to me that detecting
cylcical constraints should be relatively easy for a type inference
algorithm.

Anyway, thanks again for your help.

On Dec 21, 7:12 pm, Benedikt Schmidt <besc...@cloaked.de> wrote:

You can read forall in the same way as you read an arrow: it stands for
an argument, though a type, not a term argument. Considering that, the
difference between the two types above is analogous to the difference
between function types

  c -> (d -> a -> b) -> b

and

  c -> d -> (a -> b) -> b

You have inverted the roles of the function and its caller regarding
argument d, i.e. who is allowed to chose it. Same for type a above.