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.
Does this model infer nicely if you have an a -> b in the first argument? I’m thinking in particular if the passed in argument has infer fields. I suppose that you could have a syntax for explicitly passing in a and b in some cases to help the checker monomorphize properly…
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
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).
I don’t think this approach requires introducing new keywords for all these operations. You could instead add an
inferkeyword for type parameters that can always be inferred from the types of the function arguments. Somapwould change from:into:
When calling
map, you omit the typesaandband they’re instead inferred from the type of the first argument(a →b).This gives a more reasonable set of limitations:
maptype signature above is a little misleading, it shouldn’t have nested arrows.)infertype parameters that are fully determined by the function arguments. Puttinginferon a type parameter that cannot be so inferred would give a type error on the function definition. Instead you would omit theinfer, 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
Does this model infer nicely if you have an
a -> bin the first argument? I’m thinking in particular if the passed in argument has infer fields. I suppose that you could have a syntax for explicitly passing inaandbin some cases to help the checker monomorphize properly…score 2 · canonical
Yeah, I think that works fine. Say you have the type signatures:
and you call:
First you infer
c = Intbecause the argument3has typeInt, then you infera = Int, b = Intbecause(make-adder 10)has typeInt -> 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 forma = blike you do with unification.More detail about how I imagine this all working:
score 3 · canonical