[Agda] Universe-Heterogeneous tree

[gallais]

I should probably not post this but...

======================================================
module TreeLevel where

open import Level

infixr 0 _×_
infixr 6 _,_
record _×_ {l m : Level} (A : Set l) (B : Set m) : Set (l ⊔ m) where
   constructor _,_
   field
     fst : A
     snd : B
open _×_

infixr 2 ty node
data ASTLevel : Set where
   node : ASTLevel → ASTLevel → ASTLevel
   ty   : (l : Level) → ASTLevel

pattern _=>_ t u = node t u

bound : ASTLevel → Level
bound (t => u) = bound t ⊔ bound u
bound (ty l)   = l

record Leaf {α} (A : Set α) : Set α where
   constructor leaf
   field unleaf : A

AST : (ls : ASTLevel) → Set (suc (bound ls))
AST (t => u) = AST t × AST u
AST (ty l)   = Set l

infix 3 _⊗_] _⟩
pattern [ {ls} {ms} = node ls ms
pattern _⊗_] T U    = T , U
pattern ⟨ {l}       = ty l
pattern _⟩ S        = S

infix 1 _ast_
_ast_ : (ls : ASTLevel) (T : AST ls) → Set (bound ls)
[ ast T ⊗ U ] = _ ast T × _ ast U
⟨ ast S     ⟩ = Leaf S

open import Data.Nat

example : _ ast _
example = leaf 3 , leaf (ℕ × ℕ)

======================================================

On 05/08/15 16:52, effectfully wrote:
> It's more convenient to make the second argument of `ast' explicit and
> then define an implicit version:
>
> ast : {ls : ASTLevel} (T : AST ls) → Set (bound ls)
> ast {ls => ms} (T , U) = ast T × ast U
> ast {ty l}      T      = Leaf T
>
> astᵢ = λ {ls} {T : AST ls} -> ast T
>
> example : astᵢ
> example = leaf 3 , leaf (ℕ × ℕ)
>
> I wonder if it could be implemented in Agda that pattern matching on
> constructor-headed functions would not require pattern matching on
> their arguments. Then we could write
>
> AST : (ls : ASTLevel) → Set (suc (bound ls))
> AST (t => u) = AST t × AST u
> AST (ty l)   = Leaf (Set l)
>
> ast : {ls : ASTLevel} (T : AST ls) → Set (bound ls)
> ast (T , U)  = ast T × ast U
> ast (leaf T) = Leaf T
>
> But this is not very useful feature probably.