[Agda] Unification of function types

[Jesper Cockx]

 Thank you for the links, they are very interesting discussions. At the end
of the first one, you posed the following question:

> I have a related issue. The following does not type check:
>
> data _≡_ {a : Set1} (x : a) : a -> Set where
>   refl : x ≡ x
>
> proj₁ : forall {a₁ b₁ a₂ b₂ : Set} ->
>         (a₁ -> b₁) ≡ (a₂ -> b₂) -> a₁ ≡ a₂
> proj₁ refl = refl
>
> Agda complains about the pattern refl (a₁ != a₂). In light of your
> recent patch, is there any reason not to allow also this function?
>
> This seems to be very related to my problem, but unfortunately no answer
was given.

Also in the same thread, Ulf mentioned that he added injectivity of type
constructors, however the following code does not typecheck for me:

module Test where
>
> open import Data.Unit
> open import Relation.Binary.PropositionalEquality
>
> data I : Set → Set where
>   i : I ⊤
>
> I-inj : {A B : Set} → I A ≡ I B → A ≡ B
> I-inj refl = refl


Has this been removed again from Agda? (Maybe in light of the problems
discussed in the second thread?)

An interesting remark by Conor was the following:

> Back when I was mucking about with this type,
> my answer was "homogeneously"! That's to say,
> rather than interpreting heterogeneous equality
> as "the types are equal and the terms are equal",
> it's "if the types are equal, the terms are equal".
>
> It seems I can prove that the types are equal from the heterogeneous
equality: the type of the constructor refl (in my first post) tells us not
just that the terms a and a' are equal, but that the types A and A' are
equal as well. However, the following doesn't typecheck:

equal-types : ∀ {l} (A : Set l) (a : A) (A' : Set l) (a' : A) → a ≃ a' → A
> ≃ A'
> equal-types A a .A .a refl = {!!}
>
> Failed to infer the value of dotted pattern
> when checking that the pattern .A has type Set l
>

So I guess I'm missing something here.

>From a more theoretical perspective, it seems to me quite unproblematic to
add a rule that A1 = A2 and B1 = B2 whenever (x : A1) -> B1 = (x : A2) ->
B2. Indeed, the definitional equality rule for Pi-types is as follows (from
Goguen's PhD thesis):

Γ ⊢ A1 = A2        Γ , x : A1 ⊢ B1 = B2
---------------------------------------------------------
   Γ ⊢ (x : A1) -> B1 = (x : A2) -> B2

so the rule seems to follow by a basic inversion argument. On the other
hand, it doesn't seem possible to prove the same thing for the *
propositional* (homogeneous or heterogeneous) equality. Maybe someone could
shed some light on this?

Thanks for your answers,

Jesper Cockx






On Thu, Sep 19, 2013 at 4:43 PM, Nils Anders Danielsson <nad at cse.gu.se>wrote:

> On 2013-09-19 16:18, Jesper Cockx wrote:
>
>> I guess the problem with the first definition is that Agda doesn't
>> know how to unify the two types (x : A₁) → B₁ x and (x : A₁) → B₂ x.
>> Would it be problematic add such a rule to the unification algorithm?
>>
>
> You may be interested in the following mailing list threads:
>
>   heterogeneous equality
>   https://lists.chalmers.se/**pipermail/agda/2008/000153.**html<https://lists.chalmers.se/pipermail/agda/2008/000153.html>
>
>   Agda with the excluded middle is inconsistent ?
>   http://thread.gmane.org/gmane.**science.mathematics.logic.coq.**
> club/4322<http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/4322>
>
> --
> /NAD
>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130920/f5180e3e/attachment.html