Skip to content

Instantly share code, notes, and snippets.

View johnchandlerburnham's full-sized avatar
💭
Λ∀

John Chandler Burnham johnchandlerburnham

💭
Λ∀
View GitHub Profile
@johnchandlerburnham
johnchandlerburnham / HIT.fmc
Created April 15, 2020 06:59
HIT.fmc
Equal: (A: Type) -> A -> A -> Type
(A) (a) (b)
equal_value<P: (b: A) -> Equal(A)(a)(b) -> Type> ->
(equal: P(a)(equal<A><a>)) ->
P(b)(equal_value)
equal: <A: Type> -> <a: A> -> Equal(A)(a)(a)
<A> <a>
<P> (equal)
@johnchandlerburnham
johnchandlerburnham / FiniteEndoTypes.fm
Last active April 15, 2020 13:55
FiniteEndoTypes
module FiniteEndoTypes where
import System.IO
-- for any finite n, there are n^n mappings from the set with n elements to
-- itself
-- for n == 2
-- {0,1} -> {0,0} 0
-- {0,1} -> {0,1} 1
@johnchandlerburnham
johnchandlerburnham / ticTac15.fm
Last active January 29, 2020 03:19
A Formality proof that TicTacToe winning lines are isomorphic to the 3x3 magic square.
import Base#
// There are eight possible winning lines in a game of tic-tac-toe
// ----------------
// | 00 | 01 | 02 |
// -----+----+-----
// | 10 | 11 | 12 |
// -----+----+-----
// | 20 | 21 | 22 |
// ----------------
@johnchandlerburnham
johnchandlerburnham / wasm-i64-f64.md
Last active December 5, 2019 00:48
wasm i64 and f64 ops

i64, 29 ops

Op Signature
i64.eqz [i64] -> i32
i64.eq [i64,i64] -> i32
i64.ne [i64,i64] -> i32
i64.lt_s [i64,i64] -> i32
i64.lt_u [i64,i64] -> i32
i64.gt_s [i64,i64] -> i32
@johnchandlerburnham
johnchandlerburnham / STYLE.md
Last active November 19, 2019 22:51
Formality style

A Formality Style Guide

"considering making single-line definitions with ; a syntax error to stop your kingdom of evil" --Victor Maia

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC 2119

@johnchandlerburnham
johnchandlerburnham / fm-net-c.wat
Last active November 15, 2019 06:35
fm-net-c.wat
(module
(type (;0;) (func (param i32)))
(type (;1;) (func (result i32)))
(type (;2;) (func (param i32) (result i32)))
(type (;3;) (func (param f64) (result f64)))
(type (;4;) (func (param f64 f64) (result f64)))
(type (;5;) (func (param f64 f64) (result i64)))
(type (;6;) (func (param i32 i32 i32 i32) (result i32)))
(type (;7;) (func (param f64 f64) (result i32)))
(type (;8;) (func (param i32 i32 i32 i32) (result f64)))
@johnchandlerburnham
johnchandlerburnham / Data.Array.fm
Created November 7, 2019 21:19
Data.Array
import Data.Nat
import Data.InductionTree
Array : {A : Type, n : Nat} -> Type
case/Nat n
| succ => [x : Array(A, n.pred), Array(A, n.pred)]
| zero => A
: Type
// ::::::::::
@johnchandlerburnham
johnchandlerburnham / funext_functor.fm
Created October 20, 2019 16:37
The effect intensionality has on Functors
import Relation.Binary
import Relation.Equality
// identity function
id : {~A : Type, x:A} -> A
x
// composition function
compose : {~A : Type, ~B : Type, ~C : Type, g : B -> C, f : A -> B, x : A} -> C
g(f(x))
@johnchandlerburnham
johnchandlerburnham / HIT.fm
Created October 19, 2019 18:42
more funext
import Data.Empty
import Data.Unit
Interval : Type
$self
{ ~P : {i : Interval} -> Type
, I0 : P(i0)
, I1 : P(i1)
, ~SG : I0 == I1
} -> [x : P(self) ~ I0 == I1]
@johnchandlerburnham
johnchandlerburnham / funext.fm
Last active October 18, 2019 21:30
Why we want functional Extentionality in formality
// Let's start our lawful Functor abstraction
T Functor {F : Type -> Type}
| functor
{ map : {~A : Type , ~B : Type , f : A -> B, x : F(A)} -> F(B)
, identity : {~A : Type , fa : F(A)} -> map(~A, ~A, id(~A),fa) == fa
, composition :
{ ~A : Type
, ~B : Type
, ~C : Type