------------------------------------------------------------------------ -- This approach is incorrect, but perhaps subtly so ------------------------------------------------------------------------ -- Note that in an inductive setting, where all expressions were -- finite, this semantics (correspondingly modified) would be OK. -- Hence it may be easy to mistakenly assume that this semantics is -- also OK; at least I initially did so. module Deterministic.Incorrect where open import Data.Colist open import Coinduction open import Deterministic.Expr infix 4 _HasTrace_ data _HasTrace_ : Semantics where nop : ∀ {e ms} (s : ∞ (♭ e HasTrace ms)) → nop e HasTrace ms tick : ∀ {e m ms} (s : ∞ (♭ e HasTrace ♭ ms)) → tick m e HasTrace m ∷ ms ------------------------------------------------------------------------ -- Examples possible : nops HasTrace [] possible = nop (♯ possible) -- Should not be allowed, since nops does not emit any messages: should-be-impossible : ∀ {m ms} → nops HasTrace (m ∷ ms) should-be-impossible = nop (♯ should-be-impossible) ok : ticks HasTrace scissors ok = tick (♯ ok)