Agda Store Comonad

Question

I'm just starting with Agda but know some Haskell and would like to know how to define the Store Comonad in Agda.

This is what I have until now:

   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

For now I'm getting the following error:

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

I'm not too sure what it is I'm doing wrong. Any help would be appreciated! Thanks!

EDIT

I think I'm getting closer. I replaced the fields in the record using matching 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 is from https://github.com/agda/agda-stdlib/blob/master/src/Category/Comonad.agda and has the signature

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

and Store is based on type Store s a = (s -> a, s) in Haskell.

Now the error I'm getting is:

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

I'm wondering if this error has to do with this line:

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

I find that the compilation error messages in Agda don't give many clues or I haven't yet been able to understand them well.

Answer 1

Your problem is that λ s a → (Store s a) (or, eta-contracted, Store) is not a comonad; its type (or, for your Haskell intuition, we could say its kind) is not right.

However, for any choice of s, Store s is! So let's write that:

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

The rest of the definition of StoreComonad will follow easily.

As an aside, you can make the definition of StoreComonad nicer by using pattern-matching lambdas instead of using explicit projections (and please do read that link because it seems you have mixed up normal lambdas with pattern-matching ones); e.g:

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

and so on.

Answer 2

Wow, ok, I think silence was the answer I needed. I managed to advance quite a bit on defining the 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

along the way I learned that C-c-C-l and C-c-C-r with ? can be quite helpful in trying to find the type that is needed to fill the ?. I used ? for proving some examples before but hadn't tried using it to find how to write a type.

What's left.. I would like to make S not just a Nat.