[Agda] Universe level in heterogeneous association list

[Nicolas Osborne]

Thanks Jacques,

that's very helpfull. I have a better understanding of what's going on here.
I didn't have the idea of puting the level in the data declaration and
using it just in the hcons case.
The level-free version will be handy, it allows to easily specify the
label type.

Nicolas


Le 18/04/2020 à 17:46, Jacques Carette a écrit :
> 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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200418/eca7b017/attachment.sig>