<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">Hello Guillaume.</div><br class=""><div><blockquote type="cite" class=""><div class="">On 11 Jun 2019, at 08:53, Guillaume Allais <<a href="mailto:guillaume.allais@ens-lyon.org" class="">guillaume.allais@ens-lyon.org</a>> wrote:</div><div class=""><div class=""><br class="">The main difference comes when you try to prove decidable equality<br class="">of sized values (or anything that processes values in lock step).<br class="">Let us consider the case where we compare `t u : PList A i` which<br class="">happen to respectively be `t = pcons a t'` and `u = pcons b u'`.<br class=""><br class="">If you use `↑ i` as the return index in the `pcons` constructor then<br class="">you learn that `i = ↑ i'` and both `t' u' : Pack (PList A i')`. You<br class="">can keep comparing the subterms.<br class=""><br class="">Using the `Size< i` approach however, you get that `t' : Pack (PList A j)`<br class="">for some `j` and `u' : Pack (PList A j')` for some a priori distinct `j'`.<br class="">You are now stuck with subterms which have different types and the<br class="">comparison function cannot be homogeneous anymore.<br class=""></div></div></blockquote><div><br class=""></div><div>Thanks for that. I see the problem, but I’m not entirely convinced that one couldn’t work around such problems while still using the size-"size-parameterized” approach rather than the “size-indexed” one. In particular...</div><div class=""><br class=""></div><blockquote type="cite" class=""><div class=""><div class="">This is part of the motivation for Abel, Vezzosi and Winterhalter's<br class="">work on shape irrelevance in <a href="https://hal.archives-ouvertes.fr/hal-01596179" class="">https://hal.archives-ouvertes.fr/hal-01596179</a><br class=""></div></div></blockquote><div><br class=""></div>...thanks for pointing to that. I contemplated their motivating example (monus-diag in section 2) and came up with a simple solution the "size-parameterized” way (hence avoiding the need to contemplate shape irrelevancy, interesting though that might be). See the attached file of agda code if you are interested. </div><div><br class=""></div><div>Anyway, I think my main difficulty with sized types à la Agda is that they introduce some quite non-trivial subtype relations (very un-Agda-ish :-)) and I am finding it hard to understand when Agda thinks one type involving size expressions is a subtype of another such type and when it doesn’t. </div><div><br class=""></div><div>Andy</div><div><br class=""></div><div></div></body></html>