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

EduardoRFS

module Unify = struct
  type typ =
    | T_var of int
    | T_hole of hole ref
    | T_forall of typ
    | T_arrow of typ * typ

  and hole = H_open of int | H_link of typ * int
  
  let rec occurs h_off h in_off in_ =

EduardoRFS

module Main : sig
  val sum_before_and_after : before:int -> after:int -> int
end = struct
  module Context : sig
    type error
    type context

    val return : int -> context
    val bind : context -> (int -> context) -> context
    val level : (level:int -> context) -> context

EduardoRFS

Examples

[@import stdlib.http.v1];

(x => y => (x_plus_y: x + y) => );

((A, x))
(f: () -> (A: *, x: A)) =>
  (A, x) = (f ());

EduardoRFS

type term = Var of string | Lam of string * term | App of term * term
type value = Closure of ((string * value) list * string * term)

let rec eval env term =
  match term with
  | Var var -> List.assoc var env
  | Lam (param, body) -> Closure (env, param, body)
  | App (lambda, argument) -> (
      let lambda = eval env lambda in
      let argument = eval env argument in

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

const one: number = 1;
const a: string = "a";
type Id = <A>(a: A) => A;
const id: Id = (a) => a;
type Apply = <A, B>(f: (a: A) => B, a: A) => B;
const apply: Apply = (f, a) => f(a);
type Never_implies_anything = <A>(a: never) => A;
const never_implies_everything = <A>(a: never) => a as A;
type Not<A> = (a: A) => never;
const not_never: Not<never> = (a) => a;

EduardoRFS

type Eq<A, B> = <X>(a: A, eq: (x: A & B) => X) => X;
const refute = (x: never) => x;
const refl = <A, X>(a: A, eq: (x: A) => X) => eq(a);

const sickos = <A>(x: A, eq: Eq<A, number>) => eq(x, (x) => x);
const two = sickos(2, refl);

type Ty<A> =
  | { tag: "number"; eq: Eq<A, number> }
  | { tag: "string"; eq: Eq<A, string> };