patternMinor
Relation between Type Assignment system (TA) and Hindley-Milner system
Viewed 0 times
hindleysystemtypeassignmentbetweenandrelationmilner
Problem
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.
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.
Solution
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.
$$
\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.
Context
StackExchange Computer Science Q#64006, answer score: 9
Revisions (0)
No revisions yet.