在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
吗?
最佳答案
尼尔斯·安德斯·丹尼尔森(Nils Anders Danielsson,我怀疑是他们的作者)曾告诉我,这是因为它们不包含相应法律的证据。 AFAIK,Agda 标准库没有包含此类证明的版本,但如果您愿意,您可以推出自己的版本。
关于agda - 为什么 Agda 中的 Haskell 类型类以 `Raw` 开头?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/47172083/