Equality on Types [Re: [Agda] Is this a bug?]

[Conor McBride]

On 5 May 2011, at 11:00, Nils Anders Danielsson wrote:

> On 2011-05-05 10:06, Andreas Abel wrote:
>> Now, there is no good reason why isN should not match against TyBool
>>
>>    F : Ty Bool ->  ℕ
>>    F (isB p) = zero
>>    F (isN p) = suc zero  -- match fine
>>
>> All you get is an equality Bool == Nat, but you cannot use this to
>> derive a contradiction.
>
> Yes you can:

Indeed, cardinality arguments can be used to distinguish types.

[..]

But Nat == List Bool would not admit the same treatment.

Andreas's question is a really deep one about what we mean by a type.
I see the conceptual distinctions between the usage of types and the
structural distinctions in the arrangement of their values as of
considerable significance. I often find myself introducing type
distinctions just to ensure that incompatibility of purpose cannot be
overruled by compatibility of representation. I consider it dangerous
to admit equality of types merely on the basis of shared cardinality.

I'd like to move towards a *more* syntactic view of types, seen as
given by a universe, and supporting generic programming by case  
analysis.
 From that perspective, I'd like type constructors to be constructors:
injective and disjoint...but I'm becoming increasingly suspicious of
large indices.

I suppose an alternative view is that types themselves are morally sets,
and that the place to introduce distinctions of purpose is in the
syntax used to name types via a universe.

We would all be a lot less troubled if we could easily shift elaboration
between universes, hiding the artefacts of encoding. It would be less
important which of the competing positions was hardwired.

All the best

Conor