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 allornothing proposition. If you discover that yo...") 
m (More minor formatting changes) 

(64 intermediate revisions by 2 users not shown)  
Line 1:  Line 1:  
−  [[Category:Proposals]] 

+  <div style="borderleft:1px solid lightgray; padding: 1em" alt="blockquote"> 

−  
+  Having praised monads to the hilt, let me level one criticism. Monads tend to be an allornothing 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 an allornothing 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> 

−  +  <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> 

+  </div> 

−  Some initial definitions: 

+  <sub> </sub> 

+  Assuming the [[Partiblepartible]] types being used are appropriately defined, then: 

<haskell> 
<haskell> 

−  class Partible a where 

+  instance Partible a => Monad ((>) a) where 

−  +  return x = \ u > case part u of !_ > x 

−  parts :: a > [a] 

−  +  m >>= k = \ u > case part u of 

−  +  (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 

−  +  (u1, u2) > case m u1 of !_ > w u2 

−  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 

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

−  primPartOI :: OI > (OI, OI)  primitive 

+  </haskell> 

−   type IO a = OI > a 

−  instance Partible OI where part = primPartOI 

+  Furthermore: 

+  <haskell> 

+  instance (Partible a, Monad ((>) a)) => MonadFix ((>) a) where 

+  mfix m = \ u > yet (\ x > m x u) 

−   more primitives 

+  instance (Partible a, Monad ((>) a), Partible b, Monad ((>) b)) => MonadCommute ((>) a) ((>) b) where 

−  +  mcommute g = \ v u > g u v 

−  primPutChar :: Char > OI > () 

−   copy 'n' paste from Wadler's paper 

+  instance (Monad m, Partible b, Monad ((>) b)) => MonadCommute m ((>) b) where 

−  type Dialogue = [Response] > [Request] 

+  mcommute m = \ v > liftM ($ v) m 

−  data Request = Getq  Putq Char 

+  </haskell> 

−  data Response = Getp Char  Putp 

+  where: 

−  respond :: Request > OI > Response 

+  :{ 

−  respond Getq = primGetChar >>= return . Getp 

+  <haskell> 

−  respond (Putq c) = primPutChar c >> return Putp 

+  yet :: (a > a) > a 

+  yet f = f (yet f) 

−  runDialogue :: Dialogue > OI > () 

+  class Monad m => MonadFix m where 

−  +  mfix :: (a > m a) > m a 

−  \u > let rspl = zipWith respond (d rspl) (parts u) in 

−  foldr (\ _ r > r) () rspl 

+  class (Monad m1, Monad m2) => MonadCommute m1 m2 where 

+  mcommute :: m1 (m2 a) > m2 (m1 a) 

+  </haskell> 

+  } 

−  instance Partible a => MonadFix ((>) a) where 

+  Using partible types to define monadic ones can enable an intermediate approach to the use of effects, in contrast to the ''allornothing 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. 

−  mfix m = \ u > fix (\ x > m x u)  fix f = f (fix f) 

+  === Composing arrows === 

−   to be made into an ADT... 

+  Partible types can also be used to define [[Arrowarrow]] types: 

−  data Fresh a = Fresh (OI > a) OI 

−  afresh :: (OI > a) > OI > Fresh a 

+  <haskell> 

−  +  type A p b c = (p > b) > (p > c) 

−  instance Partible (Fresh a) where 

+  arr :: Partible p => (b > c) > A p b c 

−  part (Fresh g u) = case part u of (u1, u2) > (Fresh g u1, Fresh g u2) 

+  arr f = \ c' u > f $! c' u 

−  fresh :: Fresh a > [a] 

+  infixr 3 *** 

−  +  (***) :: Partible p => A p b c > A p b' c' > A p (b, b') (c, c') 

−  +  f' *** 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 = case part u of !_ > x 

−  
−  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 

</haskell> 
</haskell> 

−  So what qualifies as being partible? 

+  (...though most will probably opt for the convenience of the associated [https://hackage.haskell.org/package/base4.15.0.0/docs/src/ControlArrow.html#Kleisli <code>Kleisli</code>] type). 

−  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. 

+   

+  See also: 

−  If its violation causes a runtime error, the useonce 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: 

+  * [[Plainly partible]] 

−  <haskell> 

+  * [[Partible laws]] 

−  let 

+  * [[Burtonstyle nondeterminism]] 

−  x = (primPutChar 'h' u `seq` primPutChar 'a' u) 

+  * [[MonadFix]] 

−  in x `seq` x 

+  * [[Prelude extensions]] 

−  </haskell> 

+  * [https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/bangpatterns.html Bang patterns] 

−  would trigger the error; the working version being: 

+  * [https://gitlab.haskell.org/ghc/ghc//issues/19809 GHC ticket 19809: Overhaul ST using ''pseudodatata''] 

−  <haskell> 

−  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 

−  </haskell> 

−  ...rather tedious, if it weren't for Haskell's standard monadic methods: 

−  <haskell> 

−  let 

−  x = primPutChar 'h' >> primPutChar 'a' 

−  in x >> x 

−  </haskell> 

−  Higherorder functions allows the manipulation of control e.g. <code>Prelude.until</code> 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. 

+  [[User:AtraversAtravers]] 04:31, 10 April 2018 (UTC) 

−  * ''Functional Pearl: On generating unique names'', Lennart Augustsson, Mikael Rittri and Dan Synek. 

+  [[Category:Monad]] 

−  
+  [[Category:Proposals]] 

−  * ''Can functional programming be liberated from the von Neumann paradigm?'', Conal Elliott. 

−  
−  * ''NonImperative 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. 

−  
−  [[User:AtraversAtravers]] ([[User talk:Atraverstalk]]) 04:31, 10 April 2018 (UTC) 
Latest revision as of 09:19, 21 August 2021
Having praised monads to the hilt, let me level one criticism. Monads tend to be an allornothing 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:
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 allornothing 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
infixr 3 ***
(***) :: Partible p => A p b c > A p b' c' > A p (b, b') (c, c')
f' *** 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 = case part u of !_ > x
(...though most will probably opt for the convenience of the associated Kleisli
type).
See also:
 Plainly partible
 Partible laws
 Burtonstyle nondeterminism
 MonadFix
 Prelude extensions
 Bang patterns
 GHC ticket 19809: Overhaul ST using pseudodatata
Atravers 04:31, 10 April 2018 (UTC)