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.