3 ms·

Hindley-Milner (never seen it written as M-H) is beautiful because it's an elegant extension of simply-typed lambda calculus (STLC) that brings a very useful tr

by emillon 13y ago

Hindley-Milner (never seen it written as M-H) is beautiful because it's an elegant extension of simply-typed lambda calculus (STLC) that brings a very useful trait, polymorphism. Here the first 3 rules are those of STLC. The magic happens in [Gen] and [Inst]: namely, you can generalize free type variables. If you have a function that works on lists of elements of type t when there is no constraint on t, they can work on any lists of any type. This brings quantification to the type system, ie you go from: ∀ a. reverse : α list → α list to reverse : ∀ α. α list → α list (in the first one, ∀ is part of the discourse, and in the second one, part of the type). [Inst] states that you can replace a quantified variable by any variable. This is the role of the ⊑ operator, which is unfortunately not explained in this notation. This is confusing for people not used to type systems, ie most people). Technically, [Let] is redundant because it is a combination of [App]+[Abs] : let x = e1 in e2 is equivalent to (λx.e2) e1. There is a difference in the ML branch of languages (as opposed to the Haskell branch) because in the presence of memory references (mutable cells) you can't generalize everywhere, so only let-bound variables are given a type scheme σ (both in the let...in construct and in toplevel phrases). That's why there is usually an explicit generalisation step at this point. Or maybe I have overlooked this particular presentation. HTH

benbataille 13y ago
> Technically, [Let] is redundant because it is a combination of [App]+[Abs] : let x = e1 in e2 is equivalent to (λx.e2) e1. This equivalence does not hold in the HM formalisation. It's well explained in the Wikipedia article : http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism [Abs] is monomorphic while [Let] is polymorphic. Using the Wikipedia article exemple : \f.(f true, f 0) will not be typed while let f = \x.x in (f true, f 0) will be reduced to (bool, int).
- groovy2shoes 13y ago
  Does the nonequivalence have something to do with ML's value restriction?
  - emillon 13y ago
    Yes. For example, if you generalize reference values, you can type ref [] as ∀a. (a list) ref, then store [4] to it, then retrieve a float from the head of the stored list, thus breaking the type system. It is a bit similar to array type variance problem that struck Java. One solution is to distinguish between syntactic forms that may allocate memory (eg, function applications) and the ones that can not (eg, abstractions, constants, variables), and only generalize the latter ones. (Operationally speaking, the two forms (let and abs+app) are always equivalent, though).
    - groovy2shoes 13y ago
      Thank you, that was a much more detailed response than I was expecting. Would it be correct to assume, then, that a pure ML would allow HM to be trivially modified to support the equivalence?
  - benbataille 13y ago
    No, this nonequivalence applies directly to the typing of the lambda-calculus which was the topic of the original papers by Hindley and proven by Damas. On the contrary, the value restriction is a part of the extended rules used for the typing of ML. It was introduced because ML isn't pure, it supports references. The value restriction is there to prevent them having polymorphic type. The rule is simple : syntactic values are the only things receiving a polymorphic type. What is a syntactic value ? To quote Geoffrey Smith notes on SML97 "Basically, a syntactic value is an expression that can be evaluated without doing any computation". All this iss done in order to ensure type safety. Actually, if references could have a polymorphic type, the type system would accept incorrect programs such as : let r : 'a list ref = ref [] let r1 : int list ref = r let r2 : string list ref = r r2 := "a" let v : int = 1 + !r1 Which does not work because r, r1 and r2 are references to the same value. Value restriction is a bit overkill. It rejects program which could be safely typed. Other solution to this problem exists. Actually, Standard ML used a different solution at the beginning (carrying information about the typed hold in a cell along) but it has other drawbacks. MLTon has a really good page about all that : http://mlton.org/ValueRestriction http://mlton.org/ValueRestriction Some research was done about relaxing value restriction. OCaml type system, for example, has less constraints than SML and MLTon (you can see this paper about that http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf http://caml.inria.fr/pub/papers/garrigue-value_restriction-f...).

by emillon 13y ago

benbataille 13y ago

> Technically, [Let] is redundant because it is a combination of [App]+[Abs] : let x = e1 in e2 is equivalent to (λx.e2) e1. This equivalence does not hold in the HM formalisation. It's well explained in the Wikipedia article : http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism [Abs] is monomorphic while [Let] is polymorphic. Using the Wikipedia article exemple : \f.(f true, f 0) will not be typed while let f = \x.x in (f true, f 0) will be reduced to (bool, int).

groovy2shoes 13y ago
Does the nonequivalence have something to do with ML's value restriction?
- emillon 13y ago
  Yes. For example, if you generalize reference values, you can type ref [] as ∀a. (a list) ref, then store [4] to it, then retrieve a float from the head of the stored list, thus breaking the type system. It is a bit similar to array type variance problem that struck Java. One solution is to distinguish between syntactic forms that may allocate memory (eg, function applications) and the ones that can not (eg, abstractions, constants, variables), and only generalize the latter ones. (Operationally speaking, the two forms (let and abs+app) are always equivalent, though).
  - groovy2shoes 13y ago
    Thank you, that was a much more detailed response than I was expecting. Would it be correct to assume, then, that a pure ML would allow HM to be trivially modified to support the equivalence?
- benbataille 13y ago
  No, this nonequivalence applies directly to the typing of the lambda-calculus which was the topic of the original papers by Hindley and proven by Damas. On the contrary, the value restriction is a part of the extended rules used for the typing of ML. It was introduced because ML isn't pure, it supports references. The value restriction is there to prevent them having polymorphic type. The rule is simple : syntactic values are the only things receiving a polymorphic type. What is a syntactic value ? To quote Geoffrey Smith notes on SML97 "Basically, a syntactic value is an expression that can be evaluated without doing any computation". All this iss done in order to ensure type safety. Actually, if references could have a polymorphic type, the type system would accept incorrect programs such as : let r : 'a list ref = ref [] let r1 : int list ref = r let r2 : string list ref = r r2 := "a" let v : int = 1 + !r1 Which does not work because r, r1 and r2 are references to the same value. Value restriction is a bit overkill. It rejects program which could be safely typed. Other solution to this problem exists. Actually, Standard ML used a different solution at the beginning (carrying information about the typed hold in a cell along) but it has other drawbacks. MLTon has a really good page about all that : http://mlton.org/ValueRestriction http://mlton.org/ValueRestriction Some research was done about relaxing value restriction. OCaml type system, for example, has less constraints than SML and MLTon (you can see this paper about that http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf http://caml.inria.fr/pub/papers/garrigue-value_restriction-f...).