{{ message }}

Instantly share code, notes, and snippets.

# MaiaVictor

Last active Oct 17, 2020
pretty printing goals is hard
View gist:868e9a03d81a5791349c22981f6459d4
 // Equal Nat (id (succ n)) (succ n) // ~ deref:id // Equal Nat ((λn => n zero (λ pred => succ (id pred))) (succ n)) (succ n) // ~ simplify // Equal Nat (succ n zero (λ pred => succ (id pred))) (succ n) // ~ deref:succ // Equal Nat ((λ n z s => s n) n zero (λ pred => succ (id pred))) (succ n) // ~ simplify // Equal Nat ((λ pred => succ (id pred)) n) (succ n) // ~ simplify
Created Sep 16, 2020
Why I think the λ-calculus is "wrong"
View wrong_lambda_calculus.md

Mind the following, non-polymorphic, high-order λ-term representation:

``````data term
= lam (term -> term)
| app term term
``````

In the λ-calculus, you can write a HOAS interpreter like:

``````norm : term -> term
``````
Created Jul 19, 2020
View foo.js
 // Optimal Calculus terms are defined by the following grammar: // // term ::= // | λx. term -- lambda value // | ∀(x: term). term -- lambda type // | (term term) -- application // | [term,term] -- pair value // | {term,term} -- pair type // | let [x,y] = term; term -- projection // | x -- variable
Last active Sep 21, 2020
Linux experience
View linux_experience.md

## Hardware (XPS) issues:

• Trackpad is imprecise and shaky.

• Trackpad requires force to click.

• Overheats A LOT (harmfully so) under load.

Last active Jul 2, 2020
Explanation on how the lambda parser works
View lambda_parser_explanation.md
Last active Jun 26, 2020
∀ a b . a + s(b) == s(a + b)
View succ_assoc.fm.c
 Nat.succ_assoc(a: Nat, b: Nat) : Nat.add(a, Nat.succ(b)) == Nat.succ(Nat.add(a,b)) case a: | // When a is 0... // - goal: 0 + s(b) == s(0 + b) // - norm: s(b) == s(b) // Both sides equal by reduction, so `Equal.to` suffices Equal.to; | // When a is s(a.pred)... // - goal: s(a.pred) + s(b) == s(s(a.pred) + b)
Last active Jun 25, 2020
Equal in fm
View equal.fm.c
 // The equal datatype is polymorphic on a type variable A, and has two indices, // `a` and `b` of type `A` . It has only one constructor, `refl`, which // receives an argument `x : A` , and returns `Equal(A, x, x)` . In other words, // the only way to create an `Equal` is by using `refl(x)` , which sets both // indices to the same `x` , representing the notion of equalness. T Equal ~ (a: A, b: A) | refl(x: A) ~ (x, x); // With Equal, we're able to write "rewrite" as below, which substitutes an
Created Jun 23, 2020
typecase in formality
View typecase.fm
 // The Empty type has no elements. T Empty // The Unit type has 1 element. T Unit | Unit.new; // The Bool type has 2 elements. T Bool | Bool.true;
Last active Jun 27, 2020
The difference between boolean equality and type-level equality in Formality
View equality.fm.c
 // Equality with values // ==================== // A Boolean is a set with two values T Bool | true; | false; // Boolean not is a function that receives a bool and returns a bool bool_not(a: Bool): Bool
Last active Jun 21, 2020
Interfaces, traits, typeclasses, generics or whatever you call it in Formality
View traits.md

Formality doesn't have built-in typeclasses, interfaces, traits, generics or anything in special to make what those things do. Instead (like everything else), we just use plain old datatypes. Here is how:

```// We use a plain old datatype to define an "interface".
// Here, a Num is a type N that has add/sub/mul/div operations.
// We have dependent types, so you may add laws if you want!
T Num<N: Type>
| num(
add  : N -> N -> N,
mul  : N -> N -> N,```
You can’t perform that action at this time.