<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title></title>
</head>
<body>
<div name="messageBodySection">
<div dir="auto">Anything of kind (* -> *) gives a codensity monad. What’s important is that only monad-like things (like the “bad” ziplist monad instance) can be lifted _into_ codensity in a universal way (otherwise you only get the “free” pure from codensity itself). And furthermore, only at least applicatives can be lowered back into the underlying functor via lowerCodensity. Note in particular:<br /></div>
<blockquote style="border-left-color: rgb(26, 188, 156); margin: 0px; padding-left: 10px; border-left-width: thin; border-left-style: solid;">
<blockquote style="border-left-color: rgb(230, 126, 34); margin: 0px; padding-left: 10px; border-left-width: thin; border-left-style: solid; padding-bottom: 5px; padding-top: 5px;">instance Serial m a => Serial m (Codensity ZL a) where</blockquote>
</blockquote>
<blockquote style="border-left-color: rgb(26, 188, 156); margin: 0px; padding-left: 10px; border-left-width: thin; border-left-style: solid;">
<blockquote style="border-left-color: rgb(230, 126, 34); margin: 0px; padding-left: 10px; border-left-width: thin; border-left-style: solid; padding-bottom: 5px; padding-top: 5px;">series = lift <$> series</blockquote>
</blockquote>
<div dir="auto"><br />
where lift in turn packs in the “bad” bind.<br />
<br />
So in particular, with codensity over ziplist, we get back something that zips like a ziplist but also has a valid monad instance. So that doesn’t say that ZipList [a] has a monad instance. But it does say that we can get something which acts as an applicative just like ZipList [a], but does have a valid monad instance. We just need a richer underlying type to express that algebraic structure.<br />
<br />
You might see this more clearly if you change the tests to not operate directly on “Codensity ZL” but instead to take arguments of “ZL” and manually lift them.<br />
<br />
More generally if you have something that is “almost a monad” but whose candidate bind does not associate, I think you can create something else which behaves the same in all other respects, but which is a monad, by using codensity to reassociate the bind.<br />
<br />
Maybe to highlight that something is happening at all, note that this trick can’t be done with the Const applicative, since there’s no good candidate bind operator that yields the desired <*>.<br />
<br />
-g</div>
</div>
<div name="messageReplySection">On Jun 5, 2020, 1:50 AM -0400, David Feuer <david.feuer@gmail.com>, wrote:<br />
<blockquote type="cite" style="border-left-color: grey; border-left-width: thin; border-left-style: solid; margin: 5px 5px;padding-left: 10px;">I'm not really sure what you're getting at here. Codensity will turn<br />
anything into a Monad. How does that relate to the question of whether<br />
there's a valid `Monad ZipList` instance?<br />
<br />
On Fri, Jun 5, 2020 at 1:42 AM Gershom B <gershomb@gmail.com> wrote:<br />
<blockquote type="cite"><br />
Using Roman’s smallcheck code (thanks!) here’s some evidence that codensity turns a bad diagonalizing ziplist instance into a good one, by fixing associativity. I’ve been pondering this for some time, and I’m glad this thread kicked me into making it work out. Also, as David noted, this works with or without the “take i” in the code, which enforces that minimum criteria I mentioned. So I suppose there’s a range of possibilities here.<br />
<br />
If this works out, it looks like this also shows that a “purely algebraic” argument as to why ZipList can’t be a monad doesn't exist. I.e. there’s no conflict in the laws. It’s just that using a plain list as the underlying datastructure can’t force a uniform associativity.<br />
<br />
To make a real “monadic ziplist” out of this, I think the codensity stuff would just need to be inlined under the ziplist constructor.<br />
<br />
Cheers,<br />
Gershom<br />
<br />
import Data.List<br />
import Data.Maybe<br />
import Test.SmallCheck.Series<br />
import Test.Tasty<br />
import Test.Tasty.SmallCheck<br />
import Control.Monad<br />
import Control.Applicative<br />
import System.Environment<br />
<br />
data ZL a = ZL {unZL :: [a]} deriving (Eq, Show)<br />
<br />
<br />
instance Functor ZL where<br />
fmap f (ZL xs) = ZL (fmap f xs)<br />
<br />
joinZL :: ZL (ZL a) -> ZL a<br />
joinZL (ZL []) = ZL []<br />
joinZL (ZL zs) = ZL (chop . diag (0,[]) $ map unZL zs)<br />
where diag :: (Int,[a]) -> [[a]] -> (Int,[a])<br />
diag (i,acc) [] = (i,acc)<br />
diag (i,acc) (x:xs) = case drop i x of<br />
[] -> (length x, acc)<br />
(y:_) ->diag (i+1, (y : acc)) xs<br />
chop (i,acc) = take i $ reverse acc<br />
<br />
instance Applicative ZL where<br />
pure = return<br />
f <*> x = joinZL $ fmap (\g -> fmap g x) f<br />
<br />
instance Monad ZL where<br />
return x = ZL (repeat x)<br />
x >>= f = joinZL $ fmap (f $) x<br />
<br />
<br />
newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }<br />
<br />
instance Functor (Codensity k) where fmap f (Codensity m) = Codensity (\k -> m (\x -> k (f x)))<br />
<br />
instance Applicative (Codensity f) where<br />
pure x = Codensity (\k -> k x)<br />
Codensity f <*> Codensity g = Codensity (\bfr -> f (\ab -> g (\x -> bfr (ab x))))<br />
<br />
instance Monad (Codensity f) where<br />
return = pure<br />
m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))<br />
<br />
lowerCodensity :: Monad m => Codensity m a -> m a<br />
lowerCodensity a = runCodensity a return<br />
<br />
lift m = Codensity (m >>=)<br />
<br />
-- tests<br />
<br />
instance Serial m a => Serial m (ZL a) where<br />
series = ZL <$> series<br />
<br />
instance Serial m a => Serial m (Codensity ZL a) where<br />
series = lift <$> series<br />
<br />
instance Show (Codensity ZL Int) where<br />
show x = show (lowerCodensity x)<br />
<br />
instance Show (Codensity ZL Bool) where<br />
show x = show (lowerCodensity x)<br />
<br />
main = do<br />
setEnv "TASTY_SMALLCHECK_DEPTH" "4"<br />
defaultMain $ testGroup "Monad laws"<br />
[ testProperty "Right identity" $ \(z :: Codensity ZL Int) -><br />
lowerCodensity (z >>= return) == lowerCodensity z<br />
, testProperty "Left identity" $ \(b :: Bool) (f :: Bool -> Codensity ZL Bool) -><br />
lowerCodensity (return b >>= f) == lowerCodensity (f b)<br />
, testProperty "Associativity" $<br />
\(f1 :: Bool -> Codensity ZL Bool)<br />
(f2 :: Bool -> Codensity ZL Bool)<br />
(z :: Codensity ZL Bool) -><br />
lowerCodensity (z >>= (\x -> f1 x >>= f2)) == lowerCodensity ((z >>= f1) >>= f2)<br />
]<br />
On Jun 4, 2020, 4:04 PM -0400, Roman Cheplyaka <roma@ro-che.info>, wrote:<br />
<br />
On 04/06/2020 09.53, Dannyu NDos wrote:<br />
<br />
instance Monad ZipList where<br />
ZipList [] >>= _ = ZipList []<br />
ZipList (x:xs) >>= f = ZipList $ do<br />
let ZipList y' = f x<br />
guard (not (null y'))<br />
let ZipList ys = ZipList xs >>= ZipList . join . maybeToList . fmap snd . uncons . getZipList . f<br />
head y' : ys<br />
<br />
instance MonadFail ZipList where<br />
fail _ = empty<br />
<br />
instance MonadPlus ZipList<br />
<br />
<br />
While others have commented on the general feasibility of the idea, the problem with this specific instance is that it appears to violate the associativity law:<br />
<br />
% ./ziplist --smallcheck-depth=3<br />
Monad laws<br />
Right identity: OK<br />
21 tests completed<br />
Left identity: OK<br />
98 tests completed<br />
Associativity: FAIL (0.04s)<br />
there exist {True->ZipList {getZipList = [True]};False->ZipList {getZipList = [False,True]}} {True->ZipList {getZipList = [True,True]};False->ZipList {getZipList = []}} ZipList {getZipList = [True,False]} such that<br />
condition is false<br />
<br />
1 out of 3 tests failed (0.05s)<br />
<br />
<br />
Here's the code I used for testing:<br />
<br />
{-# LANGUAGE ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses #-}<br />
import Control.Applicative<br />
import Control.Monad<br />
import Data.List<br />
import Data.Maybe<br />
import Test.SmallCheck.Series<br />
import Test.Tasty<br />
import Test.Tasty.SmallCheck<br />
<br />
instance Monad ZipList where<br />
ZipList [] >>= _ = ZipList []<br />
ZipList (x:xs) >>= f = ZipList $ do<br />
let ZipList y' = f x<br />
guard (not (null y'))<br />
let ZipList ys = ZipList xs >>= ZipList . join . maybeToList . fmap snd . uncons . getZipList . f<br />
head y' : ys<br />
<br />
instance Serial m a => Serial m (ZipList a) where<br />
series = ZipList <$> series<br />
<br />
main = defaultMain $ testGroup "Monad laws"<br />
[ testProperty "Right identity" $ \(z :: ZipList Int) -><br />
(z >>= return) == z<br />
, testProperty "Left identity" $ \(b :: Bool) (f :: Bool -> ZipList Bool) -><br />
(return b >>= f) == f b<br />
, testProperty "Associativity" $<br />
\(f1 :: Bool -> ZipList Bool)<br />
(f2 :: Bool -> ZipList Bool)<br />
(z :: ZipList Bool) -><br />
(z >>= (\x -> f1 x >>= f2)) == ((z >>= f1) >>= f2)<br />
]<br />
<br />
Roman<br />
_______________________________________________<br />
Libraries mailing list<br />
Libraries@haskell.org<br />
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries<br />
<br />
_______________________________________________<br />
Libraries mailing list<br />
Libraries@haskell.org<br />
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries<br /></blockquote>
</blockquote>
</div>
</body>
</html>