为什么 Agda 中的 Haskell 类型类以 `Raw` 开头？

Question

在Agda标准库中，我们有RawMonad、RawApplicative等。

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)

为什么他们以 Raw 开头？ Agda 中有 Monad 或 Applicative 吗？

Answer 1

Nils Anders Danielsson（我怀疑是他们的作者）曾告诉我，这是因为他们不包含相应法律的证明。 AFAIK，Agda 标准库没有包含此类证明的版本，但如果您愿意，可以自己推出。

为什么 Agda 中的 Haskell 类型类以 `Raw` 开头？

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

agda