Mentions légales du service

Draft: Kinded Structures


Many type systems are equipped with kinding systems. Mostly notably (and relevant to OCaml) are the various kinding systems associated with rows. This MR aims to implement a generic kinding framework in Inferno.

This MR is used as the basis of my implementation of polymorphic variants which I will soon push and begin upstreaming.


The changes in this MR introduce a notion of a 'kinded structure':

  • an abstract type kind;
  • a kind_of function for structures that implements the kinding system on structures:
type kind

exception IllKinded
val kind_of : ('a -> kind) -> 'a structure -> kind

Kinds are equipped with a partial order k1 <= k2 defined using subkind : kind -> kind -> bool.

The MR also refactors structural conjunction to be parameterised over a generic 'first-order unification problem' U:

 U ::= t = t | exists 'a :: k. U | U && U

This is expressed as:

  • kind_of for checking kinds during conjunction
  • var to introduce existentially bound variables in the unification problem
  • free to wrap structures into terms
  • equate to emit equality constraints between terms

The Option structure is refactored into FirstOrder structure where variables now contain kinds represented as Var k instead of None. The conjunction of first-order variables relies on a partial least upper bound operator between kinds (kind_lub).

Edited by Alistair O'Brien

Merge request reports