[Agda] Simple monoid instance based on monoid instance of underlying type

[Andreas Abel]

There is a simple explanation for the error you see:

   There is no connection whatsover between the type \tau and the 
carrier of the Monoid m.

To fix this, just use (Monoid.Carrier m) instead of \tau.  An voila, 
suddenly things work like a charm! ;-)

See attached file, or here:

   monoid : (m : Monoid zero zero) → Monoid zero zero
   monoid m = record
     { Carrier = Input τ
     ; _≈_      = _≡_
     ; _∙_      = binOp
     ; ε        = {!!}
     ; isMonoid = record
       { isSemigroup = record
         { isEquivalence = {!!}
         ; assoc         = {!!}
         ; ∙-cong        = {!!}
         }
       ; identity = {!!}
       }
     }
     where
       open Monoid m renaming (Carrier to τ)

       binOp : Input τ → Input τ → Input τ
       binOp (I a) (I b) = I (a ∙ b )

Cheers,
Andreas

On 12.01.14 10:39 AM, Mateusz Kowalczyk wrote:
> Hi all,
>
> I'm struggling with something that seemed like an easy task. Consider:
>
> ```
> open import Algebra
>
> record Input (τ : Set) : Set where
>    constructor I
>    field
>      unI : τ
> ```
>
> I now want to give a monoid instance to this type, as long as τ can
> give me one. That is, in Haskell I could say
>
> ```
> import Data.Monoid
>
> newtype I t = I t
>
> instance Monoid t => Monoid (I t) where
>    mempty = I mempty
>    I x `mappend` I y = I $ x `mappend` y
> ```
>
> In fact, I could use the GHC extension to derive this for me. I
> thought writing an instance like this in Agda should not be a problem
> at all but I seem to be struggling. In the snippet below is my failed
> attempt to replicate what the Haskell code does. I had hoped that I
> can simply pass the Monoid (or should I be using RawMonoid?) instance
> of the underlying type and use that. My problem with this is that I
> don't seem to be able to get out anything meaningful out of the passed
> in Monoid. For example, opening the ‘m’ and trying to use ε in my
> ‘binOp’ function quickly shoots me down with the message that ‘Carrier
> ≠ τ’. I'm unsure how to tell Agda that I only want to pass in the
> Monoid instances with τ as a Carrier or how to get the value out once
> I do: the Monoid type doesn't seem to be parametrised by anything but
> Level. I struggle to find any examples in standard lib or elsewhere of
> how to use passed in instances of Monoid from Data.Algebra: all I can
> find are either usages of monoids from other libraries or short
> documents which show off Agda by rolling their own.
>
> Here's the snippet. I imagine that the ‘monoid’ type needs fixing up
> so that I can actually use ‘m’ somehow.
>
> I'd appreciate if someone can point me in the right direction.
>
> ```
> module InputMonoid where
>    open import Level using (zero)
>    open import Relation.Binary.PropositionalEquality
>
>    monoid : (τ : Set) → (m : Monoid {!!} {!!}) → Monoid zero zero
>    monoid τ m = record
>      { Carrier = Input τ
>      ; _≈_      = _≡_
>      ; _∙_      = binOp
>      ; ε        = {!!}
>      ; isMonoid = record
>        { isSemigroup = record
>          { isEquivalence = {!!}
>          ; assoc         = {!!}
>          ; ∙-cong        = {!!}
>          }
>        ; identity = {!!}
>        }
>      }
>      where
>        open Monoid m
>
>        binOp : ∀ {τ} → Input τ → Input τ → Input τ
>        binOp (I unI) (I unI₁) = {!!}
> ```
>
> --
> Mateusz K.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------

open import Algebra

record Input (τ : Set) : Set where
  constructor I
  field
    unI : τ

module InputMonoid where
  open import Level using (zero)
  open import Relation.Binary.PropositionalEquality

  monoid : (m : Monoid zero zero) → Monoid zero zero
  monoid m = record
    { Carrier = Input τ
    ; _≈_      = _≡_
    ; _∙_      = binOp
    ; ε        = {!!}
    ; isMonoid = record
      { isSemigroup = record
        { isEquivalence = {!!}
        ; assoc         = {!!}
        ; ∙-cong        = {!!}
        }
      ; identity = {!!}
      }
    }
    where
      open Monoid m renaming (Carrier to τ)

      binOp : Input τ → Input τ → Input τ
      binOp (I a) (I b) = I (a ∙ b )