Difference between revisions of "Partibles for composing monads"

From HaskellWiki
Jump to: navigation, search
m (Changing to secure URLS for references and articles.)
m (Minor formatting change)
 
(8 intermediate revisions by 2 users not shown)
Line 1: Line 1:
[[Category:Monad]]
 
  +
<i>
[[Category:Proposals]]
 
  +
Having praised monads to the hilt, let me level one criticism. Monads tend to be an all-or-nothing proposition. If you discover that you need interaction deep within your program, you must rewrite that segment to use a monad. If you discover that you need two sorts of interaction, you tend to make a single monad support both sorts. It seems to me that instead we should be able to move smoothly from no monads (no interactions) to one monad (a single form of interaction) to many monads (several independent forms of interactions). How to achieve this remains a challenge for the future.
<blockquote>''Having praised monads to the hilt, let me level one criticism. Monads tend to be<br>an all-or-nothing proposition. If you discover that you need interaction deep within<br>your program, you must rewrite that segment to use a monad. If you discover<br>that you need two sorts of interaction, you tend to make a single monad support<br>both sorts. It seems to me that instead we should be able to move smoothly from<br>no monads (no interactions) to one monad (a single form of interaction) to many<br>monads (several independent forms of interactions). How to achieve this remains a<br>challenge for the future.''</blockquote>
 
  +
</i>
 
  +
* <tt>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative], Philip Wadler.</tt>
* [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative], Philip Wadler.
 
   
Some sample definitions:
 
  +
<sub> </sub>
  +
Assuming the partible types being used are appropriately defined, then:
   
 
<haskell>
 
<haskell>
class Partible a where
 
  +
instance Partible a => Monad ((->) a) where
part :: a -> (a, a)
+
return x = \ u -> case part u of !_ -> x
parts :: a -> [a]
 
   
-- Minimal complete definition: part or parts
+
m >>= k = \ u -> case part u of
part u = case parts u of u1:u2:_ -> (u1, u2)
+
(u1, u2) -> case m u1 of !x -> k x u2
parts u = case part u of (u1, u2) -> u1 : parts u2
 
   
instance Partible a => Monad ((->) a) where
 
  +
m >> w = \ u -> case part u of
return x = \ u -> part u `seq` x
+
(u1, u2) -> case m u1 of !_ -> w u2
m >>= k = \ u -> case part u of (u1, u2) -> (\ x -> x `seq` k x u2) (m u1)
 
m >> w = \ u -> case part u of (u1, u2) -> m u1 `seq` w u2
 
fail s = \ u -> part u `seq` error s
 
   
data OI -- abstract
 
  +
fail s = \ u -> case part u of !_ -> error s
primPartOI :: OI -> (OI, OI) -- primitive
 
-- type IO a = OI -> a
 
 
instance Partible OI where part = primPartOI
 
 
 
-- more primitives
 
primGetChar :: OI -> Char
 
primPutChar :: Char -> OI -> ()
 
 
-- copy 'n' paste from Wadler's paper
 
type Dialogue = [Response] -> [Request]
 
data Request = Getq | Putq Char
 
data Response = Getp Char | Putp
 
 
 
respond :: Request -> OI -> Response
 
respond Getq = primGetChar >>= return . Getp
 
respond (Putq c) = primPutChar c >> return Putp
 
 
runDialogue :: Dialogue -> OI -> ()
 
runDialogue d =
 
\ u -> foldr seq () (yet (\ l -> zipWith respond (d l) (parts u)))
 
 
 
instance Partible a => MonadFix ((->) a) where
 
mfix m = \ u -> yet (\ x -> m x u)
 
 
 
-- to be made into an abstract data type...
 
data Fresh a = Fresh (OI -> a) OI
 
 
afresh :: (OI -> a) -> OI -> Fresh a
 
afresh g u = Fresh g u
 
 
instance Partible (Fresh a) where
 
parts (Fresh g u) = [ Fresh g v | v <- parts u ]
 
 
fresh :: Fresh a -> [a]
 
fresh (Fresh g u) = [ g v | v <- parts u ]
 
 
instance Functor Fresh where
 
fmap f (Fresh g u) = Fresh (f . g) u
 
 
 
-- another primitive
 
primGensym :: OI -> Int
 
 
supplyInts :: OI -> Fresh Int
 
supplyInts = \ u -> afresh primGensym u
 
 
 
-- another abstract data type
 
data Throw e
 
curb :: (Throw e -> a) -> (e -> OI -> a) -> OI -> a
 
catch :: (Throw e -> a) -> (e -> Throw e -> a) -> Throw e -> a
 
throw :: e -> Throw e -> a
 
 
partThrow :: Throw e -> (Throw e, Throw e)
 
