Rose.agda

{-# OPTIONS --sized-types #-}

module Rose where

postulate
  Size : Set
  _^   : Size -> Size
  ∞    : Size

{-# BUILTIN SIZE Size  #-}
{-# BUILTIN SIZESUC _^ #-}
{-# BUILTIN SIZEINF ∞  #-}

data List (A : Set) : {_ : Size} -> Set where
  []   : {size : Size} -> List A {size ^}
  _::_ : {size : Size} -> A -> List A {size} -> List A {size ^}

map : {A B : Set} -> (A -> B) -> 
      {size : Size} -> List A {size} -> List B {size}
map f [] = []
map f (x :: xs) = f x :: map f xs

data Rose (A : Set) : {_ : Size} -> Set where
  rose : {size : Size} -> A -> List (Rose A {size}) {∞} -> Rose A {size ^}

{-
mapRose : {A B : Set} -> (A -> B) -> 
          {size : Size} -> Rose A {size} -> Rose B {size}
mapRose {A} {B} f .{size ^} (rose {size} a l) =
   rose (f a) (map (\ r -> mapRose {A} {B} f {size} r) l)
-}

mapRose : {A B : Set} -> (A -> B) -> 
          {size : Size} -> Rose A {size} -> Rose B {size}
mapRose f (rose a l) = rose (f a) (map (mapRose f) l)