Higher-kinded bounded polymorphism in OCaml (2021)
okmij.org> Thus, with type aliases, the type equality problem becomes the higher-order unification problem, which is not decidable.
I wonder how much this is a problem in practice, aside from the type-checker taking too long.
It's tractable in practice. That's what the Idris (2) language does, for example.
If anyone is interested in how this works, I've found András Kovács' "Elaboration Zoo" to be a good tutorial: https://github.com/AndrasKovacs/elaboration-zoo
It incrementally covers normalization by evaluation, bidirectional typechecking, basic pattern unification, implicit insertion (which relies on unification), and then more sophisticated variants on pattern unification.
I'm more familiar with F#, so I got stuck at this line:
type ('a,'b) app += List_name : 'a list -> ('a,list_name) app
The variable "x" would be a list in this case. This the GADT (Generalized Abstract Data Types) syntax, where the type of the whole union can depend on the discriminated union case. Thus
reads: for any value "x" of type "'a list", "List_name x" constructs a value of type "('a, list_name) app". In this case, it is the the "list_name" tag part of the type which is dependent on the union case.List_name: 'a list -> ('a, list_name) appThank you, that makes sense. Sadly, F# doesn't support GADT's yet.
x is a list. This is OCaml’s GADT syntax: https://dev.realworldocaml.org/gadts.html
This article is pure gold. Rarely is this stuff explained so well.