Higher-kinded bounded polymorphism in OCaml (2021)

#1

Post by tinyspacewizard » Sun, Jul 28, 2024, 9:40 PM UTC

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

Re: Higher-kinded bounded polymorphism in OCaml (2021)

#2

Post by buzzin__ » Mon, Jul 29, 2024, 12:45 AM UTC

[flagged]

Re: Higher-kinded bounded polymorphism in OCaml (2021)

#3

Post by dang » Mon, Jul 29, 2024, 1:02 AM UTC

buzzin__ wrote: post #2

[flagged]

"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

Re: Higher-kinded bounded polymorphism in OCaml (2021)

#4

Post by skulk » Mon, Jul 29, 2024, 1:09 AM UTC

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

Re: Higher-kinded bounded polymorphism in OCaml (2021)

#5

Post by nerdponx » Mon, Jul 29, 2024, 2:02 AM UTC

skulk wrote: post #4

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

Re: Higher-kinded bounded polymorphism in OCaml (2021)

#6

Post by kragen » Mon, Jul 29, 2024, 9:45 AM UTC

dang wrote: post #3

buzzin__ wrote: post #2

[flagged]

" 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

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

Re: Higher-kinded bounded polymorphism in OCaml (2021)

#7

Post by munchler » Mon, Jul 29, 2024, 2:14 PM UTC

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?

Re: Higher-kinded bounded polymorphism in OCaml (2021)

#8

Post by octachron » Mon, Jul 29, 2024, 2:25 PM UTC

munchler wrote: post #7

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.

Re: Higher-kinded bounded polymorphism in OCaml (2021)

#9

Post by Neynt » Mon, Jul 29, 2024, 2:26 PM UTC

munchler wrote: post #7

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?

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

Re: Higher-kinded bounded polymorphism in OCaml (2021)

#10

Post by [deleted] » Mon, Jul 29, 2024, 2:28 PM UTC

munchler wrote: post #7

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?

[deleted]