Formality to Formality-Core Cheat Sheet

fm_to_fmc_cheatsheet.md

Criando funções

// Formality:

T V3
| v3(x: Number, y: Number, z: Number) 

add_v3(a: V3, b: V3) : V3
  case a |v3
  case b |v3
  v3(a.x + b.x, a.y + b.y, a.z + b.z)

// Formality-Core:

add_v3: (a: V3) -> (b : V3) -> V3
  (a) (b)
  a<() V3>
  | (a.x) (a.y) (a.z)
    b<() V3>
    | (b.x) (b.y) (b.z)
      let c.x = F64.add(a.x)(a.y)
      let c.y = F64.add(a.y)(b.y)
      let c.z = F64.add(a.z)(b.z)
      v3(c.x)(c.y)(c.z)
    ;
  ;

... ou ...

add_v3: (a: V3) -> (b : V3) -> V3
  (a) (b)
  a<() V3> | (a.x) (a.y) (a.z)
  b<() V3> | (b.x) (b.y) (b.z)
  let c.x = F64.add(a.x)(a.y)
  let c.y = F64.add(a.y)(b.y)
  let c.z = F64.add(a.z)(b.z)
  v3(c.x)(c.y)(c.z);;

// Formality:

T Nat
| zero
| succ(pred: Nat)

pred(n: Nat) : Nat
  case n
  | zero => zero
  | succ => n.pred

// Formality-Core:

pred : (n: Nat) -> Nat
  (n)
  n<() Nat>
  | zero;
  | (n.pred) n.pred;

...ou...

pred : (n: Nat) -> Nat
  (n)
  n<() Nat>(zero)((n.pred) n.pred)

// Formality

map(A; B; fn: A -> B, xs: List(A)) : List(B)
  case xs
  | nil  => []
  | cons => cons(_ fn(xs.head), map(__ fn, xs.tail))

// Formality-Core

map: <A: Type> -> <B: Type> -> (fn: A -> B) -> (xs: List(A)) -> List(B)
  <A> <B> (fn) (xs)
  xs<() List(B)>
  | List.nil;
  | (xs.head) (xs.tail) List.cons<B>(fn(xs.head))(map<A><B>(fn)(xs.tail));

// Formality

if eql_v3(a, b) then
  c
else
  norm_v3(sub_v3(b, a))

// Formality-Core

F64.if<V3>(eql_v3(a)(b))
| c;
| norm_v3(sub_v3(b)(a));

Criando tipos

T Bool
| true
| false

T Nat
| zero
| succ(pred: Nat)

T V3
| new(x: Number, y: Number, z: Number) 

1. Primeira linha: NOME : Type

   Bool: Type
   
   Nat: Type
   
   V3: Type
   

2. Adiciona o motive: nome<P: Nome -> Type> ->

   Bool: Type
     bool<P: Bool -> Type> ->
   
   Nat: Type
     nat<P: Bool -> Type> ->
   
   V3: Type
     v3<P: V3 -> Type> ->
   

3. Adiciona cada construtor: (ctor: ) ->

   Bool: Type
     bool<P: Bool -> Type> ->
     (true: ) ->
     (false: ) ->
   
   Nat: Type
     nat<P: Bool -> Type> ->
     (zero: ) ->
     (succ: ) ->
   
   V3: Type
     v3<P: V3 -> Type> ->
     (new: ) ->
   

4. Adiciona cada campo de cada construtor:

   Bool: Type
     bool<P: Bool -> Type> ->
     (true: ) ->
     (false: ) ->
   
   Nat: Type
     nat<P: Bool -> Type> ->
     (zero: ) ->
     (succ: (pred: Nat) -> ) ->
   
   V3: Type
     v3<P: V3 -> Type> ->
     (new: (x: F64) -> (y: F64) -> (z: F64) -> ) ->
   

5. Adiciona o retorno de cada contrutor: P(Nome.ctor(campo0)(campo1)(...))

   Bool: Type
     bool<P: Bool -> Type> ->
     (true: P(Bool.true)) ->
     (false: P(Bool.false)) ->
   
   Nat: Type
     nat<P: Bool -> Type> ->
     (zero: P(Nat.zero)) ->
     (succ: (pred: Nat) -> P(Nat.succ(pred))) ->
   
   V3: Type
     v3<P: V3 -> Type> ->
     (new: (x: F64) -> (y: F64) -> (z: F64) -> P(V3.new(x)(y)(z)) ->
   

6: Adiciona o retorno do tipo: P(nome)

```
Bool: Type
  bool<P: Bool -> Type> ->
  (true: P(Bool.true)) ->
  (false: P(Bool.false)) ->
  P(bool)

Nat: Type
  nat<P: Bool -> Type> ->
  (zero: P(Nat.zero)) ->
  (succ: (pred: Nat) -> P(Nat.succ(pred))) ->
  P(nat)

V3: Type
  v3<P: V3 -> Type> ->
  (new: (x: F64) -> (y: F64) -> (z: F64) -> P(V3.new(x)(y)(z)) ->
  P(v3)
```

7: Adiciona os construtores em arquivos separados:

```
Bool.true:

Bool.false:

Nat.zero:

Nat.succ:

V3.new:
```

8: Adiciona o tipo dos construtores:

```
Bool.true: Bool

Bool.false: Bool

Nat.zero: Nat

Nat.succ: Nat -> Nat

V3.new: F64 -> F64 -> F64 -> V3
```

9: Adiciona os campos de cada construtor:

```
Bool.true: Bool

Bool.false: Bool

Nat.zero: Nat

Nat.succ: Nat -> Nat
  (pred)

V3.new: F64 -> F64 -> F64 -> V3
  (x) (y) (z)
```

10: Adiciona o <P>

```
Bool.true: Bool
  <P>

Bool.false: Bool
  <P>

Nat.zero: Nat
  <P>

Nat.succ: Nat -> Nat
  (pred)
  <P>

V3.new: F64 -> F64 -> F64 -> V3
  (x) (y) (z)
  <P>
```

11. Adiciona um lambda pra cada construtor do tipo:

    Bool.true: Bool
      <P> (true) (false)
    
    Bool.false: Bool
      <P> (true) (false)
    
    Nat.zero: Nat
      <P> (zero) (succ)
    
    Nat.succ: Nat -> Nat
      (pred)
      <P> (zero) (succ)
    
    V3.new: F64 -> F64 -> F64 -> V3
      (x) (y) (z)
      <P> (new)
    

12. Adiciona o construtor certo aplicado aos campos:

    Bool.true: Bool
      <P> (true) (false)
      true
    
    Bool.false: Bool
      <P> (true) (false)
      false
    
    Nat.zero: Nat
      <P> (zero) (succ)
      zero
    
    Nat.succ: Nat -> Nat
      (pred)
      <P> (zero) (succ)
      succ(pred)
    
    V3.new: F64 -> F64 -> F64 -> V3
      (x) (y) (z)
      <P> (new)
      new(x)(y)(z)
    

Fim!

T Maisa
| com_maisa(blabla: Number, belanna: String)
| sem_maisa(neelix: String)

T Yuri
| com_yuri(blabla: Number, max: String)
| sem_yuri(montanha: String)

github.com/moonad/moonad

Maisa.fmc
Maisa.com_maisa.fmc
Maisa.sem_maisa.fmc

Yuri.fmc
Yuri.com_yuri.fmc
Yuri.sem_yuri.fmc

instalando

npm i -g formality-core

type-checking, só rodar:

fmc