[Agda] More universe polymorphism

[Dan Doel]

On Fri, Jun 28, 2013 at 6:53 AM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

>
>
> On 28/06/13 10:28, Nils Anders Danielsson wrote:
>
>> On 2013-06-28 01:09, Darryl McAdams wrote:
>>
>>> I've certainly run into issues with levels. A good example is an
>>> implementation of Scott/Church encodings. You can define the encoding,
>>> but trying to define simple things like addition becomes difficult if
>>> not impossible, from what I can tell.
>>>
>>
>> Are you referring to some kind of universe-polymorphic Church numerals?
>> The basic encoding works fine (for addition, at least):
>>
>
> 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.
>
> 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.
>

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.

I'm not sure what encoding is being talked about involving levels, though.

    {i : Level} {R : Set i} -> R -> (R -> R) -> R

is rejected, because you can't name things with type Setω (for reasons I
still don't fully understand).

    \(i : Level) -> {R : Set i} -> R -> (R -> R) -> R

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.

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).

-- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130628/9794ce3a/attachment.html