Why Haskell typeclasses in Agda are started with `Raw`?

2
votes

In the Agda standard library, we have RawMonad, RawApplicative, etc..

RawMonad : ∀ {f} → (Set f → Set f) → Set _
RawMonad M = RawIMonad {I = ⊤} (λ _ _ → M)

RawMonadZero : ∀ {f} → (Set f → Set f) → Set _
RawMonadZero M = RawIMonadZero {I = ⊤} (λ _ _ → M)

RawMonadPlus : ∀ {f} → (Set f → Set f) → Set _
RawMonadPlus M = RawIMonadPlus {I = ⊤} (λ _ _ → M)

Why do they start with Raw? Are there Monad or Applicative in Agda?

1
agda

1 Answers

4
votes

I've been told by Nils Anders Danielsson (their author, I suspect) once that it's because they don't contain proofs of the respective laws. AFAIK, the Agda standard library doesn't have versions of these that do contain such proofs, but you can roll your own if you like.