The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

On 7 Jan 2010, at 17:17, Andreas Abel wrote:

> I agree with Thorstens analysis.  There is nothing like a "constructor", 
> the machine only nows bits and sequences, so ultimately you need to explain 
> everything but just these two principles: alternatives (bits) and 
> composition (pairing).

and functions, i.e. pieces of code in a black box!


>  This is realized in so called structural type system, where a type is just 
> an expression made of constants, +, \times, fixpoints, and function types.  
> Thorsten analyses Agda data declarations into structural expressions, so
> 
>  I = \ X. 0
> 
> which is not injective.  Named type systems, which use constructors (Agda) 
> or class names (Java), restrict the power of structural type systems to 
> make subtyping, unification, type checking etc. decidable and maybe your 
> code more readable.  But I do not think that named type systems are 
> foundational, they need to be explained in terms of structure.
> 
> So the problem at hand can be solved in conjunction with giving a semantics 
> for Agda data types.  Using the semantics one can identify sufficient 
> criteria for injectivity.
> 
> For a pragmatic solution, I suggest to consider the problem of injective 
> type constructors in a simply-typed setting and then extrapolate to a 
> dependently typed setting.
> 
> Cheers,
> Andreas
> 
> 
> On Jan 7, 2010, at 4:15 PM, Thorsten Altenkirch wrote:
> 
>> Hi Noam,
>> 
>>>> Surely, type constructors should not be injective in general. A 
>>>> definition
>>>> of the form
>>>> data I : (Set -> Set) -> Set where
>>>> should be expandable by an annonymous declaration
>>>> I : (Set -> Set) -> Set
>>>> I F = data {}
>>>> in an analogous way a named function definition can be expanded by
>>>> definition and a lambda abstraction
>>> 
>>> ...I'm not sure about this expansion, and the analogy.  I think the
>>> question is whether we view the declaration of type constructors in
>>> the same way that we view the declaration of term constructors (i.e.,
>>> as stipulating a new way of constructing things, in this case
>>> inhabitants of Set).  If we do, then type constructors are by
>>> definition injective.
>> 
>> I don't see the analogy. A term constructor is injective because an 
>> inductive type is freely generated from constructors. Indeed, we can show 
>> that the structure map of an initial algebra is an isomorphism and hence 
>> injective. However the universe of sets is not freely constructed from 
>> type constructors but they are really definitions.
>> 
>> We should justify principles like this (i.e. all type constructors are 
>> injective) by a semantic explanation or by a translation into a well 
>> understood core language e.g. (extensional) Marttin-Loef Type Theory with 
>> W-types and universes. I don't know any such explanation which would 
>> justify this principle. Moreover, Chung's example shows that this is not 
>> possible (without giving up something else) since pure type theory is 
>> consistent with EM.
>> 
>> Cheers,
>> Thorsten
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda AT lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
> 
> Andreas ABEL
> INRIA, Projet Pi.R2
> 23, avenue d'Italie
> F-75013 Paris
> Tel: +33.1.39.63.59.41
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda AT lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda