[Agda] Agda master is anti-classical, injective type constructors are back

[Andreas Abel]

The answer to your question can be found here:
https://code.google.com/p/agda/issues/detail?id=292

Originally, equality of types was not checked at all (clearly buggy), 
then equality of types was checked, but that fix was considered to 
restrictive.  We settled in the middle: it is sufficient that the types 
have the same shape, i.e., both are instances of the Fin type.

Cheers,
Andreas

On 17.01.2015 23:03, Matthieu Sozeau wrote:
> Hi,
>
>    I'm curious here:
>
>    fzero n : Fin (suc n) =?= fzero m : Fin (suc m) -> n =?= m
>
> How come this is not postponed due to the fact that the types are different?
> -- Matthieu
>
> 2015-01-17 16:37 GMT+05:30 Andreas Abel <abela at chalmers.se>:
>> This concerns only the unreleased Agda master development branch.
>>
>> Using heterogeneous equality and big forced indices in a data type SING, I
>> manage to prove injectivity of type constructor
>>
>>    SING : (Set -> Set) -> Set
>>
>> The rest follows Chung-Kil Hur's refutation of excluded middle, as published
>> in January 2010 on the Coq and Agda lists.
>>
>> My development was fathered by my surprise that I could prove
>>
>>    inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → n ≡ m
>>
>> but not by directly matching on the heterogeneous equality (which Agda
>> refuses as Fin n = Fin m does not yield n = m), but by first matching on i
>> and j, which exposes n and m in the constructor patterns and makes then
>> available for unification.
>>
>>    inj-Fin-≅ {i = zero}  {zero} ≅refl = refl  -- matching on ≅refl succeeds!
>>    inj-Fin-≅ {i = zero}  {suc j} ()
>>    inj-Fin-≅ {i = suc i} {zero} ()
>>    inj-Fin-≅ {i = suc i} {suc j} p = {!p!}   -- Splitting on p succeeds!
>>
>> This is weird.
>>
>> A fix would be to not generate any unification constraints for forced
>> constructor arguments, for instance
>>
>>    fzero : (n : Nat) -> Fin (suc n)
>>
>>    fzero n : Fin (suc n) =?= fzero m : Fin (suc m)
>>
>> would not simplify to n =?= m : Nat.
>>
>> This change would break a lot of developments using heterogeneous equality,
>> as did the fix of issue 292
>> (https://code.google.com/p/agda/issues/detail?id=292).  In particular,
>> heterogeneous equality would not imply the equality of the types, but the
>> equality of the types has to be given in order to sensibly work with
>> heterogeneous equality.  In case of Fin, one would work with telescopes
>>
>>    {n m : Nat} (p : n == m) {i : Fin n} {j : Fin m} (q : i ~= j)
>>
>> rather than being able to derive p from q.
>>
>> This is Conor McBride's proposal for heterogeneous equality, if I am not
>> mistaken.
>>
>> RFC,
>> Andreas
>>
>> --
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>> Department of Computer Science and Engineering
>> Chalmers and Gothenburg University, Sweden
>>
>> andreas.abel at gu.se
>> http://www2.tcs.ifi.lmu.de/~abel/
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
>


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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