[Agda] Agda patterns

[Martin Escardo]

But I would argue that this is an implementation issue, which should be 
hidden from the users, particularly users like me. :-)

On 01/05/2020 22:08, ulf.norell at gmail.com wrote:
> The difference is that you are not allowed to pattern match on datatype 
> parameters, since they
> are not stored in the constructor. In a right-hand side you can give the 
> parameters to guide the
> type checker, but they are thrown out during elaboration.
> 
> / Ulf
> 
> On Fri, May 1, 2020 at 10:56 PM Martin Escardo <m.escardo at cs.bham.ac.uk 
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
> 
>     Thanks, that works. (https://github.com/agda/agda/issues/4632)
> 
>     I still wonder why refl {x} and refl {_} {_} {x} behave differently
>     according to context.
> 
>     Best,
>     Martin
> 
>     On 01/05/2020 21:16, ulf.norell at gmail.com
>     <mailto:ulf.norell at gmail.com> wrote:
>      > pattern reflpv x = refl {x = x}
>      >
>      > / Ulf
>      >
>      >
>      > On Fri, May 1, 2020 at 6:39 PM Martin Escardo
>     <m.escardo at cs.bham.ac.uk <mailto:m.escardo at cs.bham.ac.uk>
>      > <mailto:m.escardo at cs.bham.ac.uk
>     <mailto:m.escardo at cs.bham.ac.uk>>> wrote:
>      >
>      >     Consider the following, which works:
>      >
>      >     data _≡_ {ℓ} {X : Set ℓ} : X → X → Set ℓ where
>      >         refl : {x : X} → x ≡ x
>      >
>      >     pattern reflp x = refl {x}
>      >     pattern reflv x = refl {_} {_} {x}
>      >
>      >     J : ∀ {i j} (X : Set i) (A : (x y : X) → x ≡ y → Set j)
>      >         → ((x : X) → A x x (reflv x))
>      >         → (x y : X) (p : x ≡ y) → A x y p
>      >     J X A f x x (reflp x) = f x
>      >
>      >     The idea is to make the argument of refl explicit if we wish,
>     via the
>      >     pattern definition.
>      >
>      >     However, the patterns behave differently "as patterns" and
>     "as values".
>      >     For instance, the following doesn't work:
>      >
>      >     J : ∀ {i j} (X : Set i) (A : (x y : X) → x ≡ y → Set j)
>      >         → ((x : X) → A x x (reflp x))  -- error here
>      >         → (x y : X) (p : x ≡ y) → A x y p
>      >     J X A f x x (reflp x) = f x
>      >
>      >     This doesn't work either:
>      >
>      >     J : ∀ {i j} (X : Set i) (A : (x y : X) → x ≡ y → Set j)
>      >         → ((x : X) → A x x (reflv x))
>      >         → (x y : X) (p : x ≡ y) → A x y p
>      >     J X A f x x (reflv x) = f x -- error here
>      >
>      >     It would be desirable to have a definition that works both as
>     a pattern
>      >     and as a value. Is that possible?
>      >
>      >     Thanks,
>      >     Martin
>      >     _______________________________________________
>      >     Agda mailing list
>      > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>>
>      > https://lists.chalmers.se/mailman/listinfo/agda
>      >
> 
>     -- 
>     Martin Escardo
>     http://www.cs.bham.ac.uk/~mhe
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe