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_offunction 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 ::= t = t | exists 'a :: k. U | U && U
This is expressed as:
kind_offor checking kinds during conjunction
varto introduce existentially bound variables in the unification problem
freeto wrap structures into terms
equateto emit equality constraints between terms
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 (