<div dir="ltr">Hi Roman,<div><br></div><div>Maybe you can use a view (<a href="http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf">http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf</a> or <a href="http://dl.acm.org/citation.cfm?id=1411213">http://dl.acm.org/citation.cfm?id=1411213</a>). I was able to implement the following list view in my framework:</div><div><br></div><div><div><div>    data ListView (A : Set) (X : ⊤′ → Set) : ⟦ listDesc ⟧ (tt , A) X tt → Set where</div><div>      `[] : ListView A X (0 , refl)</div><div>      _`∷_ : ∀ x xs → ListView A X (1 , x , xs , refl)</div><div><br></div><div>    listView : ∀{A X} (xs : ⟦ listDesc ⟧ (tt , A) X tt) → ListView A X xs</div><div>    listView (zero , refl) = `[]</div><div>    listView (suc zero , x , xs , refl) = x `∷ xs</div><div>    listView (suc (suc ()) , _)</div></div></div><div><br></div><div>I can pattern match on the view:</div><div><br></div><div><div>    sumAlg : Alg listDesc (tt , Nat) (const Nat)</div><div>    sumAlg xs with listView xs</div><div>    sumAlg .(zero , refl) | `[] = 0</div><div>    sumAlg .(suc zero , x , xs , refl) | x `∷ xs = x + xs</div></div><div><br></div><div>I left the dot-patterns in, but you can replace them with _&#39;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.</div><div><br></div><div>Hope this helps!</div><div><br></div><div>Yorick</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Jun 18, 2016 at 12:18 PM, Roman <span dir="ltr">&lt;<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi, I&#39;m doing some generic programming and defining lots of pattern<br>
synonyms, but they are not equivalent to constructors due to their<br>
untyped nature. E.g. I have<br>
<br>
    pattern _∷_ x xs = cons₁ (x , xs , lrefl)<br>
<br>
Clearly, Agda can&#39;t infer that `_∷_` has type `∀ {α} {A : Set α} -&gt; A<br>
-&gt; List A -&gt; List A`, so the inferred type of `2 ∷ []` is `μ (_Ds_57 x<br>
xs) (_j_58 x xs)` instead of `List ℕ`, i.e. completely unspecified. It<br>
means that I need both a pattern `_∷_` and an operator<br>
<br>
    _∷′_ : ∀ {α} {A : Set α} -&gt; A -&gt; List A -&gt; List A<br>
    _∷′_ = _∷_<br>
<br>
to use on the RHS. It&#39;s rather inconvenient to have a pattern and a<br>
function instead of just one constructor, especially in my case as I<br>
want to figure out whether it&#39;s possible to type check existing code<br>
after changing data definitions to their generic counterparts.<br>
<br>
Ideally, I would like to write<br>
<br>
    pattern<br>
      _∷_ : ∀ {α} {A : Set α} -&gt; A -&gt; List A -&gt; List A<br>
      x ∷ xs = cons₁ (x , xs , lrefl)<br>
<br>
Is it possible to implement such a feature? Or maybe something else<br>
that would allow to use pattern synonyms as genuine constructors?<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>