<div dir="ltr"><div class="gmail_extra">On Fri, Apr 10, 2015 at 5:16 PM, Thorsten Altenkirch <span dir="ltr">&lt;<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>&gt;</span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5"><br><div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif"><div>Ah indeed, I thought this was a bit of a dejavue. I have to admit that I haven’t digested your code. I always thought that Church encodings are not very practical.</div></div></div></div></blockquote><div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">​They are very practical for some things and impractical for others, which is also true of the way we usually think of data/inductive types being implemented (often where one is practical, the other is impractical).​ Although typically one would think that zipping is an impractical case for encodings, it turns out not to be the case if one has positive types (positive data-like types, at least; I haven&#39;t worked through whether encodings of positive types get you the same performance increase here).<br></div> <br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5"><div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif"><span><div dir="ltr"><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div class="gmail_extra">I don&#39;t really understand what, &quot;the only justification is classical,&quot; means. System F has non-strict positive types. Is it classical?</div></blockquote></div></span><div><br></div><div>I’d say so because the only justification for impredicativity is that Prop is small because Bool=Prop.</div></div></div></div></blockquote><div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">​I still don&#39;t know what &quot;justification&quot; means.​<br> <br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5"><div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif"><span><div dir="ltr"><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div class="gmail_extra"><span style="font-family:arial,helvetica,sans-serif">I care about them inasmuch as I&#39;d be interested in seeing a system that allowed them, so I could see what kinds of programs they&#39;d be useful for, and what tradeoffs would have to be made to avoid breaking various properties of the system. From the above, it seems like they have uses when you&#39;re doing things with continuation passing.</span><br><div style="font-family:arial,helvetica,sans-serif"><br></div><div style="font-family:arial,helvetica,sans-serif">And if &quot;justification&quot; refers to the existence of some particular sort of model, I basically don&#39;t care about that at all. So positive types would automatically win that fight for me.<br></div></div></blockquote></div></span><div><br></div><div>If you just want to program you can switch off positivity checking.</div></div></div></div></blockquote><div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">​I could, but then I wouldn&#39;t know whether I could accidentally do something &#39;bad&#39; that I do care about, like write a non-terminating program, or end up in a situation where canonicity or subject reduction fails. So it is also in my interest to encourage other people&#39;s interest in studying systems specifically designed for having positive types along with the other nice properties, and studying which other features don&#39;t combine with it. That way I don&#39;t have to do it (all) myself.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">And it is also in my interest to complain at people discouraging such study because such systems aren&#39;t &quot;justified.&quot; :)<br><br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5"><div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif"><div>I didn’t refer to “some sort of model” but just some naïve understanding. Strictly positive types model some sort of trees, I have no idea what non-strict positive one are. The justification seems just formalistic.</div></div></div></div></blockquote><div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">​Formalism is fine by me. ​I&#39;m telling a computer to push around symbols until it spits out a bunch of symbols in the form I want. The problems come when an addition prevents that from happening. It&#39;s fine if there are things that aren&#39;t trees as long as when I have something that is supposed to be a tree, it&#39;s actually a tree, even if I used non-trees to get there.<br><br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5"><div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif"><div>Usually we get non-strict positivity when we apply the negative translation (aka CPS translation) to an inductive (or coinductive) definition. It is not clear to my why those should exist from a constructive point of view.</div></div></div></div></blockquote><div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">​&quot;Should&quot; sounds like &quot;justification.&quot; Like we have some other system that we&#39;ve decided is constructive, and we&#39;re trying to decide whether something else is constructive by whether we could do all the things in our original system.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">But I guess I am a formalist, because I don&#39;t see why everything doesn&#39;t simply &#39;exist&#39; by fiat, and then we look at properties of the system (like the disjunction and existence properties, or canonicity) to determine if it&#39;s constructive, and care about those properties because they work the way we want. This goes for strictly positive types, too; they exist because we said they exist when we defined the system. And if impredicative polymorphic types exist, that&#39;s very nice, too, because it gives very direct ways of internalizing universal constructions. The only problem to me is that when you add together too many of these nice things in the wrong way, other nice things go away.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">-- Dan<br></div></div></div></div></div>