Skip to content

Instantly share code, notes, and snippets.

View EduardoRFS's full-sized avatar
♥️
Laughing at the abysm

Eduardo Rafael EduardoRFS

♥️
Laughing at the abysm
990 followers · 114 following
View GitHub Profile
@EduardoRFS
EduardoRFS / cps_sigma.md
Last active July 29, 2023 16:54

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
EduardoRFS / frozen_nominal.md
Created July 3, 2023 20:53 
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) => {
@EduardoRFS
EduardoRFS / simplest_fix.md
Created June 27, 2023 05:04 
Γ, x : %self(x). T |- T : Type
------------------------------
%self(x). T : Type

Γ, x : %self(x). T |- M : T[x := %fix(x) : T. M]
------------------------------------------------
%fix(x) : T. M : %self(x). T

Γ |- M : %self(x). T
@EduardoRFS
EduardoRFS / no_internal_equality.md
Last active June 27, 2023 05:02 
!Unit ===
  %self(u). (P : %unroll Unit I_Unit unit I_unit -> Type) ->
    %unroll I_Unit unit I_unit P (%unroll unit I_unit) ->
    %unroll I_Unit unit I_unit P u;
!T_I_Unit ===
  %self(I_Unit). (unit : !T_unit) -> (I_unit : !T_I_unit) ->
    (P : %unroll Unit I_Unit unit I_unit -> Type) -> !Unit -> Type;
!T_unit ===
 %self(unit). (I_unit : !T_I_unit) -> !Unit;
@EduardoRFS
EduardoRFS / controlled_fix.md
Created June 25, 2023 23:56 
Γ, x : %self(x). T |- T : Type
------------------------------
%self(x). T : Type

Γ, x : %self(x). T,
  eq : %self(eq). (P : T -> Type) -> P (%unroll x) -> P M |- M : T[x := M]
--------------------------------------------------------------------------
%fix(self%x : T, eq). M : %self(x). T
@EduardoRFS
EduardoRFS / bronen.ts
Created March 28, 2023 23:39
// EXAMPLE: (1 (2 3 *) +)
// ((1 (2 3 +) +) 4 +)
const exhaustive = <A>(x: never): A => x;
// interpreter
type Expression =
| { tag: "literal"; value: number }
| { tag: "operation"; operation: Operation };
@EduardoRFS
EduardoRFS / not_meaningful.md
Created March 11, 2023 18:21 
const flatArgsCore = (a, b) => a + b;
const objArgsCore = ({ a, b }) => a + b;
const size = 1e6;
const dataA = new Array(1e6).fill(0).map((_) => Math.random());
const dataB = new Array(1e6).fill(0).map((_) => Math.random());

const flatArgsAcc = () => {
  let acc = 0;
  for (let i = 0; i < 1e5; i++) {
@EduardoRFS
EduardoRFS / macabas.ts
Created March 10, 2023 17:29
const f = <
A extends "number" | "string",
T extends A extends "number" ? number : A extends "string" ? string : never
>(
_: A,
x: T
) => x;
const a = f("number", 1);
const b = f("string", "b");
@EduardoRFS
EduardoRFS / torrens.md
Created March 7, 2023 20:35 
((Bool,
  true : Bool,
  false : Bool,
  case : (b : Bool) -> (A : Type) -> A -> A -> A
) => M)(
  (A : Type) -> A -> A -> A,
  A => x => y => x,
  A => x => y => y,
 b =&gt; A =&gt; x =&gt; y =&gt; b A x y
@EduardoRFS
EduardoRFS / kewerson_self.md
Created March 2, 2023 16:07 
Γ, x : %self(x). T |- T : Type
------------------------------
%self(x). T : Type

fix%Unit (unit : %self(unit). %unroll Unit unit unit) (u : %self(u). %unroll Unit unit u)
  = (P : (u : %self(u). %unroll Unit unit u) -> Type) -> P unit -> P u;
fix%unit : %unroll Unit unit unit = P => x => x;

Unit = %self(u). %unroll Unit unit u;