[Agda] Fin n -> Fin n extensional?

[Peter Selinger]

Hi Andreas,

even the statement "Functions with different names are different even
if their code is the same" seems to be only conditionally true. For
example, 

  open import Relation.Binary.PropositionalEquality

  id : {a : Set} -> a -> a
  id = λ x -> x

  id2 : {a : Set} -> a -> a
  id2 x = x

  test : {a : Set} -> id {a} ≡ id2
  test = refl

works without a hitch. Actually, even this works:

  app : {a b : Set} -> (a -> b) -> (a -> b)
  app f x = f x

  test2 : {a b : Set} -> app {a} {b} ≡ id {a -> b}
  test2 = refl

So the reality seems to be more complicated than you suggest. Even
named functions seem to be compared up to beta-eta equality, provided
that they are not pattern-matching.

-- Peter

Andreas Abel wrote:
> 
> Peter,
> 
> your analysis is correct.  Equality is not structural in Agda, but 
> generative.  Functions with different names are different even if their 
> code is the same.
> 
>    not : Bool -> Bool
>    not true = false
>    not false = true
> 
> is intensionally different from
> 
>    neg : Bool -> Bool
>    neg true = false
>    neg false = true
> 
> Each pattern matching lambda (pml) is a new named function, so pattern 
> matching lambdas are different even though they share the same code. 
> This is certainly a sort of confusion and owed to the light-weight 
> implementation of pmls.
> 
> Ordinary lambdas are just terms which are compared via beta-eta.
> 
> --Andreas
> 
> On 18.02.2015 23:57, Peter Selinger wrote:
> > This discussion reminds me that I have basically very little idea what
> > equality of functions means in Agda. It may be one of the places where
> > Agda differs from Coq. Unfortunately, the reference manual is mostly
> > silent on this point, except for an obscure reference on the page on
> > functions:
> >
> > http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Functions
> >
> > In the subsection on pattern matching lambdas, the manual states that
> > "pattern matching functions are generative. For instance, refl will
> > not be accepted as an inhabitant of the type
> >
> >    (λ { true → true ; false → false }) ≡
> >    (λ { true → true ; false → false }),
> >
> > because this is equivalent to extlam1 ≡ extlam2 for some distinct
> > fresh names extlam1 and extlam2."
> >
> >>From this, I inferred that function equality in Agda is definitional
> > equality, i.e., two functions are equal if and only if they are
> > internally represented as pointers to the same closure.
> >
> > However, this does not seem to be the case in general. For most
> > functions, Agda seems quite happy to accept refl as an inhabitant as
> > long as the two functions are beta-eta equivalent. For example,
> >
> > test : {a : Set} -> (λ(x : a -> a) -> λ(y : a) -> x y) ≡ (λ(x : a -> a) -> x)
> > test = refl
> >
> > Apparently it is only for pattern-matching functions that definitional
> > equality is used. So the correct answer for most purposes seems to be:
> > Agda equality at function types is a random, but fixed, relation that
> > is contained in beta-eta equality and that contains definitional
> > equality.
> >
> > In particular, one cannot prove extensionality for any function whose
> > domain is a datatype (such as Void or Fin n), because one can just
> > write down two identical copies of some pattern-matching function, and
> > they won't be equal.
> >
> > -- Peter
> >
> > Abhishek Anand wrote:
> >>
> >> Unprovability of void-ext has been known to be the reason why one cannot
> >> (in Coq)
> >> code up natural numbers as W Types.
> >>
> >> Here is a quote :
> >> "This is because one cannot prove that there is only a unique function from
> >> the empty set to the set of natural numbers without using extensional
> >> equality."
> >> from
> >> https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes
> >>
> >> However, I don't know a formal (meta-theoretical) proof of unprovability of
> >> void-ext.
> >> I'd be grateful if someone can point us to such a  proof.
> >>
> >>
> >> -- Abhishek
> >> http://www.cs.cornell.edu/~aa755/
> >>
> >> On Wed, Feb 18, 2015 at 11:20 AM, Dan Licata <drl at cs.cmu.edu> wrote:
> >>
> >>> Can you even do this (without otherwise assuming function extensionality)?
> >>>
> >>> For example, for Fin 0, isn't it the same as saying "any function from 0
> >>> to A is abort":
> >>>
> >>>    data Id {A : Set} (a : A) : A → Set where
> >>>      refl : Id a a
> >>>
> >>>    data Void : Set where
> >>>
> >>>    abort : {A : Set} → Void → A
> >>>    abort ()
> >>>
> >>>    void-ext : {A : Set} → (f : Void → A) → Id f abort
> >>>    void-ext f = {!!}
> >>>
> >>> (void-ext is sufficient; is it necessary?)
> >>> and if so, can you prove that?  I don't see how off the top of my head.
> >>>
> >>> -Dan
> >>>
> >>> On Feb 18, 2015, at 10:47 AM, João Paulo Pizani Flor <J.P.PizaniFlor at uu.nl>
> >>> wrote:
> >>>
> >>> Not yet (couldn't find it anywhere), but I will probably need it for my
> >>> Ph.D project, so maybe it will come in some time...
> >>>
> >>> Cheers,
> >>>
> >>> João Pizani, M.Sc <j.p.pizaniflor at uu.nl>
> >>> Promovendus - Departement Informatica
> >>> Faculteit Bètawetenschappen - Universiteit Utrecht
> >>>
> >>> On Wed, Feb 18, 2015 at 3:25 PM, Jacques Carette <carette at mcmaster.ca>
> >>> wrote:
> >>>
> >>>> Does anyone have a proof in Agda that functions at type (Fin n -> Fin n)
> >>>> are extensional?
> >>>> Jacques
> >>>> _______________________________________________
> >>>> Agda mailing list
> >>>> Agda at lists.chalmers.se
> >>>> https://lists.chalmers.se/mailman/listinfo/agda
> > _______________________________________________
> > 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/
>