Created
March 1, 2021 14:09
-
-
Save TimWSpence/03b3377653ba656826a84f5b34a9078e to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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