Hi fellow teachers and/or OCaml-type-system experts,
Until now, when teaching at ENSEEIHT, we haven’t been insisting on typing (global) let definitions, leaving typing annotations to val declarations.
However, we are pondering adding type annotations on let definitions. Specifically explicitly polymorphic annotations (probably using the ‘a . ... syntax). There are several reasons:
- It stresses the fact that in
letdefinitions, a non-quantified'adoes not stand for polymorphism, contrarily to declarations (we don’t cover type systems in this course and students tend to think that'ais necessarily polymorphic). - This notation is also covered in
valsince v4.14.0 so we now have a homogeneous notation for definitions and declarations. - Such annotations also provide with better error messages, in particular in cases when a unification variable would have been specialized without students noticing.
- This syntax is also useful when introducing “non-uniform” algebraic types, in which case polymorphic recursion is needed to type some functions.
- Finally our students already know more mainstream programming languages such as Java, where a similar notation is used for genericity, so it’s already familiar for them.
Another possibility would be to only use the type a . ... annotation which combines polymorphic recursion with locally-abstract types. Since, later in the course, we also introduce GADTs, this would allow us to teach only one notation, and since this isn’t a theory course, this would avoid difficulties trying to explain differences between syntaxes for polymorphic recursion, locally abstract types and their combination. We would lose the homogeneity with the notation in val though. (Also, as is discussed in this Github issue, the locally-abstract-type notation is probably the most user-friendly among the three possibilities.)
I’d like to know the stance of OCaml teachers or type-system experts on this topic. What would you avoid, what would you advise, how do you address this topic?