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.