<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.hoenzb
{mso-style-name:hoenzb;}
span.EmailStyle19
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Hi,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">I think there should be an alternative to these ad hoc extensions of the type system (including the size mechanism). In general this corresponds to constructing an internal model of type theory.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Incidentally this is related to a grant proposal (on “Template Type Theory”) I am working on just now.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">In this case a strictly positive type can be modelled as a container but the overhead of using containers explicitely makes this unfeasible. However, Tamara von Glehn and others have shown that containers
form a model of type theory. Maybe this doesn’t yet give you everything you want but I think this can scaled up to enable us to provide the semantics for the judgement that a type or a family of types occurs strictly positively and hence that we can use it
in an inductive (or coinductive) definition. <o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Hence what we are proposing is to turn the model constructions that justify extensions from paper code into agda code which can be used to implement these extensions safely. And using (and extending)
type theory in type theory developed with Ambrus Kaposi we have a good handle to talk about type theory internally.
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Having said this I am very much in favour of experimentation now but I think in the long run we have to think how to reign in the wild growth of extensions and modifications of type theory.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thorsten<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;color:black">Agda <agda-bounces@lists.chalmers.se> on behalf of Jesper Cockx <Jesper@sikanda.be><br>
<b>Date: </b>Friday, 20 July 2018 at 13:37<br>
<b>To: </b>Neel Krishnaswami <nk480@cl.cam.ac.uk><br>
<b>Cc: </b>agda list <agda@lists.chalmers.se><br>
<b>Subject: </b>Re: [Agda] Why does this pass the positivity checker?<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"><a name="_MailOriginalBody">Currently there is no way to do that, (partly) because positivity information is not stored in the type of a function. There has been talk of integrating this into the type system, but it's not clear at the moment
how to do this in a nice way.<o:p></o:p></a></p>
</div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody">One special case are the polarity pragma's that can be used to assign a given polarity to a postulate, see
</span><a href="https://github.com/agda/agda/blob/master/test/Succeed/Polarity-pragma.agda"><span style="mso-bookmark:_MailOriginalBody">https://github.com/agda/agda/blob/master/test/Succeed/Polarity-pragma.agda</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody">.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody">-- Jesper<o:p></o:p></span></p>
</div>
</div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody"><o:p> </o:p></span></p>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody">On Fri, Jul 20, 2018 at 2:24 PM, Neel Krishnaswami <</span><a href="mailto:nk480@cl.cam.ac.uk" target="_blank"><span style="mso-bookmark:_MailOriginalBody">nk480@cl.cam.ac.uk</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody">>
wrote:<o:p></o:p></span></p>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody">Hello,<br>
<br>
Is there any way to annotate the type signature with positivity information? It would be helpful for localizing errors, and for doing ML-style modular programming.<br>
<br>
Thanks for your help! <o:p></o:p></span></p>
<div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody"><br>
<br>
<br>
On 20/07/18 13:06, Jesper Cockx wrote:<o:p></o:p></span></p>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="mso-bookmark:_MailOriginalBody">I think Agda checks for each function definition whether it is (strictly)<br>
positive in each of its arguments. The 'depth' of this check is not limited<br>
AFAICT, but it is determined at the definition site of the function, not at<br>
the use site. I've seen this used quite often for universe constructions<br>
such as in your example.<br>
<br>
-- Jesper<br>
<br>
On Thu, Jul 19, 2018 at 1:15 PM, Neel Krishnaswami <</span><a href="mailto:nk480@cl.cam.ac.uk" target="_blank"><span style="mso-bookmark:_MailOriginalBody">nk480@cl.cam.ac.uk</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody">><br>
wrote:<o:p></o:p></span></p>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="mso-bookmark:_MailOriginalBody">Hello,<br>
<br>
I wrote the following bit of code, to experiment with generic programming.<o:p></o:p></span></p>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="mso-bookmark:_MailOriginalBody">data _×_ (A B : Set) : Set where<br>
_,_ : A → B → A × B<br>
<br>
<br>
data _+_ (A B : Set) : Set where<br>
inl : A → A + B<br>
inr : B → A + B<br>
<br>
<br>
data Poly : Set₁ where<br>
K : Set → Poly<br>
_</span><span style="mso-bookmark:_MailOriginalBody"><span style="font-family:"Cambria Math",serif">⊗</span></span><span style="mso-bookmark:_MailOriginalBody">_ : Poly → Poly → Poly<br>
_</span><span style="mso-bookmark:_MailOriginalBody"><span style="font-family:"Cambria Math",serif">⊕</span></span><span style="mso-bookmark:_MailOriginalBody">_ : Poly → Poly → Poly<br>
Id : Poly<br>
<br>
[_] : Poly → Set → Set<br>
[ K X ] A = X<br>
[ p </span><span style="mso-bookmark:_MailOriginalBody"><span style="font-family:"Cambria Math",serif">⊗</span></span><span style="mso-bookmark:_MailOriginalBody"> q ] A = [ p ] A × [ q ] A<br>
[ p </span><span style="mso-bookmark:_MailOriginalBody"><span style="font-family:"Cambria Math",serif">⊕</span></span><span style="mso-bookmark:_MailOriginalBody"> q ] A = [ p ] A + [ q ] A<br>
[ Id ] A = A<br>
<br>
data μ (F : Poly) : Set where<br>
into : [ F ] (μ F) → μ F<o:p></o:p></span></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="mso-bookmark:_MailOriginalBody">and Agda accepted the declaration of μ. I was surprised by this -- did<br>
Agda look at the body of the definition of [_] to decide that every<br>
recursive occurrence was positive? If so, how deeply does it look?<br>
<br>
--<br>
Neel Krishnaswami<br>
</span><a href="mailto:nk480@cl.cam.ac.uk" target="_blank"><span style="mso-bookmark:_MailOriginalBody">nk480@cl.cam.ac.uk</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody"><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
</span><a href="mailto:Agda@lists.chalmers.se" target="_blank"><span style="mso-bookmark:_MailOriginalBody">Agda@lists.chalmers.se</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody"><br>
</span><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank"><span style="mso-bookmark:_MailOriginalBody">https://lists.chalmers.se/mailman/listinfo/agda</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody"><o:p></o:p></span></p>
</blockquote>
</blockquote>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody"><o:p> </o:p></span></p>
</div>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="mso-bookmark:_MailOriginalBody"><span class="hoenzb"><span style="color:#888888">--
</span></span></span><span style="mso-bookmark:_MailOriginalBody"><span style="color:#888888"><br>
<span class="hoenzb">Neel Krishnaswami</span><br>
</span></span><a href="mailto:nk480@cl.cam.ac.uk" target="_blank"><span style="mso-bookmark:_MailOriginalBody">nk480@cl.cam.ac.uk</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody"><o:p></o:p></span></p>
</blockquote>
</div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody"><o:p> </o:p></span></p>
</div>
</div>
<PRE>
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</PRE></body>
</html>