Skip to content

Instantly share code, notes, and snippets.

@ncfavier
Last active December 25, 2021 16:11
Show Gist options
  • Save ncfavier/85ba702492479d65f679bd502ac360ea to your computer and use it in GitHub Desktop.
Save ncfavier/85ba702492479d65f679bd502ac360ea to your computer and use it in GitHub Desktop.
A very explicit bijection from Andreas Blass' "Seven Trees in One" https://arxiv.org/pdf/math/9405205.pdf
{-# LANGUAGE LambdaCase #-}
module SevenTreesInOne where
import Test.QuickCheck
infixl :*
data T = O | T :* T
deriving (Eq, Ord, Show)
type T7 = (T, T, T, T, T, T, T)
to :: T -> T7
to = \case
( O :* e :* d :* c :* b :* a) -> (O, O, O, O, O, O, e :* d :* c :* b :* a)
( O :* d :* c :* b :* a) -> (O, O, O, O, b :* a, c, d)
( f :* e :* O :* O :* O :* O) -> (O, O, O, O, O, f, e)
(g :* f :* e :* d :* c :* b :* a) -> (a, b, c, d, e, f, g)
( a) -> (O, O, O, O, O, O, a)
from :: T7 -> T
from = \case
(O, O, O, O, O, O, e :* d :* c :* b :* a) -> O :* e :* d :* c :* b :* a
(O, O, O, O, b :* a, c, d) -> O :* d :* c :* b :* a
(O, O, O, O, O, O, a) -> a
(O, O, O, O, O, f, e) -> f :* e :* O :* O :* O :* O
(a, b, c, d, e, f, g) -> g :* f :* e :* d :* c :* b :* a
instance Arbitrary T where
arbitrary = oneof [pure O, applyArbitrary2 (:*)]
-- prop> \t -> from (to t) === t
-- +++ OK, passed 100 tests.
-- prop> \t7 -> to (from t7) === t7
-- +++ OK, passed 100 tests.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment