a simple type system with support for (co)cartesian types

CT.md

Notes

(Co)Cartesian Types

Definitions

A cartesian type is a generalized type product where one inhabitant, called origin is common to all the types involved (called axes). A cocartesian type is a generalized type sum with a common origin to all axes.

That is, A * ... * Z is a cartesian type if there exists one inhabitant i common to every axis — i_A = i_B = ... = i_Z. Similarly, A | ... | Z is a cocartesian type if there is one inhabitant i common to every axis.

Examples

Given List(Letter) the set of all the lists containing letters of the latin alphabet (including none) and List(Nat) the set of all the lists containing integers 0, 1, 2, ... (also including none), List(Letter) * List(Nat) is a cartesian type where i is the empty list [].

Given Nonneg the integers 0, 1, 2, ... and Nonpos the integers 0, -1, -2, ..., Nonneg | Nonpos is a cocartesian type where i is 0.

Vocabulary

A unit of an axis x is a constructor of x that is, as opposed to the origin, not shared with the other axes of the cartesian type.

Possible alternative names

It was suggested to me by @MithicSpirit that global inductive type and global coproduct type (as the origin is akin to category theory's global element) are better names than cartesian and cocartesian types.

Minji's implementation

In this implementation (Minji), the syntax is as follows:

(cartesian|cocartesian) type <name> [ <axes> ] =
  | origin <name> (: <type>)
  | unit[<axis>] <name> (: <type>)

→ Things in parentheses are optional. (A|B) denotes a choice ; you have to write either A or B.

→ Axis parameters of the type must be unique and are separated with a space.

→ The origin must be specified¹. There is no constraint on the number of unit constructors.

→ The origin cannot take the type being defined as argument² ; in other words, if induction there is, it must occur on one of the unit constructors.

→ The unit constructors must produce a term of the type being defined, directly or after their application.

Example

cocartesian type Int [ nonneg nonpos ] =
  | origin Zero
  | unit[nonneg] Succ : Int -> Int
  | unit[nonpos] Pred : Int -> Int

Relation with row polymorphism and GADTs

The given example is equivalent to the following OCaml code:

type 'axis int =
  | Zero : [< `Nonneg | `Nonpos ] int
  | Succ : [< `Nonneg ] int -> [< `Nonneg ] int
  | Pred : [< `Nonpos ] int -> [< `Nonpos ] int

(Thanks to Alice for providing the code)

How to run

Assuming you have ocamlc and utop installed:

ocamlc Quickmap.ml && utop Quickmap.cmo Minji.ml

Footnotes

1. Actually, not necessarily (because of co-origins and stuff), but I've only implemented a basic version of CTs. ↩

2. Well, Minji currently does not even support function origins yet. Sorry. ↩

Minji.ml

let ( *> ) (f : 'a -> 'b) (g : 'b -> 'c) : 'a -> 'c = Fun.compose g f

module Bool = struct
  include Bool

  let on_true (func : unit -> unit) (bool : t) : t =
    (match bool with
     | true -> func ()
     | false -> ());
    bool
  ;;

  let on_false (func : unit -> unit) (bool : t) : t =
    (match bool with
     | false -> func ()
     | true -> ());
    bool
  ;;
end

module Option = struct
  include Option

  let on_none (func : unit -> unit) (option : 'a t) : 'a t =
    (match option with
     | None -> func ()
     | Some _ -> ());
    option
  ;;
end

module String = struct
  include String

  let indent ~(count : int) (string : t) : t =
    string
    |> split_on_char '\n'
    |> List.map (Printf.sprintf "%*s%s" count " ")
    |> concat "\n"
  ;;
end

module List = struct
  include List

  let map_on_cons (func : 'a -> 'b) (list : 'a list) : 'b list option =
    match list with
    | [] -> None
    | _ -> Some (List.map func list)
  ;;

  let count_elements (list : 'a list) : ('a * int) list =
    let rec inner (list : 'a list) (acc : ('a * int) list) : ('a * int) list =
      match list with
      | [] -> acc
      | first :: rest ->
        let new_count =
          List.assoc_opt first acc |> Option.map Int.succ |> Option.value ~default:1
        in
        (first, new_count) :: List.remove_assoc first (inner rest acc)
    in
    inner list []
  ;;
end

module Highlight = struct
  let bold = Printf.sprintf "\x1b[1m%s\x1b[22m"
  let dim = Printf.sprintf "\x1b[2m%s\x1b[22m"
  let fg (color : int) : string -> string = Printf.sprintf "\x1b[3%dm%s\x1b[39m" color
  let comment = dim
  let keyword = bold *> fg 5
  let operator = fg 5
  let type' = fg 3
  let metatype = fg 1
  let string = fg 2
  let constructor = fg 4
  let name = fg 6
  let error = bold *> fg 1
  let success = bold *> fg 2
  let warning = bold *> fg 3
  let info = bold *> fg 4
  let note = bold *> fg 5
end

module Name = struct
  type t = string

  let ( = ) = String.equal
  let repr (name : t) : string = Highlight.name name
end

module Syntactic = struct
  type t =
    | Atom
    | Compound
end

module Core = struct
  type term =
    | App of term * term
    | Fun of parameter list * term
    | Var of Name.t

  and kind =
    | Arrow of kind * kind
    | Axial of kind * Name.t list
    | Bottom
    | Product of kind * kind
    | Var of Name.t

  and parameter = Named of Name.t * kind

  let rec term_to_syntactic (term : term) : Syntactic.t =
    match term with
    | App _ | Fun _ -> Compound
    | Var _ -> Atom
  ;;

  let kind_to_syntactic (kind : kind) : Syntactic.t =
    match kind with
    | Axial _ | Bottom | Var _ -> Atom
    | Arrow _ | Product _ -> Compound
  ;;

  let rec repr_term (term : term) : string =
    match term with
    | App (function', argument) ->
      Printf.sprintf
        "%s %s"
        (repr_term_considering_precedence function')
        (repr_term_considering_precedence argument)
    | Fun (parameters, body) ->
      Printf.sprintf
        "%s %s %s %s"
        (Highlight.keyword "fun")
        (parameters |> List.map repr_parameter |> String.concat " ")
        (Highlight.operator "->")
        (repr_term body)
    | Var name -> Name.repr name

  and repr_term_considering_precedence (term : term) : string =
    let repr = repr_term term in
    match term_to_syntactic term with
    | Atom -> repr
    | Compound -> "(" ^ repr ^ ")"

  and repr_kind (kind : kind) : string =
    match kind with
    | Arrow (left, right) ->
      Printf.sprintf
        "%s %s %s"
        (repr_kind_considering_precedence left)
        (Highlight.operator "->")
        (repr_kind right)
    | Axial (subkind, axes) ->
      Printf.sprintf
        "%s[%s]"
        (repr_kind_considering_precedence subkind)
        (List.map Name.repr axes |> String.concat ", ")
    | Bottom -> Printf.sprintf "%s" (Highlight.metatype "\u{22A5}")
    | Product (left, right) ->
      Printf.sprintf
        "%s %s %s"
        (repr_kind left)
        (Highlight.operator "*")
        (repr_kind_considering_precedence right)
    | Var name -> Highlight.type' name

  and repr_kind_considering_precedence (kind : kind) : string =
    let repr = repr_kind kind in
    match kind_to_syntactic kind with
    | Atom -> repr
    | Compound -> "(" ^ repr ^ ")"

  and repr_parameter (parameter : parameter) : string =
    match parameter with
    | Named (name, kind) -> Printf.sprintf "(%s : %s)" (Name.repr name) (repr_kind kind)
  ;;

  module Term = struct
    type t = term

    let app (function' : t) (argument' : t) : t = App (function', argument')
    let fun' (parameters : parameter list) (body : t) : t = Fun (parameters, body)
    let var (name : Name.t) : t = Var name
    let repr = repr_term
  end

  module Kind = struct
    type t = kind

    let arrow (left : t) (right : t) : t = Arrow (left, right)
    let axial (subkind : kind) (axes : Name.t list) : t = Axial (subkind, axes)
    let product (left : t) (right : t) : t = Product (left, right)
    let var (name : Name.t) : t = Var name

    let is_bottom (kind : t) : bool =
      match kind with
      | Bottom -> true
      | _ -> false
    ;;

    let repr = repr_kind

    module Notation = struct
      let ( --> ) = arrow
      let ( @ ) = axial
      let ( * ) = product
    end
  end

  module Parameter = struct
    type t = parameter

    let named (name : Name.t) (kind : kind) : t = Named (name, kind)
    let repr = repr_parameter
  end

  module Definition = struct
    module Let = struct
      type t =
        { binding : Name.t
        ; body : Term.t
        }

      let repr : t -> string = function
        | { binding; body } ->
          Printf.sprintf
            "%s %s %s %s"
            (Highlight.keyword "let")
            (Highlight.name binding)
            (Highlight.operator "=")
            (Term.repr body)
      ;;
    end

    module Origin = struct
      type t =
        { name : Name.t
        ; annotation : Kind.t
        }

      let repr { name; annotation } : string =
        Printf.sprintf
          "%s %s %s : %s\n"
          (Highlight.operator "|")
          (Highlight.keyword "origin")
          (Highlight.constructor name)
          (Kind.repr annotation)
      ;;
    end

    module Unit = struct
      type t =
        { name : Name.t
        ; axis : Name.t
        ; annotation : Kind.t
        }

      let repr { name; axis; annotation } : string =
        Printf.sprintf
          "%s %s[%s] %s : %s\n"
          (Highlight.operator "|")
          (Highlight.keyword "unit")
          (Highlight.name axis)
          (Highlight.constructor name)
          (Kind.repr annotation)
      ;;
    end

    module Global_algebraic_type = struct
      type t =
        { binding : Name.t
        ; axes : Name.t list
        ; origin : Origin.t
        ; units : Unit.t list
        }

      let repr_axes (axes : Name.t list) : string =
        match axes with
        | [] -> ""
        | _ ->
          axes |> List.map Highlight.name |> String.concat " " |> Printf.sprintf " [ %s ]"
      ;;

      let repr_units (units : Unit.t list) : string =
        match units with
        | [] -> ""
        | _ -> units |> List.map Unit.repr |> String.concat ""
      ;;

      let repr { binding; axes; origin; units } : string =
        Printf.sprintf
          "%s %s%s %s\n  %s%s"
          (Highlight.keyword "type")
          (Highlight.type' binding)
          (repr_axes axes)
          (Highlight.operator "=")
          (Origin.repr origin)
          (repr_units units |> String.indent ~count:2)
      ;;
    end

    module Type = struct
      type t =
        | Cartesian of Global_algebraic_type.t (* product *)
        | Cocartesian of Global_algebraic_type.t (* sum *)

      let repr : t -> string = function
        | Cartesian gat ->
          Printf.sprintf
            "%s %s"
            (Highlight.keyword "cartesian")
            (Global_algebraic_type.repr gat)
        | Cocartesian gat ->
          Printf.sprintf
            "%s %s"
            (Highlight.keyword "cocartesian")
            (Global_algebraic_type.repr gat)
      ;;
    end
  end

  module Statement = struct
    type t =
      | Comment of string
      | Let of Definition.Let.t
      | Type of Definition.Type.t

    let let' (binding : Name.t) (body : Term.t) : t = Let { binding; body }

    let cartesian_type
          (binding : Name.t)
          (axes : Name.t list)
          (origin : Definition.Origin.t)
          (units : Definition.Unit.t list)
      : t
      =
      Type (Cartesian { binding; axes; origin; units })
    ;;

    let cocartesian_type
          (binding : Name.t)
          (axes : Name.t list)
          (origin : Definition.Origin.t)
          (units : Definition.Unit.t list)
      : t
      =
      Type (Cocartesian { binding; axes; origin; units })
    ;;

    let repr : t -> string = function
      | Comment content -> Printf.sprintf "%s" (Highlight.comment (";; " ^ content))
      | Let definition -> Definition.Let.repr definition
      | Type definition -> Definition.Type.repr definition
    ;;
  end

  module Program = struct
    type t = Statement.t list

    let repr : t -> string = function
      | [] -> "(empty)"
      | program -> program |> List.map Statement.repr |> String.concat "\n"
    ;;
  end

  module Diagnosis = struct
    type t =
      | Argument_type_mismatch of kind_mismatch
      | Duplicate_axis of axis_info
      | Invalid_origin_type of kind_mismatch
      | Invalid_unit_codomain of kind_mismatch
      | Name_not_found of Name.t
      | Non_functional_application of term_info
      | Unbound_axis of Name.t

    and kind_mismatch =
      { expected : Kind.t
      ; found : Kind.t
      }

    and term_info =
      { term : Term.t
      ; kind : Kind.t
      }

    and axis_info =
      { name : Name.t
      ; kind_name : Name.t
      }

    let repr (diagnosis : t) : string =
      match diagnosis with
      | Argument_type_mismatch { expected; found } ->
        Printf.sprintf
          "I expected an argument of type %s, but I found %s"
          (Kind.repr expected)
          (Kind.repr found)
      | Duplicate_axis { name; kind_name } ->
        Printf.sprintf
          "I found the axis %s more than once in the definition of the type %s ; axes \
           should be unique"
          (Name.repr name)
          (Highlight.type' kind_name)
      | Invalid_origin_type { expected; found } ->
        Printf.sprintf
          "I expected the origin to be of type %s, but I found %s"
          (Kind.repr expected)
          (Kind.repr found)
      | Invalid_unit_codomain { expected; found } ->
        Printf.sprintf
          "I expected the unit constructor to produce a value of type %s (directly or \
           after an application) but its type is %s"
          (Kind.repr expected)
          (Kind.repr found)
      | Name_not_found name ->
        Printf.sprintf "I couldn't find the name %s" (Name.repr name)
      | Non_functional_application { term; kind } ->
        Printf.sprintf
          "the term %s (of type %s) is not a function ; it cannot be applied"
          (Term.repr term)
          (Kind.repr kind)
      | Unbound_axis axis ->
        Printf.sprintf
          "I found use of an axis %s, but it doesn't exist in this scope"
          (Highlight.name axis)
    ;;
  end

  module Diagnostic = struct
    type t =
      { diagnosis : Diagnosis.t
      ; mutable source : Statement.t option
      }

    let repr (diagnostic : t) : string =
      let buffer = Buffer.create 64 in
      let write = Buffer.add_string buffer in
      write
      @@ Printf.sprintf
           "%s %s"
           (Highlight.error "error:")
           (Diagnosis.repr diagnostic.diagnosis);
      (match diagnostic.source with
       | Some statement -> write @@ Printf.sprintf "\n  | %s" (Statement.repr statement)
       | None -> ());
      Buffer.contents buffer
    ;;
  end

  module Review = struct
    type t =
      { decision : [ `Pass | `Abort ]
      ; details : string option
      }

    let print ?(out : out_channel = stderr) (review : t) : unit =
      match review.decision with
      | `Pass ->
        Printf.fprintf
          out
          "%s no type error found in the program\n"
          (Highlight.success "success:")
      | `Abort ->
        (match review.details with
         | None -> ()
         | Some content -> Printf.fprintf out "%s\n" content);
        Printf.fprintf out "\n%s\n" (Highlight.error "Aborted.")
    ;;
  end

  module Doctor = struct
    type t = { mutable diagnostics : Diagnostic.t list }

    let create () : t = { diagnostics = [] }

    let add_diagnostic
          ?(source : Statement.t option)
          (diagnosis : Diagnosis.t)
          (doctor : t)
      : unit
      =
      doctor.diagnostics <- { diagnosis; source } :: doctor.diagnostics
    ;;

    let review (doctor : t) : Review.t =
      let decision = if List.is_empty doctor.diagnostics then `Pass else `Abort in
      let details =
        doctor.diagnostics
        |> List.rev
        |> List.map_on_cons Diagnostic.repr
        |> Option.map (String.concat "\n")
      in
      { decision; details }
    ;;
  end

  module Context = Quickmap.Make (Name) (Kind)

  class analyzer ?(context : Context.t = Context.empty) ~(doctor : Doctor.t) () =
    object (self)
      val mutable context = context
      val doctor = doctor

      (* term checking *)

      method fetch_term (name : Name.t) : Kind.t option = Context.get name context

      method infer_kind_of_term (term : Term.t) : Kind.t =
        match term with
        | App (function', argument) -> self#apply_term function' argument
        | Fun (parameters, body) ->
          let body_kind = self#infer_kind_of_term body in
          (match parameters with
           | [] -> body_kind
           | first :: rest ->
             let first_parameter_kind = self#infer_kind_of_parameter first in
             Arrow (first_parameter_kind, self#infer_kind_of_term (Fun (rest, body))))
        | Var name ->
          self#fetch_term name
          |> Option.on_none (fun () -> Doctor.add_diagnostic (Name_not_found name) doctor)
          |> Option.value ~default:Bottom

      method infer_kind_of_parameter (parameter : Parameter.t) : Kind.t =
        match parameter with
        | Named (_, kind) -> kind

      method apply_term (function' : Term.t) (argument : Term.t) : Kind.t =
        let function_kind = self#infer_kind_of_term function' in
        let argument_kind = self#infer_kind_of_term argument in
        if Kind.is_bottom argument_kind
        then Bottom
        else self#apply_kind function_kind argument_kind

      method apply_kind (function_kind : Kind.t) (argument_kind : Kind.t) : Kind.t =
        match function_kind with
        | Var name ->
          let function_resolved_maybe = self#fetch_term name in
          (match function_resolved_maybe with
           | None ->
             Doctor.add_diagnostic (Name_not_found name) doctor;
             Bottom
           | Some function_resolved -> self#apply_kind function_resolved argument_kind)
        | Axial (subkind, _) ->
          (* if the function itself is axis-bound it doesn't really matter *)
          self#apply_kind subkind argument_kind
        | Arrow (left, right) ->
          if self#check_kind ~expected:left argument_kind
          then right
          else (
            Doctor.add_diagnostic
              (Argument_type_mismatch { expected = left; found = argument_kind })
              doctor;
            Bottom)
        | Product _ ->
          Doctor.add_diagnostic
            (Non_functional_application { term = Var "???"; kind = function_kind })
            doctor;
          Bottom
        | Bottom -> Bottom

      method check_term ~(expected : Term.t) (found : Term.t) : bool =
        match expected, found with
        | App (function_expected, argument_expected), App (function_found, argument_found)
          ->
          self#check_term ~expected:function_expected function_found
          && self#check_term ~expected:argument_expected argument_found
        | Fun (parameters_expected, body_expected), Fun (parameters_found, body_found) ->
          List.for_all2
            (fun expected -> self#check_parameter ~expected)
            parameters_expected
            parameters_found
          && self#check_term ~expected:body_expected body_found
        | Var name_expected, Var name_found -> Name.(name_expected = name_found)
        | _, _ -> false

      method check_kind ~(expected : Kind.t) (found : Kind.t) : bool =
        match expected, found with
        | Arrow (left_expected, right_expected), Arrow (left_found, right_found) ->
          self#check_kind ~expected:left_expected left_found
          && self#check_kind ~expected:right_expected right_found
        | Axial (subkind_expected, axes_expected), Axial (subkind_found, axes_found) ->
          self#check_kind ~expected:subkind_expected subkind_found
          && List.for_all (fun axis -> List.mem axis axes_found) axes_expected
        | Product (left_expected, right_expected), Product (left_found, right_found) ->
          self#check_kind ~expected:left_expected left_found
          && self#check_kind ~expected:right_expected right_found
        | Var name_expected, Var name_found -> Name.(name_expected = name_found)
        | _, Axial (type_found, _) ->
          (* "axis surplus" is fine *)
          self#check_kind ~expected type_found
        | _, _ -> false

      method check_parameter ~(expected : Parameter.t) (found : Parameter.t) : bool =
        match expected, found with
        | Named (_, kind_expected), Named (_, kind_found) ->
          self#check_kind ~expected:kind_expected kind_found

      (* statement checking *)

      method check_duplicate_axes (gat : Definition.Global_algebraic_type.t) : unit =
        let axes_count = List.count_elements gat.axes in
        axes_count
        |> List.filter (fun (_, count) -> count > 1)
        |> List.iter (fun (name, count) ->
          Doctor.add_diagnostic (Duplicate_axis { name; kind_name = gat.binding }) doctor)

      method check_origin_definition
        (origin : Definition.Origin.t)
        ~from:(gat : Definition.Global_algebraic_type.t)
        : bool =
        self#check_kind ~expected:(Var gat.binding) origin.annotation
        |> Bool.on_false (fun () ->
          Doctor.add_diagnostic
            (Invalid_origin_type { expected = Var gat.binding; found = origin.annotation })
            doctor)

      method check_unit_return_kind (return_kind : Kind.t) (gat : Kind.t) : bool =
        match return_kind with
        | Arrow (_, right) -> self#check_unit_return_kind right gat
        | Axial (subkind, _) -> self#check_unit_return_kind subkind gat
        | Var _ -> self#check_kind ~expected:gat return_kind
        | Product _ -> false
        | Bottom ->
          failwith "bottom leak: it should not be possible to use ⊥ in user code"

      method check_unit_definition
        (unit : Definition.Unit.t)
        ~from:(gat : Definition.Global_algebraic_type.t)
        : bool =
        List.mem unit.axis gat.axes
        |> Bool.on_false (fun () -> Doctor.add_diagnostic (Unbound_axis unit.axis) doctor)
        && self#check_unit_return_kind unit.annotation (Var gat.binding)
           |> Bool.on_false (fun () ->
             Doctor.add_diagnostic
               (Invalid_unit_codomain
                  { expected = Var gat.binding; found = unit.annotation })
               doctor)

      method constrain_kind (return_kind : Kind.t) (axis : Name.t) : Kind.t =
        match return_kind with
        | Arrow (left, right) ->
          Arrow (self#constrain_kind left axis, self#constrain_kind right axis)
        | Axial (subkind, axes) -> Axial (subkind, axis :: axes)
        | _ -> Axial (return_kind, [ axis ])

      method get_unit_kind
        (unit : Definition.Unit.t)
        (gat : Definition.Global_algebraic_type.t)
        ~(is_cocartesian : bool)
        : Kind.t =
        if self#check_unit_definition unit ~from:gat
        then
          if is_cocartesian
          then self#constrain_kind unit.annotation unit.axis
          else unit.annotation
        else Bottom

      method check_global_algebraic_type_definition
        ?(is_cocartesian : bool = false)
        (gat : Definition.Global_algebraic_type.t)
        : unit =
        let open Kind.Notation in
        (* 1) no duplicate axes *)
        self#check_duplicate_axes gat;
        (* 2) valid origin *)
        let origin_kind =
          if self#check_origin_definition gat.origin ~from:gat
          then gat.origin.annotation @ gat.axes
          else Bottom
        in
        context <- Context.add gat.origin.name origin_kind context;
        (* 3) valid units *)
        List.iter
          (fun (unit : Definition.Unit.t) ->
             context
             <- Context.add
                  unit.name
                  (self#get_unit_kind ~is_cocartesian unit gat)
                  context)
          gat.units

      method check_type_definition (type' : Definition.Type.t) : unit =
        match type' with
        | Cartesian gat -> self#check_global_algebraic_type_definition gat
        | Cocartesian gat ->
          self#check_global_algebraic_type_definition ~is_cocartesian:true gat

      method check_statement (statement : Statement.t) : unit =
        match statement with
        | Comment _ -> ()
        | Let { binding; body } ->
          let body_type = self#infer_kind_of_term body in
          context <- Context.add binding body_type context
        | Type type' -> self#check_type_definition type'

      method check_program (program : Program.t) : unit =
        match program with
        | [] -> ()
        | first :: rest ->
          self#check_statement first;
          self#check_program rest
    end
end

open Core

let nat = Kind.var "Nat"
let int = Kind.var "Int"
let plane = Kind.var "Plane"

let program : Program.t =
  [ Statement.cartesian_type
      "Plane"
      [ "x"; "y" ]
      { name = "Origin"; annotation = plane }
      [ { name = "Right"; axis = "x"; annotation = Arrow (plane, plane) }
      ; { name = "Up"; axis = "y"; annotation = Arrow (plane, plane) }
      ]
  ; Statement.cocartesian_type
      "Int"
      [ "x"; "y" ]
      { name = "O"; annotation = int }
      [ { name = "S"; axis = "x"; annotation = Arrow (int, int) }
      ; { name = "P"; axis = "y"; annotation = Arrow (int, int) }
      ]
  ; Comment "this is fine"
  ; Statement.let' "bar" (App (Var "Up", App (Var "Right", Var "Origin")))
  ; Comment "this is not"
  ; Statement.let' "impossible" (App (Var "P", App (Var "S", Var "O")))
  ]
;;

let doctor = Doctor.create ()
let analyzer = new analyzer ~doctor ()
let () = Printf.printf "%s\n" (Program.repr program)
let () = Printf.printf "%s\n" (String.make 40 '-')
let () = analyzer#check_program program
let () = Review.print (Doctor.review doctor)

Quickmap.ml

module type REPRESENTABLE = sig
  (** The showable type. *)
  type t

  (** [repr value] produces a pretty-printable representation
      of [value]. *)
  val repr : t -> string
end

module type TYPE = sig
  (** The [key] of the mapping. *)
  type key

  (** The [value] of the mapping. *)
  type value

  (** The mapping. *)
  type t

  (** A empty mapping. *)
  val empty : t

  (** [keys mapping] returns a list of the mapping keys. *)
  val keys : t -> key list

  (** [values mapping] returns a list of the mapping values. *)
  val values : t -> value list

  (** [get key mapping] returns the value associated with the
      [key] in the [mapping] if any. Returns [None] otherwise.*)
  val get : key -> t -> value option

  (** [add key value mapping] adds a [key] associated with
      [value] in the [mapping]. *)
  val add : key -> value -> t -> t

  (** [update key value mapping] updates the associated [value]
      of [key] if it exists in the [mapping]. *)
  val update : key -> value -> t -> t

  (** [concat mapping1 mapping2] returns a new mapping
      containing the entries of the two. *)
  val concat : t -> t -> t

  val repr : t -> string
end

module Make (Key : REPRESENTABLE) (Value : REPRESENTABLE) :
  TYPE with type key = Key.t with type value = Value.t = struct
  type key = Key.t
  type value = Value.t
  type t = (key * value) list

  let empty = []
  let keys = List.map fst
  let values = List.map snd
  let get = List.assoc_opt

  let[@tail_mod_cons] rec update =
    fun key value mapping ->
    match mapping with
    | [] -> []
    | (key', _) :: rest when key = key' -> (key, value) :: rest
    | (key', value') :: rest -> (key', value') :: update key value rest
  ;;

  let add = fun key value mapping -> (key, value) :: mapping
  let concat = List.append

  let repr mapping =
    match mapping with
    | [] -> "[:]"
    | _ ->
      mapping
      |> List.rev_map (fun (key, value) ->
        Printf.sprintf "%s : %s" (Key.repr key) (Value.repr value))
      |> String.concat "; "
      |> Printf.sprintf "[ %s ]"
  ;;
end

screenshot.png