<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-cite-prefix">Here is one way to do it.</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">module HAL where<br>
<br>
open import Data.List<br>
open import Level<br>
<br>
data HAL {ll lx : Level} {Label : Set ll} : List Label -> Set
(ll ⊔ suc lx) where<br>
hnil : HAL []<br>
hcons : {ls : List Label} {X : Set lx}<br>
-> (l : Label)<br>
-> (x : X)<br>
-> (h : HAL {ll} {lx} ls)<br>
-> HAL (l ∷ ls)</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">If you want to be level-free, then you
can set ll and lx to 0, and get</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">data HAL0 {Label : Set} : List Label
-> Set (suc zero) where<br>
hnil : HAL0 []<br>
hcons : {ls : List Label} {X : Set}<br>
-> (l : Label)<br>
-> (x : X)<br>
-> (h : HAL0 ls)<br>
-> HAL0 (l ∷ ls)<br>
</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">You need to go up a level because hcons
contains a whole Set (of Level 0).</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">Jacques</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">On 2020-Apr.-18 09:17 , Nicolas Osborne
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:f334a3d5-cee0-39d4-c4d5-0a9d380b1728@univ-lille.fr">
<pre class="moz-quote-pre" wrap="">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
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<p><br>
</p>
</body>
</html>