[Agda] Universe-Heterogeneous tree

[gallais]

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