Dependent RoseTree

RoseTree.idr

import Data.Vect

op : Nat -> Type -> Type
op Z a = a
op (S n) a = a -> op n a

mutual
  data RoseTree : a -> Type where
    Rose : (n : Nat ** OpTree n a) -> RoseTree a

  data OpTree : Nat -> Type -> Type where
    Node : op n a -> Vect n (RoseTree a) -> OpTree n a

leaf : a -> RoseTree a
leaf x = Rose (Z ** Node x [])

three : RoseTree Int
three = leaf 3

five : RoseTree Int
five = leaf 5

add : op 2 Int
add x y = x + y

square : op 1 Int
square x = x * x

eight : RoseTree Int
eight = Rose (2 ** Node add [three, five])

sixtyfour : RoseTree Int
sixtyfour = Rose (1 ** Node square [eight])

naryApp : op n a -> Vect n a -> a
naryApp x [] = x
naryApp f (x :: xs) = naryApp (f x) xs

eval : RoseTree a -> a
eval (Rose (Z ** Node x [])) = x
eval (Rose (k ** Node f xs)) = naryApp f (map eval xs)

test : Int
test = assert_total $ eval sixtyfour

endless : RoseTree Int
endless = Rose (1 ** Node square [endless])

data RT : Nat -> Type -> Type where
  RN : op n a -> Vect n (k : Nat ** RT k a) -> RT n a

evalRT : RT n a -> a
evalRT {n=Z} (RN x []) = x
evalRT {n=(S l)} (RN f ((_ ** rt) :: ts)) = evalRT {n=l} $ RN (f (evalRT rt)) ts