Skip to content

Instantly share code, notes, and snippets.

Avatar

MaiaVictor

View GitHub Profile
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
@MaiaVictor
MaiaVictor / wrong_lambda_calculus.md
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
  | bad

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

norm : term -> term
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
View linux_experience.md

The bad things:

Hardware (XPS) issues:

  • Trackpad is imprecise and shaky.

  • Trackpad requires force to click.

  • Overheats A LOT (harmfully so) under load.

@MaiaVictor
MaiaVictor / lambda_parser_explanation.md
Last active Jul 2, 2020
Explanation on how the lambda parser works
View lambda_parser_explanation.md
@MaiaVictor
MaiaVictor / succ_assoc.fm.c
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<Nat, Nat.succ(b)>;
| // When a is s(a.pred)...
// - goal: s(a.pred) + s(b) == s(s(a.pred) + b)
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: Type> ~ (a: A, b: A)
| refl(x: A) ~ (x, x);
// With Equal, we're able to write "rewrite" as below, which substitutes an
@MaiaVictor
MaiaVictor / typecase.fm
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;
@MaiaVictor
MaiaVictor / equality.fm.c
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
@MaiaVictor
MaiaVictor / traits.md
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.