EduardoRFS

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

((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 => A => x => y => b A x y

EduardoRFS

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

EduardoRFS

From Coq Require Import Strings.String.
From Coq Require Logic.FunctionalExtensionality.

Inductive ty : Type :=
  | T_Bool : ty
  | T_Arrow : ty -> ty -> ty.
Inductive expr : Type :=
  | E_var : string -> expr
  | E_app : expr -> expr -> expr
  | E_abs : string -> ty -> expr -> expr

EduardoRFS

Como Pensar

Ler e entender um pouco desse artigo. https://wiki.c2.com/?FeynmanAlgorithm

• Reconhecer como você pensa
• Descrever métodos que você usa para pensar
• Entender métodos diferentes de pensar
• Fazer perguntas sobre tudo(incluindo sobre perguntas)

Perguntas

EduardoRFS

Set Universe Polymorphism.

Definition Eq_0 {A : Type} (x y : A) := forall (P : A -> Type), P x -> P y.
Definition refl_0 {A : Type} {x : A} : Eq_0 x x := fun P p_x => p_x.

Definition Eq_1 {T_0 : Type} {T_1 : T_0 -> Type} {x_0 y_0 : T_0} (x_1 : T_1 x_0) (y_1 : T_1 y_0)
  := forall (P : forall z_0, T_1 z_0 -> Type), P x_0 x_1 -> P y_0 y_1.
Definition refl_1 {T_0 : Type} {T_1 : T_0 -> Type} {x_0 : T_0} {x_1 : T_1 x_0} : Eq_1 x_1 x_1 := fun P p_x => p_x.

EduardoRFS

// computing
C_bool = (A : Type) -> A -> A -> A;
(c_true : C_bool) = A => t => f => t;
(c_false : C_bool) = A => t => f => f;

// induction
I_bool b = (P : C_bool -> Type) -> P c_true -> P c_false -> P b;
i_true : I_bool c_true = P => p_t => p_f => p_t;
i_false : I_bool c_false = P => p_t => p_f => p_f;

EduardoRFS

// Church booleans
C_bool : Type 1 = (L : Level) -> (A : Type L) -> A -> A -> A;
c_true : Bool = L => A => t => f => t;
c_false : Bool = L => A => t => f => f;

// Induction principle
I_bool = b : Type 1 => (L : Level) -> (P : C_bool -> Type L) -> P c_true -> P c_false -> P b;
// Without IUP, Bool would be placed on Type Omega, making it useless
Bool : Type 1 = (b : Bool) & (ind : I_bool b);

EduardoRFS

refl : {A} -> A == A = _;
C_bool = {A} -> A -> A -> A;
c_true : C_bool = {A} => t => f => t;
c_false : C_bool = {A} => t => f => f;

Ind_bool : C_bool -> Type =
  b => {P} -> P c_true -> P c_false -> P b;
ind_true : Ind_bool c_true = {P} => t => f => t;
ind_false : Ind_bool c_false = {P} => t => f => f;

EduardoRFS

Teika

Uma linguagem funcional, pura, com tipos dependentes e um descendente de ML.

Convenção

Geralmente tipos e coisas que contem tipos começam com letra maiuscula. snake_case para tudo.

Features