EduardoRFS

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

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

  module Map = Map.Make (String)
end

module Var : sig

EduardoRFS

Roadmap

Geral

O que é uma linguagem de programação?

Linguagens de programação não são algo especial. "code is data".

Como representar código / AST

Interpretando aritmética

EduardoRFS

Examples

[@import stdlib.http.v1];

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

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

EduardoRFS

Resumo

• criar partições
• montar partições
• instalar sistema
• configurar hora
• configurar rede
• configurar localização
• configurar usuario e sudo
• configurar grub

EduardoRFS

type NatModule<Nat> = {
  
  zero: Nat;
  one: Nat;
  add: (x: Nat, y: Nat) => Nat;
};

const NatModule = <A>(cb: <Nat>(Nat: NatModule<Nat>) => A) => {
  const zero = 0;
  const one = 1;

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.

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