8
$\begingroup$

Recently I started my studies in type theory/type systems and Lambda Calculus.

I have already read about Simple Typed Lambda Calculus in Church and Curry style. The last one is also known as Type Assignment system (TA).

I'm thinking about the relations between TA and Hindley-Milner (HM), the system in languages like ML and Haskell.

The book Lambda-Calculus and Combinators: An Introduction (Hindley) says that TA is polymorphic (pag. 119). Is that the same sense of polymorphism in systems like HM and System-F?

TA is said to have the strong normalisation property, so is not turing complete. Languages that use HM system are turing complete, Haskell for example. So must be the case that HM system allows terms like the infinity loop $\Omega$ to receive a type. Is that correct or I'm missing something?

Any way, I would like to know the relation between TA and HM.

|cite|improve this question|||||
$\endgroup$
  • 1
    $\begingroup$ I've never heard of Typed Assignment system before. I googled it, and got this question as the third answer, which means it must be very niche. Can you explain what it is? Also, what's an "infinity loop"? Do you mean a non-halting computation? $\endgroup$ – gardenhead Sep 28 '16 at 16:48
  • $\begingroup$ Type Assignment is a version of the Simple Typed Lambda Calculus created by Curry. You should look for that in mentioned book. And yes, $\Omega$ is the default infinity loop $\lambda$ calculus or the non-halting program. $\endgroup$ – Rafael Castro Sep 28 '16 at 17:35
  • $\begingroup$ I think I should ask this question in some other more theoretical/mathematical stackexchange. Should I? $\endgroup$ – Rafael Castro Sep 28 '16 at 17:37
  • $\begingroup$ You could try. Give cstheory and mathoverflow a shot. However, you said you "recently started your studies", so I would be surprised if your question was that advanced. I think you're just using uncommon terminology to describe simple concepts (could be wrong though). For example, the infinity loop is usually called the bottom type (if I understand you correctly). $\endgroup$ – gardenhead Sep 28 '16 at 17:54
  • 1
    $\begingroup$ Definitely my question is not in research level. My question is more like "hey, I'm understanding this basics concepts right?". But I will try, maybe I get a answer. $\endgroup$ – Rafael Castro Sep 28 '16 at 18:23
9
$\begingroup$

System F and its subsystem HM have a type former for universal quantification:

$$ \tau \quad::=\quad \forall x.\tau \ |\ ... $$

which the system in Hindley/Seldin doesn't have. That is the key difference.

Now System F doesn't have decidable type-inference, and HM is a way of combining type-inference with reasonably expressive parametric polymorphism. HM achieves this by allowing only outermost universal quantification, i.e. all types are of the form

$$ \forall x_1 \forall x_2 ... \forall x_n.\tau $$

where $\tau$ is quantifier free (and $n \geq 0$). HM gives a rule system that ensures that only programs that can be typed in this way are admissible. This is achieved by "let-polymorphism". The system in Hindley/Seldin doesn't do any of that. Later, in Chapter 13, Hindley/Seldin introduce pure type systems (PTS), of which System F is a special case. I'm not sure if HM can be expressed as a PTS.

The question of strong normalisation is orthogonal. System F and HM are strongly normalising, but that can easily be remedied by introducing fix-point combinators or similar. The paper Principal type-schemes for functional programs by L. Damas and R. Milner even states this: "For example, recursion is omitted since it can be introduced by simply adding the polymorphic fixed-point operator ..." The introduction of fixpoints, making the system Turing complete, poses no issues from the point of view of type inference.

|cite|improve this answer|||||
$\endgroup$
  • $\begingroup$ Would be correct to think HM = TA + "let-polymorphism"? The book Lambda-Calculus and Combinators (Hindley), so far, said nothing about universal quantification on types. TA uses type variables, but I don't know anything about the range of these types. To be clear, I haven't studied the HM system yet, but I know what's used for. $\endgroup$ – Rafael Castro Sep 28 '16 at 20:02
  • $\begingroup$ @RafaelCastro If you squint ... If you have a CS background, Pierce's TAPL book is probably a much more accessible explanation of HM, and typing systems in general. The Damas/Milner paper I referenced is very easy to read, if you can see past the old-fashined type-setting. I give it to my beginning PhD students. Give it a read! Hindley/Seldin is a bit on the formal side. $\endgroup$ – Martin Berger Sep 29 '16 at 10:32
  • $\begingroup$ @RafaelCastro Type variables range over types. All types. This is why System F is impredicative. $\endgroup$ – Martin Berger Sep 29 '16 at 10:47
  • $\begingroup$ Thank you. Yes, I'm an undergraduate student in CS, so I will try Pierce's TAPL book. $\endgroup$ – Rafael Castro Sep 29 '16 at 12:37
  • $\begingroup$ @RafaelCastro There is probably no better way of learning about types than reading TAPL and implementing the typing systems that are discussed there. $\endgroup$ – Martin Berger Sep 29 '16 at 16:17

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.