Difference between revisions of "Partibles for composing monads"
m (Remove <br> in Philip Wadler blockquote (which cause line breaks on mobile devices)) 

(21 intermediate revisions by one other user not shown)  
Line 1:  Line 1:  
+  [[Category:Monad]] 

[[Category:Proposals]] 
[[Category:Proposals]] 

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

+  * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative], Philip Wadler. 

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

+  Some sample definitions: 

−  
−  * [https://wiki.ittc.ku.edu/lambda/images/3/3b/Wadler__How_to_Declare_an_Imperative.pdf ''How to Declare an Imperative''], Philip Wadler. 

−  
−  Some initial definitions: 

<haskell> 
<haskell> 

Line 46:  Line 45:  
runDialogue :: Dialogue > OI > () 
runDialogue :: Dialogue > OI > () 

runDialogue d = 
runDialogue d = 

−  \ u > foldr seq () ( 
+  \ u > foldr seq () (yet (\ l > zipWith respond (d l) (parts u))) 
−  
−   fix f = f (fix f) 

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

−  mfix m = \ u > 
+  mfix m = \ u > yet (\ x > m x u) 
Line 60:  Line 59:  
instance Partible (Fresh a) where 
instance Partible (Fresh a) where 

−  +  parts (Fresh g u) = [ Fresh g v  v < parts u ] 

fresh :: Fresh a > [a] 
fresh :: Fresh a > [a] 

−  fresh u = [ g v  
+  fresh (Fresh g u) = [ g v  v < parts u ] 
instance Functor Fresh where 
instance Functor Fresh where 

Line 69:  Line 68:  
−   
+   another primitive 
primGensym :: OI > Int 
primGensym :: OI > Int 

supplyInts :: OI > Fresh Int 
supplyInts :: OI > Fresh Int 

supplyInts = \ u > afresh primGensym u 
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 
instance (Partible a, Partible b) => Partible (a, b) where 

−  +  parts (u, v) = zipWith (,) (parts u) (parts v) 

−  ((u1, u2), (v1, v2)) > ((u1, v1), (u2, v2)) 

instance (Partible a, Partible b) => Partible (Either a b) where 
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) 
data Some a = Only a  More a (Some a) 

instance Partible a => Partible (Some a) where 
instance Partible a => Partible (Some a) where 

−  +  parts (Only u) = map Only (parts u) 

−  +  parts (More u us) = zipWith More (parts u) (parts us) 

−  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 M1 a = (Fresh Int, OI) > a 

type M2 a = Either (Fresh a) OI > a 
type M2 a = Either (Fresh a) OI > a 

type M3 a = Some (Either (Fresh Char) (Fresh Int)) > 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 
 ...whatever suits the purpose 

Line 139:  Line 149:  
Higherorder 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. 
Higherorder 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/partiblesforghc.html ''] 

Other references and articles: 
Other references and articles: 

−  * [https://maartenfokkinga.github.io/utwente/mmf2001c.pdf 
+  * [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. 
−  * [http://www.alsonkemp.com/haskell/reflectionsonleavinghaskell ''Reflections on leaving Haskell''], Alson Kemp. 

+  * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.128.9269&rep=rep1&type=pdf Unique Identifiers in Pure Functional Languages], Peter Divianszky. 

−  * [https://www.slideshare.net/nobsun/lazyio ''NonImperative Functional Programming''], Nobuo Yamashita. 

+  * [https://academic.oup.com/comjnl/articlepdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages], F. Warren Burton. 

−  * [http://www.f.waseda.jp/terauchi/papers/toplaswitness.pdf ''Witnessing Side Effects''], Tachio Terauchi and Alex Aiken. 

+  * [https://www.alsonkemp.com/haskell/reflectionsonleavinghaskell Reflections on leaving Haskell], Alson Kemp. 

−  * [https://www.cs.bham.ac.uk/~udr/papers/assign.pdf ''Assignments for Applicative Languages''], Vipin Swarup, Uday S. Reddy and Evan Ireland. 

+  * [https://paul.bone.id.au/pub/pbone2016haskellsucks.pdf Haskell Sucks!], Paul Bone. 

−  * [https://www.cs.ru.nl/barendregt60/essays/hartel_vree/art10_hartel_vree.pdf ''Lambda Calculus For Engineers''], Pieter H. Hartel and Willem G. Vree. 

+  * <span style="color:#ba0000">NonImperative Functional Programming</span>, Nobuo Yamashita. 

−  * [http://h2.jaguarpaw.co.uk/posts/mtlstyleforfree ''MTL style for free''], Tom Ellis. 

+  * [https://www.f.waseda.jp/terauchi/papers/toplaswitness.pdf Witnessing Side Effects], Tachio Terauchi and Alex Aiken. 

−  * [https://accu.org/index.php/journals/2199 ''On ZeroSideEffect Interactive Programming, Actors, and FSMs''], Sergey Ignatchenko. 

+  * [https://www.cs.bham.ac.uk/~udr/papers/assign.pdf Assignments for Applicative Languages], Vipin Swarup, Uday S. Reddy and Evan Ireland. 

−  * ''Functional I/O Using System Tokens'', Lennart Augustsson. 

+  * [https://www.cs.bham.ac.uk/~udr/papers/imperativefunctional.pdf Imperative Functional Programming], Uday S. Reddy. 

−  * ''I/O Trees and Interactive Lazy Functional Programming'', Samuel A. Rebelsky. 

+  * [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 CallbyNeed Is Clairvoyant CallbyValue], Jennifer Hackett and Graham Hutton. 

+  
+  * [http://h2.jaguarpaw.co.uk/posts/mtlstyleforfree MTL style for free], Tom Ellis. 

+  
+  * [https://accu.org/index.php/journals/2199 On ZeroSideEffect 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: 

Line 169:  Line 192:  
* [[Monomorphism by annotation of type variables]] 
* [[Monomorphism by annotation of type variables]] 

+  
+  * [[Prelude extensions]] 

Latest revision as of 21:41, 25 February 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.
Some sample 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) > (\ 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
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
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 useonce 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 OI
values:
\ u > 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
\ u > 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
Higherorder 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.
The patches for an initial implementation in GHC are available:
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.
 Unique Identifiers in Pure Functional Languages, Peter Divianszky.
 Reflections on leaving Haskell, Alson Kemp.
 Haskell Sucks!, Paul Bone.
 NonImperative Functional Programming, Nobuo Yamashita.
 Witnessing Side Effects, Tachio Terauchi and Alex Aiken.
 Assignments for Applicative Languages, Vipin Swarup, Uday S. Reddy and Evan Ireland.
 Imperative Functional Programming, Uday S. Reddy.
 Lambda Calculus For Engineers, Pieter H. Hartel and Willem G. Vree.
 CallbyNeed Is Clairvoyant CallbyValue, Jennifer Hackett and Graham Hutton.
 MTL style for free, Tom Ellis.
 On ZeroSideEffect 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.
See also:
Thank you to those who commented on early drafts of this document.
Atravers 04:31, 10 April 2018 (UTC)