<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=""><br class=""></div><br class="">
<div><br class=""><blockquote type="cite" class=""><div class="">On 8 Nov 2019, at 11:21, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" class="">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="WordSection1" style="page: WordSection1; caret-color: rgb(0, 0, 0); font-family: Menlo-Regular; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">Hi,<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">I didn’t see Wouter’s comment but I guess I can add another unhelpful comment along the same lines. Really a strictly positive operator should be a container and we do need some syntactic sugar for this so that we just have to write something similar as what you do (didn’t even know there were strict positivity annotations). The same criticism applies to the whole sized type story: a reasonable implementation of sized types should be just syntactic sugar for programs we can define without them.<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">But I realize you want to use agda as it is and my principled complaints are not helping. However, they are the reason that I haven’t taken these adhoc extensions serious. I am still waiting that somebody provides a reasonable explanation (i.e. semantics / translation) for them.<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">Thorsten<o:p class=""></o:p></span></div></div></div></blockquote></div><br class=""><div class="">I think expressing semantical scepticism is justified, and long may you do so. </div><div class=""><br class=""></div><div class="">But such scepticism is perhaps more justified for the semantic status of Agda’s notion of “strictly positive" than it is for its sized types, where we have some fine papers by Abel and Pientka (and maybe others) about its theory. (Although there is more to understand: I think your first paragraph expresses the hope that sized types are a conservative extension of some more well-understood, core type theory — it would be good to have results settling that sort of question one way or another.)</div><div class=""><br class=""></div><div class="">Andy</div><div class=""> </div></body></html>