u64 r = random_u64(); // uniform chance over [0..UINT64_MAX]
T chosen = choices[r % 10];

we might think every item has a 1/10 chance of being chosen. It does not.

…technically. Though how likely are you to actually see the difference? The relative chances of picking 0..10 are 1844674407370955162 for 0..6 and 1844674407370955161 for 7..10. Suppose you instead panicked for the largest 6 possible results of random_u64(), making the remaining distribution uniform. The chance of encountering that error is 6/2^64 = 3*10^-19, which you’re realistically not going to hit. That’s getting to the point where you’re more likely to notice a cosmic ray bit flip than to encounter the distribution being off.

score 1 · canonical

Yeah, I think that works fine. Say you have the type signatures:

map : ∀(infer a : Type, infer b : Type) → (a → b) → List a → List b
make-adder : ∀(infer c: Type, a implements Plus) → c -> (c → c)
make-adder x = lambda (y: a) x + y

and you call:

map (make-adder 10) [1, 2, 3]  // evaluates to [11, 12, 13]

First you infer c = Int because the argument 3 has type Int, then you infer a = Int, b = Int because (make-adder 10) has type Int -> Int. Note that we’re not doing general unification here: all of these inferences are always “type variables = concrete types”. You can never get a constraint of the form a = b like you do with unification.

More detail about how I imagine this all working:

• At every use site of a variable, that variable’s type is known.
• Therefore, arguments to lambdas and functions require type annotations. Unless, as the blog post suggests, there’s already an expected type for the lambda that comes from the context it’s placed in. (E.g. if you pass a lambda to a function, and that function requires it to have a fixed type (no type vars), you can omit the types of the arguments to the lambda.)
• The return value of a function or lambda can be inferred by type checking its body, though I think we’ve correctly settled as a community on the requirement that function return types must be annotated (though not lambda return types).
• Given all of the above, you can nearly always tell the type of an expression given only the types of the variables that appear in it. The exception is, as just mentioned, that if the context an expression is in requires it to have a certain type directly (nothing fancy like “it must have the same type as that other argument”), then that required type can be used to disambiguate otherwise ambiguous types (like a lambda not annotating the types of its arguments).

score 3 · canonical

There’s a related problem, which is how unification interacts with type errors. If you’re doing pure unification, you realize at some arbitrary point in time that a = Maybe Int but also a = Maybe String. Where did these come from? Which one is wrong? If one is from a type signature and the other is from a value, then the type error should be at the location of the value, because it didn’t have the expected type. They could also both be from type signatures, or both from values. How is this provenance information tracked? What do you do when the type mismatch came from a chain of reasoning 7 steps long each at different source locations? What happens when there are higher-kinded types – I don’t even know what questions to ask in that case, but imagine they’re tricksy questions.

I always give type signatures to functions in Haskell, in part to improve the error messages. And I imagine it’s not trivial for its error messages to be as good as they are, given that it’s doing unification.

score 8 · canonical

I don’t think this approach requires introducing new keywords for all these operations. You could instead add an infer keyword for type parameters that can always be inferred from the types of the function arguments. So map would change from:

map : ∀(a b : Type) → (a → b) → List a → List b

into:

map : ∀(infer a : Type, infer b : Type) → (a → b) → List a → List b

When calling map, you omit the types a and b and they’re instead inferred from the type of the first argument (a →b).

This gives a more reasonable set of limitations:

• It doesn’t play well with automatic currying, since a curried argument might be required to infer some type parameters. (So the map type signature above is a little misleading, it shouldn’t have nested arrows.)
• You can only infer type parameters that are fully determined by the function arguments. Putting infer on a type parameter that cannot be so inferred would give a type error on the function definition. Instead you would omit the infer, and the caller will have to specify the type parameters explicity. But these are more complex functions so it’s more reasonable to require annotations on them.

score 8 · canonical