Higher-kinded bounded polymorphism in OCaml (2021) | Hacker News Reader

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

I understand that app is an extensible type and this line adds a union case called List_name to the type, but the signature of List_name confuses me. If I write (List_name x) is x a list or a function?

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

      List_name: 'a list -> ('a, list_name) app

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.

Thank 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.

Reply on news.ycombinator.com