<div dir="ltr">On Fri, Jun 28, 2013 at 6:53 AM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"><br>
<br>
On 28/06/13 10:28, Nils Anders Danielsson wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On 2013-06-28 01:09, Darryl McAdams wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I've certainly run into issues with levels. A good example is an<br>
implementation of Scott/Church encodings. You can define the encoding,<br>
but trying to define simple things like addition becomes difficult if<br>
not impossible, from what I can tell.<br>
</blockquote>
<br>
Are you referring to some kind of universe-polymorphic Church numerals?<br>
The basic encoding works fine (for addition, at least):<br>
</blockquote>
<br></div>
However, you will run into problems if you want to work with Church numerals without using an existing type of inductively defined natural numbers as in your Agda code. The reason is that the recursor of the inductively defined natural numbers has a more general type than the recursor for Church numerals can have in general.<br>
<br>
For example, it has been proven that in the simply typed lambda calculus with one (unspecified) ground type, the exponential function is not definable wrt Church encoding.<br></blockquote><div><br>This is kind of a general 'problem' with predicativity, though. Encoding with a polymorphic eliminator results in a type that is too large to eliminate into, which severely limits the definable functions.<br>
<br>I'm not sure what encoding is being talked about involving levels, though.<br><br> {i : Level} {R : Set i} -> R -> (R -> R) -> R<br><br>is rejected, because you can't name things with type Setω (for reasons I still don't fully understand).<br>
<br> \(i : Level) -> {R : Set i} -> R -> (R -> R) -> R<br><br>is accepted, but then you can define addition with type ℕ i -> ℕ i -> ℕ i, at least. I guess you run into problems if you want to define sums of arbitrarily many numbers of arbitrary level? But I don't know how you'd do that anyway, because it seems like the result would have to not be the lub of the levels but the glb.<br>
</div></div><br>I generally think that Church and Scott encodings are not very compelling motivations (for Agda). Without impredicativity, I'm skeptical that they will ever be very good to work with, regardless of how fancy you make Levels. That's just a sacrifice that Agda makes (unless someone adds --impredicativity).<br>
<br>-- Dan<br></div></div>