3 ms·

Higher-kinded bounded polymorphism in OCaml (2021)

buzzin__ 2y ago
[flagged]
- dang 2y ago
  "Please don't complain about tangential annoyances—e.g. article or website formats, name collisions, or back-button breakage. They're too common to be interesting." https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
  - kragen 2y ago
    may be worth mentioning in this case that firefox reader mode (the little cartoon icon of a printed page in the address bar) is helpful. also firefox will remember an increased font size setting for oleg's site if you hit ctrl-+ a few times
skulk 2y 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 2y ago
  It's tractable in practice. That's what the Idris (2) language does, for example.
  - dunham 2y 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 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 2y 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 2y 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 2y ago
    Thank you, that makes sense. Sadly, F# doesn't support GADT's yet.
- Neynt 2y ago
  x is a list. This is OCaml’s GADT syntax: https://dev.realworldocaml.org/gadts.html https://dev.realworldocaml.org/gadts.html
- deleted 2y ago
  [deleted]
tempodox 2y ago
This article is pure gold. Rarely is this stuff explained so well.

[flagged]

dang 2y ago
"Please don't complain about tangential annoyances—e.g. article or website formats, name collisions, or back-button breakage. They're too common to be interesting." https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- kragen 2y ago
  may be worth mentioning in this case that firefox reader mode (the little cartoon icon of a printed page in the address bar) is helpful. also firefox will remember an increased font size setting for oleg's site if you hit ctrl-+ a few times

> 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 2y ago
It's tractable in practice. That's what the Idris (2) language does, for example.
- dunham 2y 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 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 2y 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 2y 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 2y ago
  Thank you, that makes sense. Sadly, F# doesn't support GADT's yet.
Neynt 2y ago
x is a list. This is OCaml’s GADT syntax: https://dev.realworldocaml.org/gadts.html https://dev.realworldocaml.org/gadts.html
deleted 2y ago
[deleted]

tempodox 2y ago

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