Nottingham FP Lab Blog

Indexing a coinductive type on a trace

by Nils Anders Danielsson on January 9, 2009.
Tagged as: Lunches.

Consider the following simple language, represented as a coinductive data type in Agda:

codata Expr : Set where
  nop  : Expr → Expr
  send : Msg → Expr → Expr

An expression is an infinite sequence of no-ops and send instructions. Assume now that we want to index the Expr type on exactly the messages being sent. One might believe that the following definition is OK:

codata Expr : Colist Msg → Set where
  nop  : ∀ {ms} → Expr ms → Expr ms
  send : ∀ {ms ms′} (m : Msg) → Expr ms → ms′ ≈ m ∷ ms → Expr ms′

However, this definition has a problem; it does not actually enforce that all the messages in the index are being sent, as demonstrated by the expression incorrect:

incorrect : ∀ {ms} → Expr ms
incorrect ~ nop incorrect

In the meeting today we discussed various ways to address this problem.

(You may wonder why send is not given the type

∀ {ms} (m : Msg) → Expr ms → Expr (m ∷ ms).

The reason is that this can make it harder to construct values in the Expr family; the coinductive equality _≈_ is stronger than Agda’s built-in one.)