Higher-kinded bounded polymorphism in OCaml (2021) (opens in new tab)

(okmij.org)

141 pointstinyspacewizard1y ago10 comments

10 comments

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

nerdponx1y ago

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

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

munchler1y 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?

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

munchler1y ago

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

Neynt1y ago

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

tempodox1y ago

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

j / k navigate · click thread line to collapse

10 comments

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

nerdponx1y ago

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

dunham1y 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

munchler1y 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

octachron1y 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

munchler1y ago

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

Neynt1y ago

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

tempodox1y ago

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

j / k navigate · click thread line to collapse