6
$\begingroup$

I'm wondering if there is a way to extend Hinley-Milner's type system to allow polymorphic types without the need of a let construct, by adding an intersection type (as Dan pointed out) that represents the possible types of a function type.

Say I have this expression:

$\lambda x.\lambda y.(x\ (x\ y))$

While running the type inference algorithm, I'd normally, after looking at the expression $(x\ y)$, assign to $x$ some type $Y \rightarrow A$, where $Y$ is the type of $y$ and $A$ is whatever $x$ returns. Then, since $x$ also takes $(x\ y)$ which has the type $A$, I replace $Y$ with $A$, such that the type of $x$ becomes $A \rightarrow A$ and give to the whole thing the type $(A \rightarrow A) \rightarrow (A \rightarrow A)$.

But what if I, instead of replacing $Y$ with $A$ when I see $(x\ (x\ y))$, add a new type to $x$, say, $A \rightarrow B$, such that the final type is $((Y \rightarrow A) \wedge (A \rightarrow B)) \rightarrow (Y \rightarrow B)$, which is also a tautology and seems like a better representation of what the function does.

Now say I give to this abstraction the term $\lambda n.n$ like this:

$(\lambda x.\lambda y.(x\ (x\ y))\ \lambda n.n)$

Since $\lambda n.n$ has the type $N \rightarrow N$, I'd need to unify $N \rightarrow N$ with $((Y \rightarrow A) \wedge (A \rightarrow B))$. So I instantiate two copies of $N \rightarrow N$, say $N_1 \rightarrow N_1$ and $N_2 \rightarrow N_2$, and unify $N_1 \rightarrow N_1$ with $Y \rightarrow A$ and $N_2 \rightarrow N_2$ with $A \rightarrow B$. Because $A$ would be equal to $N_1$ on one side and equal to $N_2$ on the other side, $N_1$, $Y$, $A$ and $B$ are all equal to $N_2$, so the type $Y \rightarrow B$ becomes $N_2 \rightarrow N_2$, which is consistent with the expression you'd get after evaluating the lambda term.

With this type system I should be able to type things like this:

$(\lambda i.\lambda x.\lambda y.((i\ x)\ (i\ y))\ \lambda n.n)$

But these examples are simple, and it becomes a pain to type something like:

$(\lambda x.\lambda y.(x\ (x\ y))\ \lambda x.\lambda y.(x\ (x\ y)))$

I'm having trouble trying to figure out what the actual rules of this system would be, like what would you do if you'd have to unify two intersection types (or whether that situation is even possible).

So my question is, am I moving towards a type system that already exists? If yes, which one? If not, is this because my type system wouldn't meet the requirements of a type system (such as being decidable)?

$\endgroup$
  • $\begingroup$ Those are called intersection types. $\endgroup$ – Dan D. Mar 30 '14 at 9:37
  • $\begingroup$ OCaml supports explicit polymorphic type annotations as an extension. It's different from the intersection type you described. $\endgroup$ – didierc May 14 '14 at 17:16
  • 1
    $\begingroup$ I really think such type inference algorithm is undecidable. Wonder if someone can provide a proof of this. $\endgroup$ – Juan May 17 '14 at 3:52
  • 3
    $\begingroup$ Inferring intersection types is undecidable. This answer gives good information. $\endgroup$ – cody Feb 18 '15 at 17:57
3
$\begingroup$

I am not sure what you mean by type system being decidable. I guess you mean type checking and type inference. (strictly speaking type inference is not a decision problem, although it can be casted as one and people usually think of it that way).

In addition to intersection types, I would also suggest looking at System F where universal quantification does not appear only at the let construct. For system F, type inference is undecidable: paper

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.