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

We should kill Prop

Notação

Irei estar usando letras maiusculas para tipos e minusculas para o que não é um tipo ou é desconhecido.

Funções: (x : A) -> B === ∏x:A. B, uma função que aceita x de um tipo A e retorna algo do tipo B, também chamado de abstração, a variável pode ser omitida quando ela não aparece em B A -> B. Implicito: {x : A} -> B, uma função aonde o parametro é implicito, aka o compilador irá achar o argumento. Módulo: (x : A, B) === Σx:A. B, um módulo aonde a esquerda x tem um tipo A e a direita algo do tipo B, também chamado de par, módulos podem ser transparentes tendo a forma de (x : A = v, B.

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) => {

EduardoRFS

Γ, 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

!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

Γ, 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

bindsym --release $mod+F11 exec "xdotool key F11; i3-msg fullscreen disable"

# Start i3bar to display a workspace bar (plus the system information i3status
# finds out, if available)
bar {
        status_command i3status
        position top
}

#interactive screenshot by pressing printscreen

EduardoRFS

// 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

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++) {