[Agda] A feature request: typed pattern synonyms.

[Yorick Sijsling]

Hi Roman,

Maybe you can use a view (
http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf or
http://dl.acm.org/citation.cfm?id=1411213). I was able to implement the
following list view in my framework:

    data ListView (A : Set) (X : ⊤′ → Set) : ⟦ listDesc ⟧ (tt , A) X tt →
Set where
      `[] : ListView A X (0 , refl)
      _`∷_ : ∀ x xs → ListView A X (1 , x , xs , refl)

    listView : ∀{A X} (xs : ⟦ listDesc ⟧ (tt , A) X tt) → ListView A X xs
    listView (zero , refl) = `[]
    listView (suc zero , x , xs , refl) = x `∷ xs
    listView (suc (suc ()) , _)

I can pattern match on the view:

    sumAlg : Alg listDesc (tt , Nat) (const Nat)
    sumAlg xs with listView xs
    sumAlg .(zero , refl) | `[] = 0
    sumAlg .(suc zero , x , xs , refl) | x `∷ xs = x + xs

I left the dot-patterns in, but you can replace them with _'s to clean
things up. A case split (C-c C-c) also generates these constructors
automatically, while pattern synonyms often require some manual work in
that area.

Hope this helps!

Yorick


On Sat, Jun 18, 2016 at 12:18 PM, Roman <effectfully at gmail.com> wrote:

> Hi, I'm doing some generic programming and defining lots of pattern
> synonyms, but they are not equivalent to constructors due to their
> untyped nature. E.g. I have
>
>     pattern _∷_ x xs = cons₁ (x , xs , lrefl)
>
> Clearly, Agda can't infer that `_∷_` has type `∀ {α} {A : Set α} -> A
> -> List A -> List A`, so the inferred type of `2 ∷ []` is `μ (_Ds_57 x
> xs) (_j_58 x xs)` instead of `List ℕ`, i.e. completely unspecified. It
> means that I need both a pattern `_∷_` and an operator
>
>     _∷′_ : ∀ {α} {A : Set α} -> A -> List A -> List A
>     _∷′_ = _∷_
>
> to use on the RHS. It's rather inconvenient to have a pattern and a
> function instead of just one constructor, especially in my case as I
> want to figure out whether it's possible to type check existing code
> after changing data definitions to their generic counterparts.
>
> Ideally, I would like to write
>
>     pattern
>       _∷_ : ∀ {α} {A : Set α} -> A -> List A -> List A
>       x ∷ xs = cons₁ (x , xs , lrefl)
>
> Is it possible to implement such a feature? Or maybe something else
> that would allow to use pattern synonyms as genuine constructors?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160620/ad7673df/attachment.html