Type inference of pair (product) types

Question

I am looking into Hindler-Milney type system and I am trying to add support for the pair type. In Pierces book, he introduces special language constructs for creation of pairs and getting their elements.

What I am interested in is the following. What if I don't introduce new constructs, yet use special functions with this signatures:

$$pair: \alpha \rightarrow \beta \rightarrow \alpha \times \beta $$

$$proj1: \alpha \times \beta \rightarrow \alpha$$

$$proj2: \alpha \times \beta \rightarrow \beta $$

If I use Wand's algorithm for type inference, after collecting all equations between type expressions and solving it a bit, I get the following equation for $((pair\; 2\;) 4): \tau$:

$$\alpha \rightarrow \beta \rightarrow \alpha \times \beta = Int \rightarrow Int \rightarrow \tau$$

It seems to me that the unification algorithm should infer at the end that $\tau = Int \times Int$. Is this true?

Do I really need a special construct for pairs? Is there something conceptually wrong with this? Probably their is, so it would be great if someone could point me out.

Note that I would also prefer using special constructs as that way looks cleaner and easier to program with; this question is just for my complete understanding of the subject.

Answer 1

You can use things like pair, proj ... as constants only. That works very well conceptually. Nevertheless, there are reasons why programming languages tend to use special syntactic forms for the like of products:

• Readability, e.g. ( M, N ) reads more natural than pair M N to some.

• For efficient reductions. It is possible to code the reductions for pairs up in pure$\lambda$-calculus, but that's usually not as efficient.

• Finally, you'd need a polymorphic typing system for this to work.

As an aside, the formalisation of logics in interactive proof assistants like Isabelle is based on a similar idea, called logical frameworks.