# Type inference of pair (product) types

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.

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