[Agda] More universe polymorphism
m.escardo at cs.bham.ac.uk
Fri Jun 28 12:53:08 CEST 2013
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.
More information about the Agda