I was reading the “ Lightweight Higher-Kinded Polymorphism ” paper and I couldn’t quite understand the motivation section (I’m familiar with Haskell). In Haskell data and newtype definitions create fresh data types. It is possible to hide the data constructors of such types by leaving them out of t…

I wrote the description in the paper, so you’ve already read my best efforts to explain this, but I’ll have another go. In Haskell, if you have a type Foo Int you know that there is no type Bar Int that will be equal to it. The newtypes/datatypes Foo and Bar are fresh types that do not overlap. Yo…

I came up with an example that demonstrates my understanding of the issue. The goal is to construct an example where always choosing either of the two possible solutions for the unification problem makes the program ill-typed (so we can see there is no most general solution). First, let’s introduce…

Thanks for taking the time to write a detailed explanation! Unfortunately, after re-reading it multiple times, I’m still not certain of what exactly the OCaml code is doing. For example, what do the _ in the type signatures do? Also, I’m not sure what the final conclusion is :confused: ? I would’ve…

I think the final conclusion is simply that due to this issue with higher-order unification it’s not possible to have both implicit type abstraction (i.e. without any annotations e.g. in the form of type coercions/wrapper constructors) and implicit higher-kinded polymorphism (i.e. without any annot…

For the type signatures I just wanted to show an example where having a synonym type a t = int list with a phantom parameter can be “useful” or, at least, meaningful. I could have used the number of elements in the set as type-level number or some other trick… But since OCaml doesn’t have type famil…

Thanks for that explanation. It’s the first time I’ve seen an explanation for something that I had only had an intuition about before.

[image] lpw25: For example, type 'a foo = 'a * int type 'a bar = int * 'a In this case, if you need to unify int foo with int 'm (assuming we had higher-kinded variables) you can not just make 'm = foo because 'm = bar would also be a valid solution and neither one is more general than the oth…

Unless I’m misunderstanding you, then (assuming OCaml had higher-kinded variables) considering: let foo : 'm. int 'm -> float 'm option = fun _ -> None let bar : int foo = 1, 2 let result = foo bar is sufficient to see that both solutions are not equivalent. If you go one way then you get result :…

Indeed. By manually constraining the types it’s possible to construct much smaller examples. I also think another reason why Haskell approach doesn’t work for OCaml is that OCaml has type synonyms that don’t have a canonical form, e.g. type ('a, 'b) t = [`A of 'a | `B of 'b] Even if we choose to a…

is the ~ above part of the type expression language?

No, just to designate a unification problem, similar to Haskell’s equality constraint ~ (in Haskell it is a part of type expression language).

Higher kinded polymorphism

Learning

lpw25 July 1, 2018, 9:17am 14

It is not particularly related to generative vs applicative functors, these issues come up regardless of whether functors are applicative or generative.

Topic		Replies	Views
The alias problem : Lightweight HK polymorphism Learning type-system , type-inference , higher-kinds	5	669	September 17, 2024
Weird behaviors with first order polymorphism Learning type-system , bug	5	640	January 5, 2024
Modular Implicits Ecosystem compiler , faq	63	24354	October 24, 2022
Struggling with (higher-kinded?) polymorphism Learning	11	275	March 7, 2026
To create or not to create a new type Learning	24	2094	June 10, 2021

Higher kinded polymorphism

Related topics