Difference between revisions of "Partibles for composing monads"
m |
m |
||
(28 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
+ | <div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | [[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><tt>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.</tt></blockquote> |
||
− | + | <small>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative], Philip Wadler.</small> |
|
+ | </div> |
||
+ | <sub> </sub> |
||
− | Some initial definitions: |
||
+ | Assuming the [[Partible|partible]] types being used are appropriately defined, then: |
||
<haskell> |
<haskell> |
||
− | + | type M p a = p -> a |
|
− | part :: a -> (a, a) |
||
− | parts :: a -> [a] |
||
− | + | unit :: Partible p => a -> M p a |
|
− | + | unit x = \ u -> let !_ = part u in x |
|
− | parts u = case part u of (u1, u2) -> u1 : parts u2 |
||
− | + | bind :: Partible p => M p a -> (a -> M p b) -> M p b |
|
− | + | m `bind` k = \ u -> let !(u1, u2) = part u in |
|
− | + | let !x = m u1 in |
|
− | + | let !y = k x u2 in |
|
− | + | y |
|
− | + | next :: Partible p => M p a -> M p b -> M p b |
|
− | + | m `next` w = \ u -> let !(u1, u2) = part u in |
|
− | + | let !x = m u1 in |
|
+ | let !y = w u2 in |
||
+ | y |
||
− | + | fail :: Partible p => String -> M p a |
|
+ | fail s = \ u -> let !_ = part u in error s |
||
− | |||
− | |||
− | -- 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 () (fix (\ l -> zipWith respond (d l) (parts u))) |
||
− | |||
− | -- fix f = f (fix f) |
||
− | |||
− | |||
− | instance Partible a => MonadFix ((->) a) where |
||
− | mfix m = \ u -> fix (\ 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 |
||
− | 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) |
||
− | |||
− | data Some a = Only a | More a (Some a) |
||
− | |||
− | instance Partible a => Partible (Some a) where |
||
− | part (Only u) = case part u of |
||
− | (u1, u2) -> (Only u1, Only u2) |
||
− | part (More u us) = case part u of |
||
− | (u1, u2) -> |
||
− | case part us of |
||
− | (us1, us2) -> (More u1 us1, More u2 us2) |
||
− | |||
− | 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 |
||
− | -- ...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? |
||
− | |||
− | 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>. |
||
− | |||
− | 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: |
||
<haskell> |
<haskell> |
||
− | + | mfix :: Partible p => (a -> M p a) -> M p a |
|
− | + | mfix m = \ u -> yet (\ x -> m x u) |
|
− | in x `seq` x |
||
− | </haskell> |
||
+ | mcommute :: (Partible p1, Partible p2) => M p1 (M p2 a) -> M p2 (M p1 a) |
||
+ | mcommute g = \ v u -> g u v |
||
+ | mcommute' :: (Monad m, Partible p) => m (M p a) -> M p (m a) |
||
− | would trigger the error; the working version being: |
||
+ | mcommute' m = \ v -> liftM ($ v) m |
||
− | |||
− | <haskell> |
||
− | let |
||
− | 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> |
</haskell> |
||
+ | where: |
||
+ | :{| |
||
− | ...rather tedious, if it weren't for Haskell's standard monadic methods: |
||
+ | |<haskell> |
||
− | |||
+ | yet :: (a -> a) -> a |
||
− | <haskell> |
||
− | + | yet f = f (yet f) |
|
− | 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. |
||
+ | === Composing arrows === |
||
− | 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. |
||
+ | Partible types can also be used to define [[Arrow|arrow]] types: |
||
− | The patches for an initial implementation in GHC are available:[https://tidbits.neocities.org/partibles-for-ghc.html ''] |
||
+ | <haskell> |
||
− | Other references and articles: |
||
+ | type A p b c = (p -> b) -> (p -> c) |
||
+ | arr :: Partible p => (b -> c) -> A p b c |
||
− | * [https://maartenfokkinga.github.io/utwente/mmf2001c.pdf ''An alternative approach to I/O''], Maarten Fokkinga and Jan Kuper. |
||
+ | arr f = \ c' u -> f $! c' u |
||
− | * ''Functional Pearl: On generating unique names'', Lennart Augustsson, Mikael Rittri and Dan Synek. |
||
+ | both :: Partible p => A p b c -> A p b' c' -> A p (b, b') (c, c') |
||
− | * [http://www.alsonkemp.com/haskell/reflections-on-leaving-haskell ''Reflections on leaving Haskell''], Alson Kemp. |
||
+ | f' `both` g' = \ c' u -> let !(u1:u2:u3:_) = parts u in |
||
+ | let !(x, x') = c' u1 in |
||
+ | let !y = f' (unit x) u2 in |
||
+ | let !y' = g' (unit x') u3 in |
||
+ | (y, y') |
||
+ | where |
||
+ | unit x u = let !_ = part u in x |
||
+ | </haskell> |
||
+ | (...though most will probably opt for the convenience of the associated [https://hackage.haskell.org/package/base-4.15.0.0/docs/src/Control-Arrow.html#Kleisli <code>Kleisli</code>] type). |
||
− | * [https://paul.bone.id.au/pub/pbone-2016-haskell-sucks.pdf ''Haskell Sucks!''], Paul Bone. |
||
+ | === Composing comonads === |
||
− | * ''Non-Imperative Functional Programming'', Nobuo Yamashita. |
||
+ | [[Comonad|Comonadic]] types can be defined using partible types as well: |
||
− | * [http://www.f.waseda.jp/terauchi/papers/toplas-witness.pdf ''Witnessing Side Effects''], Tachio Terauchi and Alex Aiken. |
||
+ | <haskell> |
||
− | * [https://www.cs.bham.ac.uk/~udr/papers/assign.pdf ''Assignments for Applicative Languages''], Vipin Swarup, Uday S. Reddy and Evan Ireland. |
||
+ | type C p a = (a, p) |
||
+ | extract :: Partible p => C p a -> a |
||
− | * [https://www.cs.ru.nl/barendregt60/essays/hartel_vree/art10_hartel_vree.pdf ''Lambda Calculus For Engineers''], Pieter H. Hartel and Willem G. Vree. |
||
+ | extract (x, u) = let !_ = part u in x |
||
+ | duplicate :: Partible p => C p a -> C p (C p a) |
||
− | * [http://www.cs.nott.ac.uk/~pszgmh/clairvoyant.pdf ''Call-by-Need Is Clairvoyant Call-by-Value''], Jennifer Hackett and Graham Hutton. |
||
+ | duplicate (x, u) = let !(u1, u2) = part u in |
||
− | |||
+ | ((x, u1), u2) |
||
− | * [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. |
||
− | |||
− | * ''Functional I/O Using System Tokens'', Lennart Augustsson. |
||
− | |||
− | * ''I/O Trees and Interactive Lazy Functional Programming'', Samuel A. Rebelsky. |
||
− | |||
− | * ''Arborescent data structures and lazy evaluation: A new approach to numerical problems'', Manuel Carcenac. |
||
+ | extend :: Partible p => (C p a -> b) -> C p a -> C p b |
||
+ | extend h (x, u) = let !(u1, u2) = part u in |
||
+ | let !y = h (x, u1) in |
||
+ | (y, u2) |
||
+ | </haskell> |
||
+ | ---- |
||
See also: |
See also: |
||
+ | * [[Plainly partible]] |
||
− | * [[Sequential ordering of evaluation]] |
||
+ | * [[Partible laws]] |
||
+ | * [[Burton-style nondeterminism]] |
||
+ | * [[MonadFix]] |
||
+ | * [[Prelude extensions]] |
||
+ | * [https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/bang-patterns.html Bang patterns] |
||
+ | * [https://gitlab.haskell.org/ghc/ghc/-/issues/19809 GHC ticket 19809: Overhaul ST using ''pseudodatata''] |
||
− | * [[Monomorphism by annotation of type variables]] |
||
− | |||
− | |||
− | 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:Arrow]] |
||
+ | [[Category:Monad]] |
||
+ | [[Category:Proposals]] |
Latest revision as of 08:14, 12 June 2023
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.
Assuming the partible types being used are appropriately defined, then:
type M p a = p -> a
unit :: Partible p => a -> M p a
unit x = \ u -> let !_ = part u in x
bind :: Partible p => M p a -> (a -> M p b) -> M p b
m `bind` k = \ u -> let !(u1, u2) = part u in
let !x = m u1 in
let !y = k x u2 in
y
next :: Partible p => M p a -> M p b -> M p b
m `next` w = \ u -> let !(u1, u2) = part u in
let !x = m u1 in
let !y = w u2 in
y
fail :: Partible p => String -> M p a
fail s = \ u -> let !_ = part u in error s
Furthermore:
mfix :: Partible p => (a -> M p a) -> M p a
mfix m = \ u -> yet (\ x -> m x u)
mcommute :: (Partible p1, Partible p2) => M p1 (M p2 a) -> M p2 (M p1 a)
mcommute g = \ v u -> g u v
mcommute' :: (Monad m, Partible p) => m (M p a) -> M p (m a)
mcommute' m = \ v -> liftM ($ v) m
where:
yet :: (a -> a) -> a yet f = f (yet f)
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.
Composing arrows
Partible types can also be used to define arrow types:
type A p b c = (p -> b) -> (p -> c)
arr :: Partible p => (b -> c) -> A p b c
arr f = \ c' u -> f $! c' u
both :: Partible p => A p b c -> A p b' c' -> A p (b, b') (c, c')
f' `both` g' = \ c' u -> let !(u1:u2:u3:_) = parts u in
let !(x, x') = c' u1 in
let !y = f' (unit x) u2 in
let !y' = g' (unit x') u3 in
(y, y')
where
unit x u = let !_ = part u in x
(...though most will probably opt for the convenience of the associated Kleisli
type).
Composing comonads
Comonadic types can be defined using partible types as well:
type C p a = (a, p)
extract :: Partible p => C p a -> a
extract (x, u) = let !_ = part u in x
duplicate :: Partible p => C p a -> C p (C p a)
duplicate (x, u) = let !(u1, u2) = part u in
((x, u1), u2)
extend :: Partible p => (C p a -> b) -> C p a -> C p b
extend h (x, u) = let !(u1, u2) = part u in
let !y = h (x, u1) in
(y, u2)
See also:
- Plainly partible
- Partible laws
- Burton-style nondeterminism
- MonadFix
- Prelude extensions
- Bang patterns
- GHC ticket 19809: Overhaul ST using pseudodatata
Atravers 04:31, 10 April 2018 (UTC)