[Agda] Equality of arguments in Agda

[Ulf Norell]

On Mon, May 5, 2008 at 3:07 PM, Nils Anders Danielsson <
nils.anders.danielsson at gmail.com> wrote:

> On Mon, May 5, 2008 at 10:30 AM, Robert Rothenberg <robrwo at gmail.com>
> wrote:
> >
> > In Haskell, I can use the class system to define a function that works
> on
> > any type with equality [...]
>
> >  But I am unsure how to define such a function in Agda. As there is no
> class
> > system, how do I specify it should be type with equality, and then use
> it in
> > the function definition?
>
> By passing suitable arguments or dictionaries directly to the function:
>
> f : {a : Set} -> (a -> a -> Bool) -> ...
>
> To simplify things you can use parameterised modules:
>
> module M {a : Set} (_==_ : a -> a -> Bool) where
>  ...
>
> Or if you want to ensure that the function is a decidable equivalence
> relation:
>
> open import Relation.Binary
>
> module M (ds : DecSetoid) where
>  open DecSetoid ds
>  ...


Another alternative is to use what's called a universe construction. This is
nice when you know at which types you want to instantiate the function
beforehand. Here, I'm choosing natural numbers and lists of (lists of)
natural numbers (untested code):

data Code : Set where
  nat : Code
  list : Code -> Code

-- The decoder is called El for historical reasons.
El : Code -> Set
El nat = Nat
El (list a) = List (El a)

_==_ : {a : Code} -> El a -> El a -> Bool
_==_ {nat} n m = natEq n m
_==_ {list a} [] [] = true
_==_ {list a} (x :: xs) (y :: ys) = (x == y) && (xs == ys)
_==_ {list a} _ _ = false

transpose : {a : Code} -> El a -> El a -> El a -> El a
transpose x y z =
  if z == x then y
  else if z == y then x
  else z

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080505/ab3ce149/attachment.html