Skip to content

Instantly share code, notes, and snippets.

@TimWSpence
Created March 1, 2021 14:09
Show Gist options
  • Save TimWSpence/03b3377653ba656826a84f5b34a9078e to your computer and use it in GitHub Desktop.
Save TimWSpence/03b3377653ba656826a84f5b34a9078e to your computer and use it in GitHub Desktop.
let Tree
: Type Type
= λ(Elem : Type)
(T : Type) (Branch : Elem T T T) (Leaf : T) T
let showTree =
λ(elem : Type)
λ(show : elem Text)
λ(tree : Tree elem)
tree
Text
( λ(e : elem)
λ(l : Text)
λ(r : Text)
"(Branch '${show e}' ${l} ${r})"
)
"Leaf"
let tree
: Tree Text
= λ(t : Type)
λ(Branch : Text t t t)
λ(Leaf : t)
Branch "foo" (Branch "bar" Leaf Leaf) Leaf
let identity = λ(A : Type) λ(a : A) a
in showTree Text (identity Text) tree
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment