[Agda] Universe-Heterogeneous tree

[Philipp Hausmann]

That's actually quite a neat solution, thank you. Extending it to
dependent types is actually also quite straightforward:

---------------------------
module TreeLevel where

open import Level
open import Data.Product

data ASTLevel : Set where
  _A=>_ : ASTLevel → ASTLevel → ASTLevel
  Aty   : (l : Level) → ASTLevel

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

AST : (ls : ASTLevel) → Set (suc (bound ls))
el : {ls : ASTLevel} (T : AST ls) → Set (bound ls)


AST (t A=> u) = Σ (AST t) (λ t' → (el t' → AST u))
AST (Aty l)   = Set l

el {ls A=> ls₁} (T , U) = (t : el T) → el (U t)
el {Aty l} t = t


open import Data.Nat
open import Data.Vec

example : AST _
example = ℕ , (λ n → Set , (λ A → Vec A n))
----------------------------

I'm also wondering if it's possible to use Level arguments in the AST
language, but
that seems quite tricky. Just writing a universe-polymorphic function
with the above AST
doesn't work, but that's not really surprising:
--------
m : AST _
m = Level , (λ l → Set l)
-------
(l : Level) → Set (Level.suc l) !=< _B_81 Level
because this would result in an invalid use of Setω
when checking that the expression λ l → Set l has type _B_81 Level
--------

Philipp

On 08/05/2015 01:40 PM, gallais wrote:
> Hi Philipp,
>
> One possible approach is to store all the levels in a tree with
> the shape you're looking for and then define various types by
> recursion on that tree.
>
> Here I start with a tree `ASTLevel` similar to yours except that
> it only stores the levels. `bound` then lets me compute the level
> of the `AST` type which I define by recursion on the `ASTLevel`.
>
> `ast` is an example of how to give a semantics to an `AST` type
> as a proper Agda type. Basically always use recursion on the type
> describing the structure of the whole thing (here ASTLevel).
>
> Cheers,
>
> =================================================================
> module TreeLevel where
>
> open import Level
> open import Data.Product
>
> data ASTLevel : Set where
>   _=>_ : ASTLevel → ASTLevel → ASTLevel
>   ty   : (l : Level) → ASTLevel
>
> bound : ASTLevel → Level
> bound (t => u) = bound t ⊔ bound u
> bound (ty l)   = l
>
> AST : (ls : ASTLevel) → Set (suc (bound ls))
> AST (t => u) = AST t × AST u
> AST (ty l)   = Set l
>
> ast : (ls : ASTLevel) (T : AST ls) → Set (bound ls)
> ast (ls => ms) (T , U) = ast ls T × ast ms U
> ast (ty l)     T       = T
>
> open import Data.Nat
>
> example : ast _ (ℕ , Set)
> example = 3 , (ℕ × ℕ)
> =================================================================
>
> On 05/08/15 12:21, Philipp Hausmann wrote:
>> Hi all,
>>
>> I'm a bit stuck with a problem with the universe levels of Agda.
>>
>> What I'm trying to do is to create a small AST representing Haskell-like
>> types in Agda. A
>> simplified version of my datatype looks like this:
>>
>> data AST {l} : Set (suc l) where
>>    -- function type
>>    _=>_ : AST {l} -> AST {l} -> AST
>>    -- A concrete named type, e.g. Nat, Int, or also Set
>>    ty : Set l -> AST
>>
>> The problem with the above definition is that
>> all "ty" nodes in the tree need to have the same level.
>> It's not possible to write e.g. the following:
>>
>> (ty Set0) => (ty Nat)
>>
>> "ty Set0" requires the level to be 1, "ty Nat" forces it to be 0. In
>> this example,
>> there are only two different levels, but deeper trees may require an
>> arbitrary number
>> of different levels, one for each leaf node of the AST.
>>
>> So what I want is basically a universe heterogeneous tree. What I tried
>> so far is the following:
>>
>> 1. Index the datatype on a level argument:
>>
>> data AST ... : (l : Level) -> Set l where
>>    ....
>>
>> Agda doesn't accept this: "The sort of AST cannot depend on its indices
>> ...."
>>
>>
>> 2. The Level.Lift record by itself doesn't help, as it does not hide any
>> Level arguments.
>>
>> 3. Add one additional level argument to AST:
>>
>> data AST {l m} : Set (sup l m)
>>    _=>_ : AST {l} {l} -> AST {m} {m} -> AST
>>    .....
>>
>> Now the whole tree takes exactly two level arguments instead of one.
>> This does not solve the problem,
>> as a tree might require more than two level arguments. E.g.:
>>    (ty Set0) => (ty Set1) => (ty Set2)
>>
>>
>>
>>
>> So I'm kind of unsure what else to try. I suspect it may be possible to
>> do this by avoiding datatypes and
>> just using functions, but I haven't investigated this yet and I'm trying
>> to avoid going in that direction.
>>
>>
>> Do you maybe have any ideas or hints?
>>
>> Philipp
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda