Agda Store Comonad
Agda Store Comonad
我刚开始接触 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...
我不太确定我做错了什么。任何帮助,将不胜感激!谢谢!
编辑
我想我越来越接近了。我使用匹配的 lambda 替换了记录中的字段:
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 中的编译错误信息并没有提供很多线索,或者我还没有能够很好地理解它们。
哇,好的,我认为沉默是我需要的答案。我在定义 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
。
你的问题是λ s a → (Store s a)
(或者,eta-contracted,Store
)不是comonad;它的类型(或者,根据您的 Haskell 直觉,我们可以说它的类型)不正确。
但是,对于s
的任意选择,Store s
就是!所以让我们这样写:
StoreComonad : ∀ {s : Set} → RawComonad (Store s)
StoreComonad
的其余定义很容易理解。
顺便说一句,您可以通过使用 pattern-matching lambdas 而不是使用显式投影来使 StoreComonad
的定义更好(请务必阅读 link 因为看起来您混合了使用 pattern-matching 的普通 lambda 表达式);例如:
extract = λ { (f , a) → f a }
等等。
我刚开始接触 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...
我不太确定我做错了什么。任何帮助,将不胜感激!谢谢!
编辑
我想我越来越接近了。我使用匹配的 lambda 替换了记录中的字段:
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 中的编译错误信息并没有提供很多线索,或者我还没有能够很好地理解它们。
哇,好的,我认为沉默是我需要的答案。我在定义 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
。
你的问题是λ s a → (Store s a)
(或者,eta-contracted,Store
)不是comonad;它的类型(或者,根据您的 Haskell 直觉,我们可以说它的类型)不正确。
但是,对于s
的任意选择,Store s
就是!所以让我们这样写:
StoreComonad : ∀ {s : Set} → RawComonad (Store s)
StoreComonad
的其余定义很容易理解。
顺便说一句,您可以通过使用 pattern-matching lambdas 而不是使用显式投影来使 StoreComonad
的定义更好(请务必阅读 link 因为看起来您混合了使用 pattern-matching 的普通 lambda 表达式);例如:
extract = λ { (f , a) → f a }
等等。