[Agda] Generic programming and pointfree stuff.

[Ulf Norell]

On Sat, Apr 5, 2014 at 1:46 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> On 05.04.2014 01:37, flicky frans wrote:
> > Hi. I'm playing with generic programming in Agda. I've written a
> > function, which can be used to construct combinators. Here are the
> > examples: http://lpaste.net/4817148711178076160 Here is the main
> > module: http://lpaste.net/1337448319143641088 The whole code is
> > attached. I have some questions:
> >
> > Why doesn't agda have non-dependent pattern-matching? It's very
> > usefull.
>

We have pattern matching lambdas (which can also be dependent) and the
standard library defines in the Function module two functions case_of_ and
case_return_of_ for non-dependent and dependent pattern matching
respectively.
For instance

iszero : ℕ → Bool
iszero n =
  case n of λ
  { zero    → true
  ; (suc m) → false
  }

> It would be nice to have the opportunity to rename fields in a
> > datatypes. Something like: LTerm  n = TreeLike (Fin n) renaming
> > (Leaf to Var; Branch to App) Or just Leaf = Var and Branch = App,
> > but with opportunity to use Var and App in the pattern-matching.
>
> You can use the pattern synonym facility:
>
> pattern App = Branch
> pattern Var = Leaf


Or you can use the module system, which has a renaming facility:

module LT n where
  LTerm = TreeLike (Fin n)
  open TreeLike public  -- the module TreeLike contains the constructors of
the datatype TreeLike

open LT renaming (Leaf to Var; Branch to App)

foo : ∀ {n} → LTerm n → LTerm n
foo (Var x)   = Var x
foo (App f v) = App (foo f) (foo v)

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140406/9d09e907/attachment.html