instance Partible (Throw e) where part = partThrow
 
 
 
instance (Partible a, Partible b) => Partible (a, b) where
 
parts (u, v) = zipWith (,) (parts u) (parts v)
 
 
instance (Partible a, Partible b) => Partible (Either a b) where
 
parts (Left u) = map Left (parts u)
 
parts (Right v) = map Right (parts v)
 
 
data Some a = Only a | More a (Some a)
 
 
instance Partible a => Partible (Some a) where
 
parts (Only u) = map Only (parts u)
 
parts (More u us) = zipWith More (parts u) (parts us)
 
 
type M1 a = (Fresh Int, OI) -> a
 
type M2 a = Either (Fresh a) OI -> a
 
type M3 a = Some (Either (Fresh Char) (Fresh Int)) -> a
 
type M4 a = (Throw IOException, Some (Either Float OI)) -> a
 
-- ...whatever suits the purpose
 
 
 
class (Monad m1, Monad m2) => MonadCommute m1 m2 where
 
mcommute :: m1 (m2 a) -> m2 (m1 a)
 
 
instance (Partible a, Partible b) => MonadCommute ((->) a) ((->) b) where
 
mcommute m = \ v u -> m u v
 
 
</haskell>
 
</haskell>
   
  +
Furthermore:
   
So what qualifies as being partible?
 
  +
<haskell>
  +
instance (Partible a, Monad ((->) a)) => MonadFix ((->) a) where
  +
mfix m = \ u -> yet (\ x -> m x u)
   
A partible value can be used only once to generate new values that can be used for the same purpose. Think of a very large sheet of paper - new sheets can be made from it, other sheets can be made from those, etc, with the original sheet no longer in existence. Unlike paper sheets, partible values are intended to have no limits e.g. the result of applying <code>supplyInts</code>.
 
  +
instance (Partible a, Monad ((->) a), Partible b, Monad ((->) b)) => MonadCommute ((->) a) ((->) b) where
  +
mcommute g = \ v u -> g u v
   
If its violation causes a runtime error, the use-once property of partible values can help to maintain referential transparency in the effectful segments of a program; using another example from Wadler's paper minimally rewritten in Haskell syntax using <code>OI</code> values:
 
  +
instance (Monad m, Partible b, Monad ((->) b)) => MonadCommute m ((->) b) where
 
  +
mcommute m = \ v -> liftM ($ v) m
<haskell>
 
\ u -> let
 
x = (primPutChar 'h' u `seq` primPutChar 'a' u)
 
in x `seq` x
 
 
</haskell>
 
</haskell>
   
  +
where:
   
would trigger the error; the working version being:
 
  +
:{|
  +
|<haskell>
  +
yet :: (a -> a) -> a
  +
yet f = f (yet f)
   
<haskell>
 
  +
class Monad m => MonadFix m where
let
+
mfix :: (a -> m a) -> m a
x = (\ v -> case part v of
 
(v1, v2) -> primPutChar 'h' v1 `seq` primPutChar 'a' v2)
 
in
 
\ u -> case part u of
 
(u1, u2) -> x u1 `seq` x u2
 
</haskell>
 
   
 
  +
class (Monad m1, Monad m2) => MonadCommute m1 m2 where
...rather tedious, if it weren't for Haskell's standard monadic methods:
 
  +
mcommute :: m1 (m2 a) -> m2 (m1 a)
 
<haskell>
 
let
 
x = primPutChar 'h' >> primPutChar 'a'
 
in x >> x
 
 
</haskell>
 
</haskell>
  +
|}
   
  +
Using partible types to define monadic ones can enable an intermediate approach to the use of effects, in contrast to the ''all-or-nothing proposition'' of only using the monadic interface. In addition, if the definitions for such monadic types are ''visible'' (e.g. as type synonyms), this may also allow the manipulation of control in ways beyond what the monadic interface provides.
   
Higher-order functions allows the manipulation of control e.g. <code>Prelude.until</code> in Haskell. As the definition of <code>runDialogue</code> shows, monadic types with visible definitions based on types of partible values may also allow the manipulation of control in ways beyond what the standard monadic methods provide.
 
  +
----
 
