Experimental, procreative type system based on a foundational binary type equipped with induction and parametric polymorphism.

Cygnus.ml

(** Cygnus is an experiment for the proof assistant Caroline.

    It defines a simple type system based on a foundational type -
    coloquially called "Hole" - which is inhabited by two
    constructors, `⊥` (bottom) and `()` (unit).

    From this type, we describe each other type of the system,
    by either simply settling on a bijection from Hole, or by
    inductively specifying its constructors.

    On top of that, we also introduce a lambda variant for
    parametric polymorphism, allowing us to establish generic
    types, e.g. linked lists à la Lisp in this implementation. *)

module Hole = struct
  (** Our foundational type, from which all the other ones are based on. *)
  type t =
    | Bottom : t (* Termination (or lack thereof) *)
    | Unit : t (* Continuation *)
end

module Foundation = struct
  (** Simple bijective factory from Hole to our new type. *)
  type 'a primitive = Hole.t -> 'a

  (** More complex factory that allow us to express types with
      a greater number of constructors. *)
  type 'a inductive = 'a -> Hole.t -> 'a
end

module Type = struct
  (* Various constructors for the different type kinds. *)
  type t =
    | Primitive : 'a Foundation.primitive -> t
    | Inductive : 'a Foundation.inductive -> t
    | Lambda : (t -> t) -> t

  (** The well-known boolean type: false and true. *)
  let boolean =
    let boolean_factory = function
      | Hole.Bottom -> `False
      | Hole.Unit -> `True
    in
    Primitive boolean_factory
  ;;

  (** Inductive definition of natural numbers in the style of
      Peano. *)
  let nat =
    let nat_factory (pred : [< `Zero | `Succ of 'a ]) = function
      | Hole.Bottom -> `Zero
      | Hole.Unit -> `Succ pred
    in
    Inductive nat_factory
  ;;

  (** Generic list type, nil-cons style. *)
  let list =
    let list_generic (t : t) =
      Inductive
        (fun (next : [< `Nil | `Cons of 'a * 'b ]) -> function
          | Hole.Bottom -> `Nil
          | Hole.Unit -> `Cons (t, next))
    in
    Lambda list_generic
  ;;

  (** [specialize app arg] attempts to specialize [app] with
      [arg], i.e. applies [app] to [arg]. For example,
      [specialize list int] gives us a new type which is a
      specific list where all the items are integers.
      The function returns an [option] as it requires [app] to
      be a lambda type specifically. *)
  let specialize (app : t) (arg : t) : t option =
    match app with
    | Lambda lambda -> Some (lambda arg)
    | _ -> None
  ;;

  (** [specialize_or_raise app arg] is identical to
      [specialize app arg], except that it raises an exception
      upon failure instead of returning an [option]. *)
  let specialize_or_raise (app : t) (arg : t) : t =
    match specialize app arg with
    | None -> failwith "failed to specialize (app must be a Lambda)"
    | Some t -> t
  ;;
end

let list_of_nats = Type.specialize_or_raise Type.list Type.nat