package higher_kinded

  1. Overview
  2. Docs
A library with an encoding of higher kinded types in OCaml

Install

Dune Dependency

Authors

Maintainers

Sources

higher_kinded-v0.14.0.tar.gz
sha256=867ec43d232f6dcc82403009d081cf63fa2fa7dd273a7d5fb7d2d5b598a1d8b6
md5=092fd34c2aba8fe5be548f7addc72309

Description

OCaml natively supports parameterized type constructors, such as =option=. The parameters of a type constructor may only be types, not arbitrary type constructors. This library makes it possible to parameterize a type with a witness that represents a type constructor.

Published: 31 May 2020

README

README.mlt

[%%org
  {|
#+TITLE: Higher kinded types

OCaml natively supports parameterized type constructors, such as ~option~. The parameters
of a type constructor may only be types, not arbitrary type constructors.

The following is not legal syntax:

#+begin_src ocaml
type 'a person =
  { name : string 'a
  ; age  : int    'a
  }
#+end_src

It is not possible to define such a type where ~'a~ can be replaced with something
like ~option~ or ~ref~, because you can't apply ~'a~ to other types like ~string~ or
~int~. In other words, although ~int option~ is a valid type expression, ~int 'a~ is not.

The ~Higher_kinded~ library makes something similar possible. The above example would be
defined like this:
|}]

type 'a person =
  { name : (string, 'a) Higher_kinded.t
  ; age : (int, 'a) Higher_kinded.t
  }

[%%org
  {|
Note that the ordering here is ~(string, 'a)~, not ~('a, string)~, similar to how you
write ~string option~, not ~option string~.

A signature defining a type constructor can include one of the ~Higher_kinded.S~
signatures, and its implementation should use one of the ~Higher_kinded.Make~ functors.
For example, ~Option~ could look something like this:
|}]

;;
#verbose true

module Option : sig
  type 'a t = 'a option

  include Higher_kinded.S with type 'a t := 'a t
end = struct
  type 'a t = 'a option

  include Higher_kinded.Make (Base.Option)
end

[%%expect
  {|
module Option :
  sig
    type 'a t = 'a option
    type witness1
    type 'a witness = ('a, witness1) Higher_kinded.t
    val inject : 'a t -> 'a witness
    val project : 'a witness -> 'a t
  end
|}]

[%%org
  {|
Now it is possible to define values of type ~int Option.witness~, which as you can see in
the signature above is the same as the type ~(int, Option.witness) Higher_kinded.t~:
|}]

let a = Option.inject (None : int option)

[%%expect {|
val a : int Option.witness = <abstr>
|}]

let b = Option.inject (Some 42)

[%%expect {|
val b : int Option.witness = <abstr>
|}]

[%%org {|
Here is how to observe them:
|}]

let _ = (Option.project a : int option)

[%%expect {|
- : int option = None
|}]

let _ = (Option.project b : int option)

[%%expect {|
- : int option = Some 42
|}]

[%%org
  {|
Now that ~Option~ can be used this way, we can express the ~person~ example from earlier:
|}]

let alice = { name = Option.inject (Some "alice doe"); age = Option.inject None }

[%%expect {|
val alice : Option.witness1 person = {name = <abstr>; age = <abstr>}
|}]

[%%org {|
If we did the same thing with refs:
|}]

module Ref : sig
  type 'a t = 'a ref

  include Higher_kinded.S with type 'a t := 'a t
end = struct
  type 'a t = 'a ref

  include Higher_kinded.Make (Base.Ref)
end

[%%expect
  {|
module Ref :
  sig
    type 'a t = 'a ref
    type witness1
    type 'a witness = ('a, witness1) Higher_kinded.t
    val inject : 'a t -> 'a witness
    val project : 'a witness -> 'a t
  end
|}]

[%%org {|
we could write:
|}]

let secret_agent : Ref.witness1 person =
  { name = Ref.inject (ref "alice"); age = Ref.inject (ref 55) }
;;

[%%expect {|
val secret_agent : Ref.witness1 person = {name = <abstr>; age = <abstr>}
|}]

[%%org {|
Here's how we could modify the references:
|}]

let () =
  Ref.project secret_agent.name := "Austin Powers";
  Ref.project secret_agent.age := 35
;;

[%%org
  {|
The ~inject~ and ~project~ functions have no runtime cost; they only change the type.

This library is based on Jeremy Yallop and Leo White's "Lightweight higher-kinded
polymorphism".
|}]

Dependencies (2)

  1. dune >= "2.0.0"
  2. ocaml >= "4.09.0"

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.