[Agda] Something like type classes in Agda?

[Nils Anders Danielsson]

On 2011-10-10 11:26, Dirk Ullrich wrote:
> can implement or fake something like type classes in Agda?
>
> A simple example: I can implement, for instance, a product binary type
> either by using `data' or `record'. I can put these implementations in
> different modules but give them the same 'API' - say `_x_' for the
> type constructor, `<_,_>  for the pairing and `pr0', `pr1' for the
> projection function. Now I do not want to care whose of these modules
> I use in other modules that need binary products.

record Product-type : Set₁ where
   field
     _×_ : Set → Set → Set
     _,_ : {A B : Set} → A → B → A × B
     pr₀ : {A B : Set} → A × B → A
     pr₁ : {A B : Set} → A × B → A

module Uses-products (P : Product-type) where

   open Product-type P

   ...

You may also want to look at "instance arguments" (ICFP 2011).

-- 
/NAD