Higher-kinded bounded polymorphism in OCaml (2021)

Higher-kinded bounded polymorphism in OCaml (2021)(okmij.org)

141 points by tinyspacewizard 1 year ago | 10 comments

skulk 1 year ago |

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

nerdponx 1 year ago | |

It's tractable in practice. That's what the Idris (2) language does, for example.

dunham 1 year ago | | |

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.

munchler 1 year ago |

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?

octachron 1 year ago | |

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.

munchler 1 year ago | | |

Thank you, that makes sense. Sadly, F# doesn't support GADT's yet.

Neynt 1 year ago | |

x is a list. This is OCaml’s GADT syntax: https://dev.realworldocaml.org/gadts.html

tempodox 1 year ago |

This article is pure gold. Rarely is this stuff explained so well.