Difference between revisions of "Partibles for composing monads"

From HaskellWiki
Jump to: navigation, search
m
 
(47 intermediate revisions by the same user not shown)
Line 1: Line 1:
  +
[[Category:Monad]]
 
[[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>''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>
   
* ''How to Declare an Imperative'', Philip Wadler.
+
* [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative], Philip Wadler.
   
Some initial definitions:
+
Some sample definitions:
   
 
<haskell>
 
<haskell>
 
class Partible a where
 
class Partible a where
 
part :: a -> (a, a)
 
part :: a -> (a, a)
parts :: a -> [a]
+
parts :: a -> [a]
   
 
-- Minimal complete definition: part or parts
 
-- Minimal complete definition: part or parts
part u = case parts u of u1:u2:_ -> (u1, u2)
+
part u = case parts u of u1:u2:_ -> (u1, u2)
 
parts u = case part u of (u1, u2) -> u1 : parts u2
 
parts u = case part u of (u1, u2) -> u1 : parts u2
   
 
instance Partible a => Monad ((->) a) where
 
instance Partible a => Monad ((->) a) where
 
return x = \ u -> part u `seq` x
 
return x = \ u -> part u `seq` x
m >>= k = \ u -> case part u of (u1, u2) -> (k $! m u1) 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
 
m >> w = \ u -> case part u of (u1, u2) -> m u1 `seq` w u2
 
fail s = \ u -> part u `seq` error s
 
fail s = \ u -> part u `seq` error s
Line 40: Line 41:
 
respond :: Request -> OI -> Response
 
respond :: Request -> OI -> Response
 
respond Getq = primGetChar >>= return . Getp
 
respond Getq = primGetChar >>= return . Getp
respond (Putq c) = primPutChar c >> return Putp
+
respond (Putq c) = primPutChar c >> return Putp
   
 
runDialogue :: Dialogue -> OI -> ()
 
runDialogue :: Dialogue -> OI -> ()
 
runDialogue d =
 
runDialogue d =
\u -> let rspl = zipWith respond (d rspl) (parts u) in
+
\ u -> foldr seq () (yet (\ l -> zipWith respond (d l) (parts u)))
foldr (\ _ r -> r) () rspl
 
   
   
 
instance Partible a => MonadFix ((->) a) where
 
instance Partible a => MonadFix ((->) a) where
mfix m = \ u -> fix (\ x -> m x u) -- fix f = f (fix f)
+
mfix m = \ u -> yet (\ x -> m x u)
   
   
-- to be made into an ADT...
+
-- to be made into an abstract data type...
 
data Fresh a = Fresh (OI -> a) OI
 
data Fresh a = Fresh (OI -> a) OI
   
Line 58: Line 59:
   
 
instance Partible (Fresh a) where
 
instance Partible (Fresh a) where
part (Fresh g u) = case part u of (u1, u2) -> (Fresh g u1, Fresh g u2)
+
parts (Fresh g u) = [ Fresh g v | v <- parts u ]
   
 
fresh :: Fresh a -> [a]
 
fresh :: Fresh a -> [a]
fresh u = [ g v | Fresh g v <- parts u ]
+
fresh (Fresh g u) = [ g v | v <- parts u ]
   
 
instance Functor Fresh where
 
instance Functor Fresh where
Line 67: Line 68:
   
   
-- one more primitive
+
-- 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
part (u, v) = case (part u, part v) of
+
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
part (Left u) = case part u of (u1, u2) -> (Left u1, Left u2)
+
parts (Left u) = map Left (parts u)
part (Right v) = case part v of (v1, v2) -> (Right v1, Right v2)
+
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 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 M4 a = (Throw IOException, Some (Either Float OI)) -> a
 
-- ...whatever suits the purpose
 
-- ...whatever suits the purpose
   
Line 90: Line 103:
   
 
instance (Partible a, Partible b) => MonadCommute ((->) a) ((->) b) where
 
instance (Partible a, Partible b) => MonadCommute ((->) a) ((->) b) where
mcommute m = \ u2 u1 -> m u1 u2
+
mcommute m = \ v u -> m u v
 
</haskell>
 
</haskell>
  +
   
 
So what qualifies as being partible?
 
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.
+
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:
   
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:
 
 
<haskell>
 
<haskell>
let
+
\ u -> let
 
x = (primPutChar 'h' u `seq` primPutChar 'a' u)
 
x = (primPutChar 'h' u `seq` primPutChar 'a' u)
 
in x `seq` x
 
in x `seq` x
 
</haskell>
 
</haskell>
  +
  +
 
would trigger the error; the working version being:
 
would trigger the error; the working version being:
  +
 
<haskell>
 
<haskell>
 
let
 
let
 
x = (\ v -> case part v of
 
x = (\ v -> case part v of
 
(v1, v2) -> primPutChar 'h' v1 `seq` primPutChar 'a' v2)
 
(v1, v2) -> primPutChar 'h' v1 `seq` primPutChar 'a' v2)
in
+
in
case part u of
+
\ u -> case part u of
(u1, u2) -> x u1 `seq` x u2
+
(u1, u2) -> x u1 `seq` x u2
 
</haskell>
 
</haskell>
  +
  +
 
...rather tedious, if it weren't for Haskell's standard monadic methods:
 
...rather tedious, if it weren't for Haskell's standard monadic methods:
  +
 
<haskell>
 
<haskell>
 
let
 
let
Line 118: Line 137:
 
in x >> x
 
in x >> x
 
</haskell>
 
</haskell>
Higher-order 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.
 
   
  +
 
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:
 
Other references and articles:
   
* ''An alternative approach to I/O'', Maarten Fokkinga and Jan Kuper.
+
* [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/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.
  +
  +
* [http://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.
  +
  +
* [http://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.
   
* ''Functional Pearl: On generating unique names'', Lennart Augustsson, Mikael Rittri and Dan Synek.
 
  +
* <span style="color:#ba0000">Arborescent data structures and lazy evaluation: A new approach to numerical problems</span>, Manuel Carcenac.
   
* ''Can functional programming be liberated from the von Neumann paradigm?'', Conal Elliott.
 
  +
See also:
   
* ''Non-Imperative Functional Programming'', Nobuo Yamashita.
 
  +
* [[Sequential ordering of evaluation]]
   
* ''MTL style for free'', Tom Ellis.
 
  +
* [[Monomorphism by annotation of type variables]]
   
* ''Functional I/O Using System Tokens'', Lennart Augustsson.
 
  +
* [[Prelude extensions]]
   
   
 
Thank you to those who commented on early drafts of this document.
 
Thank you to those who commented on early drafts of this document.
   
[[User:Atravers|Atravers]] ([[User talk:Atravers|talk]]) 04:31, 10 April 2018 (UTC)
+
[[User:Atravers|Atravers]] 04:31, 10 April 2018 (UTC)

Latest revision as of 02:49, 18 May 2020

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.

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


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.

The patches for an initial implementation in GHC are available:

Other references and articles:

  • Functional Pearl: On generating unique names, Lennart Augustsson, Mikael Rittri and Dan Synek.
  • Non-Imperative Functional Programming, Nobuo Yamashita.
  • 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)