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

[Andrea Vezzosi]

According to "A few constructions on constructors" the types don't
need to be strictly equal, but in addition of having the same shape
you need equality constraints for all the arguments of the family.

For example the following collection of constraints simplifies to
false even when e1 and e2 are not unifiable:
(e1 : Nat =?= e2 : Nat) & (zero : Fin (suc e1) =?= suc i : Fin (suc e2))

while (zero : Fin (suc e1) =?= suc i : Fin (suc e2)) alone is undecided.

Cheers,
Andrea

On Sun, Jan 18, 2015 at 3:38 PM, Andreas Abel <abela at chalmers.se> wrote:
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda