Vague Arguments
Remind the definition of List.
After the definition List.null is a List(String).
List.null is also a List(Trivial).
How can List.null be both List(String) and List(Trivial)?
Because List.null has been vague about its argument.
The type of List.null is actually (vague E: Type) -> List(E).
We can also explicitly apply List.null to a vague argument.
A vague argument is like an implicit argument, but it is resolved during type checking, by the information of the return type.
For example, we can use vague arguments to define a function -- my_list_null, who works just like the data constructor List.null.
Suppose I am the type checker, I am checking my_list_null: List(String).
I infer my_list_null to be (vague E: Type) -> List(E);
I compare the given return type List(String) with List(E);
I insert the vague argument for my_list_null, to get my_list_null(vague String).
We can also define my_list_cons to be like List.cons.