Difference between revisions of "Partibles for composing monads"
(Created page with "Category:Proposals <blockquote><tt>Having praised monads to the hilt, let me level one criticism. Monads tend to be an all-or-nothing proposition. If you discover that yo...") |
|||
Line 1: | Line 1: | ||
[[Category:Proposals]] |
[[Category:Proposals]] |
||
− | |||
<blockquote><tt>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.</tt></blockquote> |
<blockquote><tt>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.</tt></blockquote> |
||
Revision as of 04:31, 10 April 2018
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.
- How to Declare an Imperative, Philip Wadler.
Some initial definitions:
class Partible a where
part :: a -> (a, a)
parts :: a -> [a]
-- Minimal complete definition: part or parts
part u = case parts u of u1:u2:_ -> (u1, u2)
parts u = case part u of (u1, u2) -> u1 : parts u2
instance Partible a => Monad ((->) a) where
return x = \ u -> part u `seq` x
m >>= k = \ u -> case part u of (u1, u2) -> (k $! m u1) u2
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
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 -> let rspl = zipWith respond (d rspl) (parts u) in
foldr (\ _ r -> r) () rspl
instance Partible a => MonadFix ((->) a) where
mfix m = \ u -> fix (\ x -> m x u) -- fix f = f (fix f)
-- to be made into an ADT...
data Fresh a = Fresh (OI -> a) OI
afresh :: (OI -> a) -> OI -> Fresh a
afresh g u = Fresh g u
instance Partible (Fresh a) where
part (Fresh g u) = case part u of (u1, u2) -> (Fresh g u1, Fresh g u2)
fresh :: Fresh a -> [a]
fresh u = [ g v | Fresh g v <- parts u ]
instance Functor Fresh where
fmap f (Fresh g u) = Fresh (f . g) u
-- one more primitive
primGensym :: OI -> Int
supplyInts :: OI -> Fresh Int
supplyInts = \ u -> afresh primGensym u
instance (Partible a, Partible b) => Partible (a, b) where
part (u, v) = case (part u, part v) of
((u1, u2), (v1, v2)) -> ((u1, v1), (u2, v2))
instance (Partible a, Partible b) => Partible (Either a b) where
part (Left u) = case part u of (u1, u2) -> (Left u1, Left u2)
part (Right v) = case part v of (v1, v2) -> (Right v1, Right v2)
type M1 a = (Fresh Int, OI) -> a
type M2 a = Either (Fresh a) 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 = \ u2 u1 -> m u1 u2
So what qualifies as being partible?
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 supplyInts.
If its violation causes a runtime error, the use-once property of partible values aids in maintaining referential transparency in the effectful segments of a program; using another example from Wadler's paper minimally rewritten in Haskell syntax using OI values:
let
x = (primPutChar 'h' u `seq` primPutChar 'a' u)
in x `seq` x
would trigger the error; the working version being:
let
x = (\ v -> case part v of
(v1, v2) -> primPutChar 'h' v1 `seq` primPutChar 'a' v2)
in
case part u of
(u1, u2) -> x u1 `seq` x u2
...rather tedious, if it weren't for Haskell's standard monadic methods:
let
x = primPutChar 'h' >> primPutChar 'a'
in x >> x
Higher-order functions allows the manipulation of control e.g. Prelude.until
in Haskell. As the definition of runDialogue 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.
Other references and articles:
- An alternative approach to I/O, Maarten Fokkinga and Jan Kuper.
- Functional Pearl: On generating unique names, Lennart Augustsson, Mikael Rittri and Dan Synek.
- Can functional programming be liberated from the von Neumann paradigm?, Conal Elliott.
- Non-Imperative Functional Programming, Nobuo Yamashita.
- MTL style for free, Tom Ellis.
- Functional I/O Using System Tokens, Lennart Augustsson.
Thank you to those who commented on early drafts of this document.