Cayley monoid

cayley.idr

module Cayley

-- https://doisinkidney.com/posts/2020-12-27-cayley-trees.html

import Data.Vect

foldlVec : {0 b : Nat -> Type} -> ({0 m : Nat} -> a -> b m -> b (S m)) -> b Z -> Vect n a -> b n
foldlVec f bz  []       = bz
foldlVec f bz (x :: xs) = foldlVec {b = b . S} f (f x bz) xs

revVect : Vect n a -> Vect n a
revVect = foldlVec {b = flip Vect a} (::) []

record VectCont (n : Nat) (a : Type) (b : Type) where
  constructor MkVectCont
  runVectCont : Vect n a -> Vect n (a,b)

revZip : Vect n a -> Vect n b -> Vect n (a,b)
revZip = flip $ runVectCont . foldlVec {b = \n=>VectCont n a b}
                                       (\y,k => MkVectCont \(x::xs) => (x,y) :: runVectCont k xs)
                                       (MkVectCont $ const Nil)

--data Tree : Nat -> Type -> Type where
--  Leaf  : a -> Tree 1 a
--  Split : Tree n a -> Tree m a -> Tree (n + m) a

data Tree2 : Nat -> Nat -> Type -> Type where
  Leaf  : a -> Tree2 n (S n) a
  Split : Tree2 n2 n3 a
       -> Tree2 n1 n2 a
       -> Tree2 n1 n3 a

Tree : Nat -> Type -> Type
Tree = Tree2 Z

three : Tree 3 Int
three = Split (Split (Leaf 1) (Leaf 2)) (Leaf 3)

treeToList : Tree n a -> Vect n a
treeToList xs = go xs []
  where
    go : Tree2 k m a -> Vect k a -> Vect m a
    go (Leaf x)      ks = x :: ks
    go (Split xs ys) ks = go xs (go ys ks)