> Why can’t we just allow polymorphic lambda-bound variables?
Two reasons. The first is that in general, type inference for higher-rank polymorphism is undecidable. The second is that even if it were decidable, it would be impractical - I think that if we have a program like this one:
let test(f) = (f(1), f(true))
the assumption that the programmer made an error is statistically much more likely than the assumption that `f` should have a polymorphic type. Another reason is that it's not entirely clear what kind of polymorphic type to infer for `f` - should it be `forall a. a -> a` or e.g. `forall a. a -> int`?
> What does this have to do with different “ranks” of polymorphism?
Higher-rank polymorphism means that polymorphic types can appear within other types; in a system with support for higher-rank polymorphic types, the parameter `f` in the function `test` above could be declared with type `forall a. a -> a`, the function `test` would have a type `(forall a. a -> a) -> int * bool`. Higher-rank polymorphism is formalized using System F, and there are a few implementations of (incomplete, but decidable) type inference for it - see e.g. Daan Leijen's research page [1] about it, or my experimental implementation [2] of one of his papers. Higher-rank types also have some limited support in OCaml and Haskell.
> How is let-polymorphism implemented? How do you implement it without just copying code around?
The "standard" implementation consists of two operations, generalization and instantiation. At let bindings, types are generalized by replacing all unbound type variables with polymorphic type variables (care must be taken not to generalize type variables that can be bound later, but that's a secondary issue here). Every time a variable with a polymorphic type is used, its type is instantiated, which means that all polymorphic type variables are replaced with fresh unbound type variables.
let f = fun x -> (x, x)
print f(1), f("boo")
In the example above, the type inferred for `fun x -> (x, x)` is `_a -> _a * _a`, where `_a` is an unbound (but not polymorphic) type variable. At let binding, this type is transformed into `forall a. a -> a * a` by replacing `_a` with a polymorphic type variable `a` (in most ML languages, the `forall` is implicit). Then, when `f` is used in `f(1)`, its type is instantiated into `_b -> _b * _b` and `_b` is unified with the type of `1`, `int`. When `f` is used in `f("boo")`, its type is instantiated into `_c -> _c * _c`, and `_c` is unified with type of `"boo"`, `string`. Since `_b` and `_c` are different variables, there is no error here (if `f` had a monomorphic type, `_b` and `_c` would in fact be the same, and this example would result in an error "cannot unify type int with type string").
> What’s the relationship between let enabling exponential function composition and the exponential time result?
So there is quite a bit of copying happening every time a variable with polymorphic type is used. I've never studied the worst-case scenarios of Hindley-Milner, but I imagine that it has to do with instantiation copying large polymorphic types around.
> Do implementations of Hindley-Milner actually represent types as dags and utilize structural sharing?
Yes; an unbound type variable is typically represented as a reference cell, which is assigned to the type the type variable is unified with. So, if we have
double : forall a. a -> a * a
double (1, 1, 1) : (int * int * int) * (int * int * int)
then the type of double is first instantiated, yielding `_b -> _b * _b`, and then the type of the parameter is unified with the type of the argument, `int * int * int`. At this point, the reference cell in the internal representation of `_b` is updated to point to `int * int * int`, which means that both `_b` in the result type actually point to the same representation of `int * int * int`.
[1] http://research.microsoft.com/en-us/projects/fcp/
[2] https://github.com/tomprimozic/type-systems/tree/master/firs...
Two reasons. The first is that in general, type inference for higher-rank polymorphism is undecidable. The second is that even if it were decidable, it would be impractical - I think that if we have a program like this one:
the assumption that the programmer made an error is statistically much more likely than the assumption that `f` should have a polymorphic type. Another reason is that it's not entirely clear what kind of polymorphic type to infer for `f` - should it be `forall a. a -> a` or e.g. `forall a. a -> int`?> What does this have to do with different “ranks” of polymorphism?
Higher-rank polymorphism means that polymorphic types can appear within other types; in a system with support for higher-rank polymorphic types, the parameter `f` in the function `test` above could be declared with type `forall a. a -> a`, the function `test` would have a type `(forall a. a -> a) -> int * bool`. Higher-rank polymorphism is formalized using System F, and there are a few implementations of (incomplete, but decidable) type inference for it - see e.g. Daan Leijen's research page [1] about it, or my experimental implementation [2] of one of his papers. Higher-rank types also have some limited support in OCaml and Haskell.
> How is let-polymorphism implemented? How do you implement it without just copying code around?
The "standard" implementation consists of two operations, generalization and instantiation. At let bindings, types are generalized by replacing all unbound type variables with polymorphic type variables (care must be taken not to generalize type variables that can be bound later, but that's a secondary issue here). Every time a variable with a polymorphic type is used, its type is instantiated, which means that all polymorphic type variables are replaced with fresh unbound type variables.
In the example above, the type inferred for `fun x -> (x, x)` is `_a -> _a * _a`, where `_a` is an unbound (but not polymorphic) type variable. At let binding, this type is transformed into `forall a. a -> a * a` by replacing `_a` with a polymorphic type variable `a` (in most ML languages, the `forall` is implicit). Then, when `f` is used in `f(1)`, its type is instantiated into `_b -> _b * _b` and `_b` is unified with the type of `1`, `int`. When `f` is used in `f("boo")`, its type is instantiated into `_c -> _c * _c`, and `_c` is unified with type of `"boo"`, `string`. Since `_b` and `_c` are different variables, there is no error here (if `f` had a monomorphic type, `_b` and `_c` would in fact be the same, and this example would result in an error "cannot unify type int with type string").> What’s the relationship between let enabling exponential function composition and the exponential time result?
So there is quite a bit of copying happening every time a variable with polymorphic type is used. I've never studied the worst-case scenarios of Hindley-Milner, but I imagine that it has to do with instantiation copying large polymorphic types around.
> Do implementations of Hindley-Milner actually represent types as dags and utilize structural sharing?
Yes; an unbound type variable is typically represented as a reference cell, which is assigned to the type the type variable is unified with. So, if we have
then the type of double is first instantiated, yielding `_b -> _b * _b`, and then the type of the parameter is unified with the type of the argument, `int * int * int`. At this point, the reference cell in the internal representation of `_b` is updated to point to `int * int * int`, which means that both `_b` in the result type actually point to the same representation of `int * int * int`.[1] http://research.microsoft.com/en-us/projects/fcp/
[2] https://github.com/tomprimozic/type-systems/tree/master/firs...