type-systems

safer bet than gradual typing that could lead to very similar results, but I don't know how feasible or acceptable to mainstream programmers this is. [1] https://github.com/tomprimozic/type-systems/tree/master/exte... [2] https://elm-lang.org/docs/records

s useful. Gradual typing is relevant in this regard, which makes it possible to combine static and dynamic types and do type inference. See e.g. https://github.com/tomprimozic/type-systems/tree/master/grad... Now of course PyPy may hold the position that it's going to eschew static types on principle, but then it's a matter of ideology, not a technical reason, which causes these type annotations to "never have any value for PyPy".

` 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...

s" as well - check out [4], which attempts to do just that (implemented in language Sage [5]). I'm very interested in this topic as well, and have experimented a bit [6]; as it turns out, it's not that hard to implement a basic type-checker for simple refined types. It's also quite powerful - using Z3, even non-linear problems such as rectangular array access (mentioned by a poster below) are solvable, since you can trivially prove its safety using real arithmetics (which is decidable). The only big disadvantage that I see is the difficulty with dealing with state, but then again, even programmers can't reason about it properly; I mean, if `x` is a mutable object, can you really say `if x.a != 0 then 1 / 0` and be sure that no-one will modify `x.a` in the meantime from another thread? I hope that linear types could help. [1] http://goto.ucsd.edu/~rjhala/papers/liquid_types.pdf [2] https://www.cs.purdue.edu/homes/suresh/papers/vmcai13.pdf [3] http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pd... [4] http://www.kennknowles.com/research/knowles-flanagan.toplas.... [5] http://sage.soe.ucsc.edu/sage-tr.pdf [6] https://github.com/tomprimozic/type-systems/tree/master/refi...

oposals.