[Agda] Unification of function types

[Andreas Abel]

Hi Jesper, here are some answers:

On 20.09.2013 12:14, Jesper Cockx wrote:
>   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?

See very end of this message.

> 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?)

No, but you need

   {-# OPTIONS --injective-type-constructors #-}

and then the example checks.

> 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

This surely should not work, since you wrote a' : A and not a' : A'.

> 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.

Definitional equality does include a congruence rule for function types.

> 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?

I guess the homotopy guys would not like this, since for them equality 
between types is really just isomorphism.

Cheers,
Andreas

> On Thu, Sep 19, 2013 at 4:43 PM, Nils Anders Danielsson <nad at cse.gu.se
> <mailto: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?
>


-- 
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/