What is `where .force`?

user_1744344 0
Viewed 97

I've been playing around with the idea of writing programs that run on Streams and properties with them, but I feel that I am stuck even with the simplest of things. When I look at the definition of repeat in Codata/Streams in the standard library, I find a construction that I haven't seen anywhere in Agda: λ where .force →.

Here, an excerpt of a Stream defined with this weird feature:

repeat : ∀ {i} → A → Stream A i
repeat a = a ∷ λ where .force → repeat a

Why does where appear in the middle of the lambda function definition?, and what is the purpose of .force if it is never used?

I might be asking something that is in the documentation, but I can't figure out how to search for it.

Also, is there a place where I can find documentation to use "Codata" and proofs with it? Thanks!

agda stream
2 Answers

Why does where appear in the middle of the lambda function definition?,

Quoting the docs:

Anonymous pattern matching functions can be defined using one of the two following syntaxes:

\ { p11 .. p1n -> e1 ; … ; pm1 .. pmn -> em }

\ where p11 .. p1n -> e1 … pm1 .. pmn -> em

So λ where is an anonymous pattern matching function. force is the field of Thunk and .force is a copattern in postfix notation (originally I said nonsense here, but thanks to @Cactus it's now fixed, see his answer).

Also, is there a place where I can find documentation to use "Codata" and proofs with it? Thanks!

Check out these papers

  1. Normalization by Evaluation in the Delay Monad A Case Study for Coinduction via Copatterns and Sized Types
  2. Equational Reasoning about Formal Languages in Coalgebraic Style
  3. Guarded Recursion in Agda via Sized Types
user_32374650

As one can see in the definition of Thunk, force is the field of the Thunk record type:

record Thunk {ℓ} (F : Size → Set ℓ) (i : Size) : Set ℓ where
  coinductive
  field force : {j : Size< i} → F j

So in the pattern-matching lambda, .force is not a dot pattern (why would it be? there is nothing prescribing the value of the parameter), but instead is simply syntax for the record field selector force. So the above code is equivalent to making a record with a single field called force with the given value, using copatterns:

repeat a = a :: as
  where
    force as = repeat a

or, which is actually where the .force syntax comes from, using postfix projection syntax:

repeat a = a :: as
  where
    as .force = repeat a
user_4774760
Related