[Haskell-cafe] What to call Occult Effects

[Sergey Goncharov]

Dear Olaf,

>>
>> [1] H. Thielecke, Categorical structure of continuation passing
>> style, Ph.D. Thesis, University of
>> Edinburgh, 1997.
>>
>> [2] C. Führmann, Varieties of effects, in: M. Nielsen, U. Engberg
>> (Eds.), Foundations of Software
>> Science and Computation Structures, FOSSACS 2002, in: Lect. Notes
>> Comput. Sci., vol. 2303, Springer,
>> 2002, pp. 144–158.
>>
>> [3] L. Schröder, T. Mossakowski, Monad-independent dynamic logic in
>> HasCasl, J. Logic Comput. 14 (2004)
>> 571–619
> 
> I've got the impression that all three of the above works look at a
> problem dual to the OP in a certain sense: At least [1] and [2] ask:
> For a given monad M, what is the subset of computations b with
> b >> a = a for all a?
> In contrast, I understood Kim-Ee's question as: What are the monads M
> where all computations b belong to this class?

Well, these two questions are closely related, as you actually indicate further below. In [1] the main 
monad is the continuation monad, and equational laws are used as means to classify classes of 
computations with important properties, but nothing prevents one from using them for classifying monads 
entirely satisfying such laws.

> 
> Assuming this property, the monoid M () is isomorphic to ().
> Indeed, the monoid M () inherits the property
> a <> b = b
> for all a, b :: M () and the only monoid with this property is the one-
> element monoid.
> 
> In category theory a monad M with M 1 being isomorphic to the terminal
> object 1 is called 'affine'. Bart Jacobs in [4] gives a diagram (10)
> that amounts to
> return.const = fmap.const
> and shows that this is equivalent to being affine. Hence we might also
> use 'affine' for monads with Kim-Ee's property. Bart Jacobs' proof
> first reduces the  general identity
> 
> return.const = fmap.const :: a -> m b -> m a
> 
> to the case b = () just as Sergey did above. Then
> = fmap (const a)
> = fmap (const a) . (id :: m () -> m ())
> = fmap (const a) . return . const ()     by assumption
> = return . const a . const ()            by naturality of return
> = return . const a                       property of const
> 

Yes, it is again just the same law: isomorphism of M () and () is a yet more concise way to state this 
property, neat!

> I also learned that the school of 'effects' tries to avoid monads (this
> going back to John Power), so the terms 'discardable' and 'affine'
> might just be names for the same thing in different communities.
> 
> Further there is a categorical construction (see [4]) to compute the
> greatest affine sub-monad of a monad. Interestingly, the affine part of
> the state monad is the reader monad, that is, functions
> s -> (a,s)
> that may use s but not change it.
> 

I think [3] and [4] are related (and somewhat contrast [1] and [2]) in that, the laws like 
discardability are meant to identify those computations (or (sub-)monad), which can in a way play a role 
of logical assertions. So, the slogan is: assertions are well-behaved computations.

In that sense, from the perspective of [3], discardability is a desirable property, but not sufficient. 
For example, the 'copyability law'

	do {x <- p; y <- p; return (x, y)} = do {x <- p; return (x, x)}

is not satisfied by the probability distribution monad, which is discardable, roughly, because when 
tossing a coin, getting tails twice in a row is 1/4, while the probability of getting tails after 
tossing it once is 1/2. So, if we regard sequential composition of programs as a kind of conjunction, 
then it would not be idempotent.

 From the perspective of [4], not having copyability is fine, because the underlying logic is meant to 
be more permissive, and admits non-idempotent conjunctions. Same goes for commutativity: even the 
conjunction of copyability and discardability does not entail commutativity -- [3] contains a 
counterexample to this effect (Example 37).

Cheers,
Sergey

> 
> Olaf
> 
> 
> [4] https://hal.inria.fr/hal-01446033/file/418352_1_En_5_Chapter.pdf
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5384 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20201125/0dc3446d/attachment.bin>