阿格达商店 Comonad答案

【问题标题】：Agda Store Comonad阿格达商店 Comonad
【发布时间】：2021-01-20 22:36:15
【问题描述】：

我刚开始使用 Agda，但了解一些 Haskell，想知道如何在 Agda 中定义 Store Comonad。

这是我到现在为止的：

   open import Category.Comonad
   open import Data.Product

   Store : Set → Set → ((Set → Set) × Set)
   Store s a = ((λ s → a) , s)

   StoreComonad : RawComonad (λ s a → (Store s a))
   StoreComonad = record
     { extract (Store s a) = extract s a
     ; extend f (Store s a = Store (extend (λ s' a' → f (Store s' a')) s) a
     } where open RawComonad

现在我收到以下错误：

Parse error
=<ERROR>
 extract s a
  ; extend f (Sto...

我不太确定我做错了什么。任何帮助，将不胜感激！谢谢！

编辑

我想我越来越近了。我使用匹配的 lambdas 替换了记录中的字段：

Store : Set → Set → ((Set → Set) × Set)
Store s a = ((λ s → a) , s)

StoreComonad : RawComonad (λ s a → (Store s a))
StoreComonad = record
  { extract   = λ st → (proj₁ st) (proj₂ st)
  ; duplicate = λ st → Store (λ s → Store (proj₁ st) s) (proj₂ st)
  ; extend    = λ g st → g (duplicate st)
  } where open RawComonad

RawComonad 来自https://github.com/agda/agda-stdlib/blob/master/src/Category/Comonad.agda 并有签名

record RawComonad (W : Set f → Set f) : Set (suc f)

Store 基于 Haskell 中的 type Store s a = (s -> a, s)。

现在我得到的错误是：

(a : Set) → Σ (Set → Set) (λ x → Set) !=< Set
when checking that the expression λ a → Store s a has type Set

我想知道这个错误是否与这一行有关：

StoreComonad : RawComonad (λ s a → (Store s a))

我发现Agda中的编译错误信息并没有给出太多线索或者我还不能很好地理解它们。

【问题讨论】：

定义记录时不能进行模式匹配。请改用where 子句或匹配的 lambda。
感谢您指出这一点！我正在尝试根据agda-stdlib-1.4 中的extract = head 和extend = unfold ∘′ < tail ,_> 中的Stream 实现方式来实现Store。我仍在努力思考如何定义 StoreComonad 实例。我是否需要将右侧实现为商店具有的功能，即这些功能是否是pos、peek、seek 等？

标签： agda comonad

【解决方案1】：

你的问题是λ s a → (Store s a)（或者，eta-contracted，Store）不是一个comonad；它的类型（或者，根据您的 Haskell 直觉，我们可以说它的类型）不正确。

但是，对于s，Store s 是！所以让我们这样写：

StoreComonad : ∀ {s : Set} → RawComonad (Store s)

StoreComonad 的其余定义很容易遵循。

顺便说一句，您可以通过使用 pattern-matching lambdas 而不是使用显式投影来更好地定义 StoreComonad（请阅读该链接，因为您似乎将普通 lambda 与模式匹配的 lambda 混为一谈）；例如：

  extract   = λ { (f , a) → f a }

等等。

【讨论】：

【解决方案2】：

哇，好吧，我认为沉默是我需要的答案。我设法在定义 Store Comonad 方面取得了很大进展：

S : Set
S = ℕ

Store : Set → Set
Store A = ((S → A) × S)

pos : ∀ {A : Set} → Store A → S
pos = λ st → proj₂ st

peek : ∀ {A : Set} → S → Store A → A
peek = λ s → λ st → (proj₁ st) s

fmap : ∀ {A : Set} {B : Set} → (A → B) → Store A → Store B
fmap = λ f → λ st → ((f ∘ proj₁ st) , proj₂ st)

duplicate' : ∀ {A : Set} → (Store A) → Store (Store A)
duplicate' = λ st → (λ s' → proj₁ st , s') , proj₂ st

StoreComonad : RawComonad Store
StoreComonad = record
  { extract = λ st → (proj₁ st) (proj₂ st)
  ; extend  = λ g st → fmap g (duplicate' st)
  } where open RawComonad

在此过程中，我了解到 C-c-C-l 和 C-c-C-r 与 ? 在尝试找到填充 ? 所需的类型时非常有帮助。我之前使用? 来证明一些示例，但没有尝试使用它来查找如何编写类型。

还剩下什么.. 我想做S 而不仅仅是Nat。

【讨论】：