[Agda] Re: record field as Instance Argument

[Guillermo Calderon - INCO]

On 24/04/15 14:44, Chris Jenkins wrote:
> Guillermo,
>
> Is there a particular reason you want A and EqA to be fields, instead of
> parameters?

Well, I would like to work with the two kinds of records. (with and 
without parameters )
since I am follow the way  of representing algebras presented in agda 
stdlib. For instance:

   1)  record IsMonoid {A} (≈ : Rel A) (∙ : Op₂ A) (ε : A) : Set where
              ...
   2)  record Monoid : Set1 where ...

In certain cases I find more appropriate the form 2) which allows to 
consider the  whole algebraic structure contained in the record.

> If not, you can do:
>
>     open import Data.Bool
>
>     record Eq (T : Set) : Set where
>        field
>          _==_ : (x y : T) → Bool
>
>        _/=_ : (x y : T) → Bool
>        x /= y = not (x == y)
>     open Eq ⦃...⦄
>
>     record A2 (A : Set) ⦃ EqA : Eq A ⦄ : Set where
>        field
>          a b : A
>
>        a≠b = a /= b
>
>
>
> On Thu, Apr 23, 2015 at 10:38 AM, Guillermo Calderon - INCO
> <calderon at fing.edu.uy
> <mailto:calderon at fing.edu.uy>> wrote:
>
>     Hi,
>
>     I am working with Instance Arguments to simulate Haskell classes
>     as explained here:
>
>     http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments
>
>     So, I have:
>
>       record Eq (t : Set) : Set where
>         field _==_ : t → t → Bool
>         _/=_ : t → t → Bool
>         a /= b = not $ a == b
>
>     and the following record definition:
>
>     record A2 : Set₁ where
>        field
>          A : Set
>          EqA : Eq A
>          a b : A
>        a≠b : Bool
>        a≠b =  a /= b
>
>     Agda gives an error at the last /= :
>     "No variable of type Eq A was found in scope".
>     But EqA is in the scope.  Why Agda does not consider it?
>
>     I can fix it defining an alias of EqA as an instance Eq.
>     The keyword instance is required.
>     I do not find the way to apply "instance" directly over the field EqA.
>
>     record A2 : Set₁ where
>        field
>          A : Set
>          EqA : Eq A
>          a b : A
>        instance foo = EqA
>        a≠b : Bool
>        a≠b =  a /= b
>
>     Is there a better  way to solve this?
>     Thanks,
>     Guillermo
>
>
>
>
>
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se
>     <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> --
> Christopher Jenkins
> Embedded Systems Software Engineer
> Genesi USA Inc.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>