[Agda] Unification of function types
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Sep 20 20:37:34 CEST 2013
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/
More information about the Agda
mailing list