qexat

type inhabited = Inhabited

module Hole = struct
  (* Discriminator for Done *)
  type 'ty value = Value of 'ty

  (* Discriminator for Falling *)
  type nonterm = Nonterm

  type 'value t =

qexat

let ( or ) option default = Option.value option ~default

module Int = struct
  include Int

  let compare i1 i2 =
    let as_int = compare i1 i2 in
    if as_int > 0 then `Greater else if as_int < 0 then `Less else `Equal
  ;;

qexat

jekyll: a hyper-declarative, statically-typed programming language around environment manipulation

# x is introduced to the environment
{ ..?e } → { x := 3 ; ..?e }
# y too ; ?e is not the same row variable as the one above
{ ..?e } → { y := 5 ; ..?e }
# matching the current context on one that contains an x and a y
# which allows us to add them to introduce y
{ x ; y ; ..?e } → { z := x + y ; ..?e } 

qexat

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.

qexat

Require Import String.

Inductive Term : nat -> Type :=
  | App : forall {n m : nat}, Term (S n) -> Term m -> Term (n + m)
  | Fun : forall {n : nat}, Term 0 -> Term n -> Term (S n)
  | Var : string -> Term 0.

qexat

Require Import Utf8.

(** [Eqw f x y] represents the equivalence x y up to an isomorphism f. *)
Inductive Eqw {A B : Type} (f : A → B) : A → A → Prop :=
  | Refl (x y : A) : f x = f y → Eqw f x y.

(** Notation for convenience. Same level as equality. *)
Notation "x = y 'up' 'to' f" := (Eqw f x y).

(** Utilitary functions for the theorems below. *)

qexat

tokens:
  INFINITY ≔ '∞'
  ZERO ≔ '0'
  ONE ≔ '1'
  NONZERO ≔ /[1-9][0-9]*/
  QUESTION_MARK ≔ '?'
  BANG ≔ '!'

  NAME ≔ /[A-Za-z_][A-Za-z0-9_']*/
  CONTAINS ≔ '∋'

qexat

module Option = struct
  include Option

  let or_else : type item. (unit -> item t) -> item t -> item t =
    fun rightf left ->
    match left with
    | None -> rightf ()
    | _ -> left
  ;;

qexat

let get_char () =
  let attr = Unix.tcgetattr Unix.stdin in
  let () =
    Unix.tcsetattr
      Unix.stdin
      Unix.TCSADRAIN
      { attr with Unix.c_icanon = false }
  in
  let res = input_byte stdin in
  Unix.tcsetattr Unix.stdin Unix.TCSADRAIN attr;

qexat

module type TYPE = sig
  type t
end

type 't module' = (module TYPE with type t = 't)
type 'a first = 'b constraint 'a = 'b * _
type 'a second = 'c constraint 'a = _ * 'c

module Runtype = struct
  type 'a t =