The patches for an initial implementation in GHC are available:[https://tidbits.neocities.org/partibles-for-ghc.html '']
 
 
Other references and articles:
 
 
* [https://maartenfokkinga.github.io/utwente/mmf2001c.pdf An alternative approach to I/O], Maarten Fokkinga and Jan Kuper.
 
 
* <span style="color:#ba0000">Functional Pearl: On generating unique names</span>, Lennart Augustsson, Mikael Rittri and Dan Synek.
 
 
* [https://www.alsonkemp.com/haskell/reflections-on-leaving-haskell Reflections on leaving Haskell], Alson Kemp.
 
 
* [https://paul.bone.id.au/pub/pbone-2016-haskell-sucks.pdf Haskell Sucks!], Paul Bone.
 
 
* <span style="color:#ba0000">Non-Imperative Functional Programming</span>, Nobuo Yamashita.
 
 
* [https://www.f.waseda.jp/terauchi/papers/toplas-witness.pdf Witnessing Side Effects], Tachio Terauchi and Alex Aiken.
 
 
* [https://www.cs.bham.ac.uk/~udr/papers/assign.pdf Assignments for Applicative Languages], Vipin Swarup, Uday S. Reddy and Evan Ireland.
 
 
* [https://www.cs.ru.nl/barendregt60/essays/hartel_vree/art10_hartel_vree.pdf Lambda Calculus For Engineers], Pieter H. Hartel and Willem G. Vree.
 
 
* [https://www.cs.nott.ac.uk/~pszgmh/clairvoyant.pdf Call-by-Need Is Clairvoyant Call-by-Value], Jennifer Hackett and Graham Hutton.
 
 
* [http://h2.jaguarpaw.co.uk/posts/mtl-style-for-free MTL style for free], Tom Ellis.
 
 
* [https://accu.org/index.php/journals/2199 On Zero-Side-Effect Interactive Programming, Actors, and FSMs], Sergey Ignatchenko.
 
 
* <span style="color:#ba0000">Functional I/O Using System Tokens</span>, Lennart Augustsson.
 
 
* <span style="color:#ba0000">I/O Trees and Interactive Lazy Functional Programming</span>, Samuel A. Rebelsky.
 
 
* <span style="color:#ba0000">Arborescent data structures and lazy evaluation: A new approach to numerical problems</span>, Manuel Carcenac.
 
 
 
See also:
 
See also:
   
* [[Sequential ordering of evaluation]]
 
  +
* [[Plainly partible]]
 
  +
* [[Partible laws]]
* [[Monomorphism by annotation of type variables]]
 
  +
* [[Burton-style nondeterminism]]
 
  +
* [[MonadFix]]
 
* [[Prelude extensions]]
 
* [[Prelude extensions]]
  +
* [https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/bang-patterns.html Bang patterns]
   
   
Thank you to those who commented on early drafts of this document.
 
   
 
[[User:Atravers|Atravers]] 04:31, 10 April 2018 (UTC)
 
[[User:Atravers|Atravers]] 04:31, 10 April 2018 (UTC)
  +
  +
[[Category:Monad]]
  +
[[Category:Proposals]]

Latest revision as of 04:22, 27 April 2021

Having praised monads to the hilt, let me level one criticism. Monads tend to be an all-or-nothing proposition. If you discover that you need interaction deep within your program, you must rewrite that segment to use a monad. If you discover that you need two sorts of interaction, you tend to make a single monad support both sorts. It seems to me that instead we should be able to move smoothly from no monads (no interactions) to one monad (a single form of interaction) to many monads (several independent forms of interactions). How to achieve this remains a challenge for the future.

Assuming the partible types being used are appropriately defined, then:

instance Partible a => Monad ((->) a) where
    return x = \ u -> case part u of !_ -> x

    m >>= k  = \ u -> case part u of
                        (u1, u2) -> case m u1 of !x -> k x u2

    m >> w   = \ u -> case part u of
                        (u1, u2) -> case m u1 of !_ -> w u2

    fail s   = \ u -> case part u of !_ -> error s

Furthermore:

instance (Partible a, Monad ((->) a)) => MonadFix ((->) a) where
    mfix m = \ u -> yet (\ x -> m x u)

instance (Partible a, Monad ((->) a), Partible b, Monad ((->) b)) => MonadCommute ((->) a) ((->) b) where 
    mcommute g = \ v u -> g u v

instance (Monad m, Partible b, Monad ((->) b)) => MonadCommute m ((->) b) where
    mcommute m = \ v -> liftM ($ v) m

where:

yet   :: (a -> a) -> a
yet f =  f (yet f)

class Monad m => MonadFix m where
    mfix :: (a -> m a) -> m a

class (Monad m1, Monad m2) => MonadCommute m1 m2 where
    mcommute :: m1 (m2 a) -> m2 (m1 a)

Using partible types to define monadic ones can enable an intermediate approach to the use of effects, in contrast to the all-or-nothing proposition of only using the monadic interface. In addition, if the definitions for such monadic types are visible (e.g. as type synonyms), this may also allow the manipulation of control in ways beyond what the monadic interface provides.


See also:


Atravers 04:31, 10 April 2018 (UTC)