EduardoRFS

%{
open Tree
(*
type expr = Tree.expr =
  | Literal of int
  | Add of (expr * expr)
  | Sub of (expr * expr)
  | Mul of (expr * expr)
  | Div of (expr * expr)
*)

EduardoRFS

[@@@ocaml.warning "-37-32"]

module Name = struct
  type name = string
  type t = name

  module Map = Map.Make (String)
end

module Var : sig

EduardoRFS

Set Universe Polymorphism.

Set Primitive Projections.
Record ssig (A : Type) (P : A -> SProp) : Type := { l : A; r : P l }.

Definition C_Bool : Type := forall A, A -> A -> A.
Definition c_true : C_Bool := fun A x y => x.
Definition c_false : C_Bool := fun A x y => y.

Definition I_Bool (c_b : C_Bool) : SProp :=

EduardoRFS

```rust
// rules
// Those rules are fully church-style
Γ, x : A |- B : Type
---------------------------
Γ |- @self(x : A). B : Type

Γ, x : A |- M : B[x := @fix(x : A). M]  Γ |- A ≂ @self(x : A). B
----------------------------------------------------------------
Γ |- @fix(x : A). M : @self(x : A). B

EduardoRFS

let Closed A = ∀(G : Grade). A [G]
// closed as it is unknown how many copies it will be needed(0..1)
let Bool : Type = ∀(A : Type). Closed A -> Closed A -> Closed A
let true : Closed Bool =
  // safe to ignore y as it is used 0 times
  ΛG. [ΛA. fun x y -> let [y] = y 0 in x]
let false : Closed Bool =
  ΛG. [ΛA. fun x y -> let [y] = x 0 in y]

// same applies to nats but (0..n)

EduardoRFS

data Bool =
  Bool (exists {n : Nat} . exists {m : Nat} .
    (forall {a : Type} . a [n] -> a [m] -> a))

true : Bool
true = 
  let true_ex_m = 
    pack <0, (/\(a : Type) -> \([x] : a [1]) -> \([y] : a [0]) -> x)>
      as exists {m : Nat} .
        (forall {a : Type} . a [1] -> a [m] -> a) in

EduardoRFS

module type T = sig
  module type S
end

module T = struct
  module type S = T
end

module type K_Bool = functor (X : T) (Y : T) -> T

EduardoRFS

// hi
func (wr WorkspaceRepository) CreateWorkspace(workspace *models.Workspace) error {
  result := wr.db.Table("workspaceszz").
				Create(workspace).
				Where("foo").
				Where("foo2");
	return errors.Wrap(
    repository_utils.HandleDatabaseError(result),
		StrWorkspaceRepositoryCreateWorkspaceErr
  )

EduardoRFS

CPSify Sigma

CPSifying Sigma seems to suffer from the same issue as lambda encoding of any inductive type, which is self reference.

The lambda encodings of inductive types can be solved by using self types, instead of declaring unit using the traditional church encoding, by using self types we self encode the induction principle, allowing to be known that (u : Unit) -> u == unit.

// traditional church encoding of unit, no induction
Unit : Type;
unit : Unit;

EduardoRFS

Key : Type;
Frozen : {
  @Frozen : (A : Type, k : Key) -> Type;
  freeze : {A} -> (k : Key, x : A) -> Frozen(A, k);
  unfreeze : {A} -> (k : Key, x : Frozen(A, k)) -> A;
};

Nat_TE = ($Nat_key) => {