package higher

The code in this directory is taken from the paper "Lightweight Higher-Kinded Polymorphism" (Jeremy Yallop and Leo White). The following examples are available:

• typed defunctionalization (Section 1.2)
• folds over perfect trees (Section 2.1)
• Leibniz equality (Section 2.2)
• the codensity transform (Section 2.3)
• kind polymorphism (Section 2.4)

Most of the code depends on the higher library, which you can install using opam. Once higher is installed you can load the examples into the top level directly:

  $ ocaml
        OCaml version 4.01.0

  # #use "topfind";;
  [...]
  # #require "higher";;
  [...]
  # #use "example-1-perfect-trees.ml";;
  type 'a perfect = Zero of 'a | Succ of ('a * 'a) perfect
  [...]
  #