[Agda] Partiality/delay monad

[Nils Anders Danielsson]

On 2018-03-20 16:10, Guillaume Allais wrote:
> E.g. (reusing your notations, forgetting about the very general setting
> for the moment) would it make sense to have:
> 
>    data [_]_≈_ (i : Size) :
>             Delay A ∞ → Delay A ∞ → Set a where
>        now    : ∀ {k x} → [ i ] now x ≈ now x
>        later  : ∀ {k x y} →
>                 [ i ] force x ≈′ force y →
>                 [ i ] later x ≈ later y
>        later-now : ∀ {k x y} →
>                 [ i ] force x ≈ now y →
>                 [ i ] later x ≈ now y
>        now-later : ∀ {x y} →
>                 [ i ] now x ≈ force y →
>                 [ i ] now x ≈ later y
> 
> ? Have you experimented with such a definition in the past?

This definition reminds me of Venanzio Capretta's definition of weak
bisimilarity. I have proved that his definition (defined using sized
types) is pointwise logically equivalent to the one that I use, in a
size-preserving way:

   http://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.Bisimilarity.Alternative.html

I guess that this also holds for your definition. I have no strong
argument for preferring one definition over the others.

There is another definition (also discussed by Venanzio) that has the
advantage of being propositional in the HoTT sense, assuming
extensionality, when the carrier type is a set (this observation is
possibly due to Thorsten Altenkirch):

   ∀ v → x ⇓ v ⇔ y ⇓ v

Here "x ⇓ v" means that x terminates with the value v; _⇓_ is defined
inductively.

This relation is also pointwise logically equivalent to the others.
However, it is not defined using sized types, so the translations are
not size-preserving, and I suspect (without any hard evidence) that it
would be tiresome to work directly with this type.

-- 
/NAD