Bodigrim/infinite-list

Diagonalizing monad instance

Closed this issue · 9 comments

-- | 'Control.Applicative.ZipList' cannot be made a lawful 'Monad',
-- but 'Infinite', being a
-- <https://hackage.haskell.org/package/adjunctions/docs/Data-Functor-Rep.html#t:Representable Representable>,
-- can. Namely, 'Control.Monad.join'
-- picks up a diagonal of an infinite matrix of 'Infinite' ('Infinite' @a@).
-- This is mostly useful for parallel list comprehensions once
-- @{\-# LANGUAGE MonadComprehensions #-\}@ is enabled.
instance Monad Infinite where
xs >>= f = go 0 xs
where
go n (y :< ys) = f y !! n :< go (n + 1) ys

The monad instance picks the main diagonal (0,0), (1,1), (2,2) ... What is the motivation for this over a more traditional striping instance, IE:

-- a0 :<
-- a1 :< b0 :<
-- a2 :< b1 :< c0 :<
-- ...
join =
  unfoldr \case
    (x:<xs):<xss ->
      (x, zipWith (:<) xs xss)

Unlike the current implementation, the striping one is reversible:

-- cantor's π function
π z = (x, y)
  where
    w = div (isqrt (8*z+1)-1) 2
    t = div (w*w + w) 2
    y = z - t
    x = w - y

unπ (x,y) =
  div ((x+y)*(x+y+1)) 2 + y

----

ix s (π(i,j)) =
  s !! j !! i

unix s is = go 0 is s
  where
    go i (j:<js) (drop (j-i)->a:<as) =
      a :< go (j+1) js as

----

nats = go 0 where
  go n = n :< go (n+1)

join'  Infinite (Infinite a)  Infinite a
join' s =
  map (ix s) nats

duplicate  Infinite a  Infinite (Infinite a)
duplicate s =
  map (unix s) $
    nats & map \i ->
    nats & map \j ->
      unπ (j, i)

Does your implementation satisfy monad laws?

Yes it does. It is the same instance as control-monad-omega or Moore from machines

The current implementation gives liftM2 = zipWith, so Data.List.Infinite is a ZipList if you will. My instance would give a liftM2 that does what the Applicative instance for Data.List does. This instance is non-determinism!

So if we want our Applicative instance to be consistent with Monad, we either leave it as is, or we change both.

If we leave it as is, I feel like we should provide this instance as a function- much like Data.List provides zipWith.

With the current instance and MonadComprehensions, [ (a,b) | a <- foo, b <- bar ] and [ (a,b) | a <- foo | b <- bar ]` does the exact same thing, but with the new instance it would do what you'd expect.

Yes it does. It is the same instance as control-monad-omega or Moore from machines

Documentation of control-monad-omega is clear that it does not satisfy monad laws.

Documentation of control-monad-omega is clear that it does not satisfy monad laws.

I might be wrong here, but I think this is only because it is implemented for finite lists. I'll investigate!

Negative. An obvious counter-example is m = m >>= pure. It might be a lawful bind instance, though, but we don't provide Bind!

Moore actually picks the main diagonal rather than stripes, their instance looks like this:

j ((a:<_):<as) = a :< j (fmap tail as)