[Agda] Universe level in heterogeneous association list

[Jacques Carette]

Here is one way to do it.

module HAL where

open import Data.List
open import Level

data HAL {ll lx : Level} {Label : Set ll} : List Label -> Set (ll ⊔ suc 
lx) where
   hnil  : HAL []
   hcons : {ls : List Label} {X : Set lx}
     -> (l : Label)
     -> (x : X)
     -> (h : HAL {ll} {lx} ls)
     -> HAL (l ∷ ls)

If you want to be level-free, then you can set ll and lx to 0, and get

data HAL0 {Label : Set} : List Label -> Set (suc zero) where
   hnil  : HAL0 []
   hcons : {ls : List Label} {X : Set}
     -> (l : Label)
     -> (x : X)
     -> (h : HAL0 ls)
     -> HAL0 (l ∷ ls)

You need to go up a level because hcons contains a whole Set (of Level 0).

Jacques

On 2020-Apr.-18 09:17 , Nicolas Osborne wrote:
> Hello,
>
> I am trying to implement the heterogeneous association list from McBride
> and McKinna's View From the Left, and universe polymorphism is giving me
> a hard time.
>
> The version without any level information is:
>
> ```agda
> module HAL where
>
> open import Data.List
> open import Level
>
> data HAL {Label : Set} : List Label -> Set where
>    hnil  : HAL []
>    hcons : {ls : List Label}{X : Set}
>      -> (l : Label)
>      -> (x : X)
>      -> (h : HAL ls)
>      -> HAL (l ∷ ls)
> ```
>
> The `hcons` constructor raises an error. I believe that the Universe
> level should be the max between the level of the Label and the level of
> X, a list of Label being at the same level as Label. (But, am I right in
> believing so ?)
>
> Here is what Agda said:
>
> Set₁ is not less or equal than Set
> when checking that the type
> {ls : List Label} {X : Set} (l : Label) → X → HAL ls → HAL (l ∷ ls)
> of the constructor hcons fits in the sort Set of the datatype.
>
>
> So far, in the few Universe polymorphism I have done, the level
> information was in the type signature. But I don't want to put X in the
> type signature, the point being that we should be able to change the X
> at each hcons (also, Agda does not accept this definition neither).
>
> Anybody has a suggestion ?
>
>
> Nicolas Osborne
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200418/1284b1a9/attachment.html>