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

[Andreas Abel]

[This message concerns all that are interested in the theory and 
practice of dependently typed pattern matching...]

Hi Nisse,

If you turn the type indexed data type into its semantics, a 
parametrized datatype with equality proofs, you get:

   data _==_ {U : Set1}(A : U) : U -> Set1 where
     refl : A == A

   data Ty (A : Set) : Set1 where
     isB : (A == Bool) -> Ty A
     isN : (A == ℕ) -> Ty A

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.

So what is the justification that Agda refuses to match isNat against 
Type Bool in your previous message (unfortunately cut away)?

The only justification I can think of is

   "uh, if you matched isNat against Type Bool, you would get an 
equality of  Bool == Nat, but I have no means to hand it to you, so I 
report an error instead"

Also you can write:

   G : (A : Set) -> Ty A -> Ty A -> ℕ
   G .Bool (isB refl) (isB q) = zero
   G .ℕ    (isN refl) (isN q) = succ zero

and this gives a correct "match incomplete" error.

It seems that our current handling of type indices in constructors is 
not principled.  What can we do?

1. Discriminate data types and make Nat == Bool an empty type.
    This strengthens the theory, of course.
    It is not Voevodsky-compatible.

2. Not unify types during matching.  That would be consistent with the
    current view that Nat == Bool is not disprovable.

    This leads to the Coq situation:  You can match, but you
    do not get the type equalities.

3. Forbid matching that would lead to unification of types.
    That might give better error message, but feels a bit like a
    dictatorship.  Are there good programs we would exclude?

Anyway, the current situation lacks a foundation.

On 04.05.11 6:53 PM, Nils Anders Danielsson wrote:
> On 2011-05-04 17:55, Andreas Abel wrote:
>> But Nisse, should not this fail then also?
>>
>> f : (A : Set) → Type A → ℕ
>> f .Bool isBool = zero
>> f .ℕ isℕ = succ zero
>>
>> Agda does unify A with Bool in the first case. If Agda could not tell
>> apart Bool and Nat, then it could not unify A with Bool.
>
> I don't follow you. Unifying a variable and a data type doesn't strike
> me as problematic.

If you write

   g : {A : Set} -> Type A -> Type A -> A
   g isBool isNat = zero

then there are two competitors for A: you get the equations

   A == Bool
   A == Nat

There is no reason to just grab the first one.  This would only be 
justifiable if Bool == Nat was disprovable.

In the current situation, if you choose A := Bool then you get a type 
error for zero : Bool.  The proper error should be that zero is not of 
type *A*.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/