[TYPES] Y-combinator in Type:Type?

[Jonathan P. Seldin]

I cannot believe the last statement about getting iteration but not  
primitive recursion.  In Combinatory Logic, vol. II, section 3A3,  
Curry gives several methods for defining the primitive recursion  
combinator R in terms of an iterator Z, and the compatibility of some  
of them with simple types is shown in section 13D3, especially  
Theorem 13D3 for the R he calls R(Kp).  (The typing system Curry is  
using here is $\lambda \rightarrow$, and he is writing Fab instead of  
a -> b; furthermore, he is taking the type N of natural numbers as an  
atomic type.  But with the Pi types and the impredicative  
definitions, N can be defined.)

On 19-May-08, at 8:16 AM, Thorsten Altenkirch wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Actually, the initial PTS (Type : Type) has got no identity types but
> only Pi-types. However, we can encode an equality type using the usual
> "Leibniz encoding"
>
> Eq : (A:Type) -> A -> A -> Type
> Eq A a b = Pi P:A -> Type.P a -> P b
>
> and this behaves like intensional equality actually worse: we cannot
> even show that equality is a groupoid (actually using eta we can show
> that it is a category but the laws involving symmetry require
> parametricity, I think).
>
> If you add W-types with the normal elimination principle you get a
> fixpoint combinator (See Thierry's paper on the paradox of Trees).
> That's maybe cheaper then extensional equality (depending on your
> currency). The problem is that the impredicative encodings don't give
> you primitive recursion but only iteration - I'd say.
>
> Cheers,
> Thorsten
>
> On 16 May 2008, at 16:41, Thomas Streicher wrote:
>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
>> types-list
>>  ]
>>
>> But if you have Type:Type together with extensional identity types
>> then
>> every type X is equal to X->X and thus provides a model for untyped
>> lambda calculus and thus allows one to write down an Y-combinator of
>> type X.
>>
>> So the problem is open because of intensional identity types, isn't
>> it?
>>
>> Thomas
>
>
> This message has been checked for viruses but the contents of an  
> attachment
> may still contain software viruses, which could damage your  
> computer system:
> you are advised to perform your own checks. Email communications  
> with the
> University of Nottingham may be monitored as permitted by UK  
> legislation.
>

Jonathan P. Seldin                                                     
tel: 403-329-2364
Department of Mathematics and Computer Science                  
jonathan.seldin at uleth.ca
University of Lethbridge                                              
seldin at cs.uleth.ca
4401 University Drive                                   http:// 
www.cs.uleth.ca/~seldin/
Lethbridge, Alberta, Canada, T1K 3M4