<div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote">On Sat, Apr 5, 2014 at 1:46 PM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">-----BEGIN PGP SIGNED MESSAGE-----<br>
Hash: SHA1<br>
<div class=""><br>
On 05.04.2014 01:37, flicky frans wrote:<br>
&gt; Hi. I&#39;m playing with generic programming in Agda. I&#39;ve written a<br>
&gt; function, which can be used to construct combinators. Here are the<br>
&gt; examples: <a href="http://lpaste.net/4817148711178076160" target="_blank">http://lpaste.net/4817148711178076160</a> Here is the main<br>
&gt; module: <a href="http://lpaste.net/1337448319143641088" target="_blank">http://lpaste.net/1337448319143641088</a> The whole code is<br>
&gt; attached. I have some questions:<br>
&gt;<br>
&gt; Why doesn&#39;t agda have non-dependent pattern-matching? It&#39;s very<br>
&gt; usefull.<br></div></blockquote><div><br></div><div>We have pattern matching lambdas (which can also be dependent) and the</div><div>standard library defines in the Function module two functions case_of_ and</div><div>

case_return_of_ for non-dependent and dependent pattern matching respectively.</div><div>For instance</div><div><br></div><div><div>iszero : ℕ → Bool</div><div>iszero n =</div><div>  case n of λ</div><div>  { zero    → true</div>

<div>  ; (suc m) → false</div><div>  }</div></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">

<div class="">&gt; It would be nice to have the opportunity to rename fields in a<br>
&gt; datatypes. Something like: LTerm  n = TreeLike (Fin n) renaming<br>
&gt; (Leaf to Var; Branch to App) Or just Leaf = Var and Branch = App,<br>
&gt; but with opportunity to use Var and App in the pattern-matching.<br>
<br>
</div>You can use the pattern synonym facility:<br>
<br>
pattern App = Branch<br>
pattern Var = Leaf</blockquote><div><br></div><div>Or you can use the module system, which has a renaming facility:</div><div><br></div><div>module LT n where</div><div>  LTerm = TreeLike (Fin n)</div><div>  open TreeLike public  -- the module TreeLike contains the constructors of the datatype TreeLike</div>

<div><br></div><div>open LT renaming (Leaf to Var; Branch to App)</div><div><br></div><div>foo : ∀ {n} → LTerm n → LTerm n</div><div>foo (Var x)   = Var x</div><div>foo (App f v) = App (foo f) (foo v)</div><div><br></div>

<div>/ Ulf</div></div></div></div>