Plainly partible: Difference between revisions

From HaskellWiki
(Reference to "Partible laws" added)
mNo edit summary
 
(14 intermediate revisions by the same user not shown)
Line 1: Line 1:
== What is partible? ==
== What is partible? ==


''Partible types'' are specific forms of ''pseudodata'' (a generalisation of [[Opting for oracles|oracles]]) whose values satisfy the following properties:
''Partible types'' are specific forms of [[Pseudo-data|pseudo-data]] whose values satisfy the following properties:


* they are all ''unique'': no two values will ever be the same;
* they are all [[Uniqueness annotations for types|''unique'']]: no two values will ever be the same;


* they are ''monousal'': if it is used, each value can only be used once;
* they are ''monousal'': if it is used, each value can only be used once;
Line 9: Line 9:
* their splitting is ''disjoint'': the resulting new values are independent.
* their splitting is ''disjoint'': the resulting new values are independent.


== Why ''splittable'' isn't always enough ==
== A matter of nomenclature: why <i>splittable</i> isn't always enough ==


=== Further developments ===
In [https://www.iro.umontreal.ca/~lecuyer/myftp/papers/cacm88.pdf Efficient and Portable Combined Random Number Generators], Pierre L'Ecuyer suggests the ''disjoint'' splitting of random numbers into independent subsequences. But for entities like unique-name supplies, disjoint splitting is an ''absolute necessity!'' To avoid having to repeatedly specify it, an alternate terminology is needed - one which clearly indicates that for some pseudo-data types, the "disjointedness" of splitting is '''mandatory''', instead of just being very convenient.
 
Since its advent, ''pseudodata'' (or aspects thereof) have appeared, or can be recognised in other contexts:
 
* In Simon Peyton Jones's [[Books|The implementation of functional programming languages]] (section 9.6 on page 188 of 458), Peter Hancock provides a simpler interface for generating new type variables (of type <tt>tvname</tt>) for a type checker, using the type <tt>name_supply</tt>:
 
<tt>
::|| page 188 of 458
::next_name :: name_supply -> tvname
::deplete :: name_supply -> name_supply
::split :: name_supply -> (name_supply, name_supply)
</tt>
 
:The crucial point here is the absence of trees - they have been reduced to an implementation detail, oblivious to the users of <tt>name_supply</tt> values.
 
* In [https://www.iro.umontreal.ca/~lecuyer/myftp/papers/cacm88.pdf Efficient and Portable Combined Random Number Generators], Pierre L'Ecuyer suggests the ''disjoint'' splitting of random numbers into independent subsequences as needed.
 
* As previously specified, if ''pseudodata'' is used then it remains constant - reusing it doesn't change its value. Lennart Augustsson, Mikael Rittri and Dan Synek take this to an extreme in their functional pearl [[Research papers/Functional pearls|On generating unique names]] with their concept implementation for a ''single-use'' variant of Hancock's unique-name supply - each one can only be used once, if at all:
 
<tt>
::abstype uniquesupply
::with
:::new_uniquesupply  :: uniquesupply
:::split_uniquesupply :: uniquesupply -> (uniquesupply, uniquesupply)
:::get_unique        :: uniquesupply -> unique
 
::uniquesupply ::= US
 
::new_uniquesupply = US
::split_uniquesupply US = (US, US)
::get_unique s = gensym(s)
 
::unique == int
 
::|| Not a regular definition!
::gensym :: * -> unique
</tt>
 
:In contrast to the example by John Launchbury and Simon Peyton Jones in [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.52.3656&rep=rep1&type=pdf State in Haskell] (see pages 39-40 of 51), this ''monousal'' strategy completely obviates the need for trees (or other intermediary structured values such as streams).
 
* Nobuo Yamashita uses a single-use type similar to ''pseudodata'' in his <code>IO</code>-alternative [https://hackage.haskell.org/package/oi ''oi''] package: see the [https://hackage.haskell.org/package/oi-0.4.0.2/docs/src/Data-OI-Internal.html#OI Data.OI.Internal] module for the details.
 
=== A matter of nomenclature ===
 
As mentioned earlier, L'Ecuyer suggests the splitting of random numbers be disjoint. But for entities like unique-name supplies, disjoint splitting is an ''absolute necessity!'' To avoid having to repeatedly specify it, an alternate terminology is needed - one which clearly indicates that for some types of pseudodata, the ''disjointedness'' of its splitting is '''mandatory''', instead of just being very convenient.


== The <code>Partible</code> class ==
== The <code>Partible</code> class ==


Depending on how its corresponding partible type is defined, the disjoint splitting of an unused value can either be a pair or list of new values:
Depending on how it's corresponding partible type is defined, the disjoint splitting of an unused value can either be a pair or list of new values:


<tt>
<tt>
Line 67: Line 23:
</tt>
</tt>


As each definition can be defined with the other:
As each method can be defined using the other:


<tt>
<tt>
Line 93: Line 49:
== Examples ==
== Examples ==


* Yamashita's single-use type can be made partible:
* Using [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.52.3656&rep=rep1&type=pdf State in Haskell] as a guide, an ''encapsulated single-use'' type can be defined as follows:


:<haskell>
:<haskell>
data OI                = OI OI#
{-# LANGUAGE BangPatterns, RankNTypes, UnboxedTuples, MagicHash #-}
module UseOnce(UO, Monomo, part, runUO, useUO, asUO) where
import Prelude(String, Eq(..))
import Prelude((.), ($), (++), error, all)
import Data.Char(isSpace)
import Partible
import Monomo
import GHC.Base(State#, MutVar#)
import GHC.Base(runRW#, newMutVar#, noDuplicate#)
import GHC.Exts(atomicModifyMutVar#)
import GHC.ST(ST(..), STRep)


instance Partible OI where
data UO s              = UO (UO# s)
    part = partOI


partOI                  :: OI -> (OI, OI)
instance Partible (UO s) where
partOI (OI h)          = case part# h of (# h1, h2 #) -> (OI h1, OI h2)
    part = partUO


runOI                  :: (OI -> a) -> IO a
partUO                  :: UO s -> (UO s, UO s)
runOI g                = IO $ \s -> case dispense# s of
partUO (UO h)          = let !(# h1, h2 #) = partUO# h in (UO h1, UO h2)
                                      (# s', h #) -> seq# (g (OI h)) s'


invokes                :: Monomo a => String -> IO a -> OI -> a
runUO                  :: (forall s . UO s -> a) -> a
(name `invokes` IO act) (OI h)
runUO g                =  let !(# _, r #) = runRW# (useUO# (g . UO)) in r
                        = (name `invokes#` act) h


class Monomo a
useUO                  :: (UO s -> a) -> ST s a
useUO g                =  ST (\s -> useUO# (g . UO) s)
 
asUO                    :: Monomo a => String -> ST s a -> UO s -> a
asUO name (ST act) (UO h)
                        =  asUO# name act h


  -- local definitions --
  -- local definitions --
  --
  --
type OI#               = String -> State# RealWorld
type UO# s              = String -> State# s


part#                   :: OI# -> (# OI#, OI# #)
partUO#                 :: UO# s -> (# UO# s, UO# s #)
part# h                 = case h "partOI" of
partUO# h               =  let !s            = h "partUO"
                            s -> case dispense# s of
                              !(# s', h1 #) = dispense# s
                                  (# s', h1 #) ->
                              !(# _, h2 #) = dispense# s'
                                    case dispense# s' of
                          in  (# h1, h2 #)
                                      (# _, h2 #) -> (# h1, h2 #)


dispense#               :: IO# OI#
useUO#                 :: (UO# s -> a) -> STRep s a
dispense# s             = case newMutVar# () s of
useUO# g s              =  let !(# s', h #) = dispense# s
                            (# s', r #) -> (# s', expire# s' r #)
                              !r          = g h
                          in  (# s', r #)
 
dispense#               :: STRep s (UO# s)
dispense# s             =  let !(# s', r #) = newMutVar# () s
                          in  (# s', expire# s' r #)


expire#                :: State# s -> MutVar# s () -> String -> State# s
expire#                :: State# s -> MutVar# s () -> String -> State# s
expire# s r name        = case atomicModifyMutVar# r use s of
expire# s r name        = let !(# s', () #) = atomicModifyMutVar# r use s
                            (# s', () #) -> s'
                          in  s'
                          where
                          where
                              use x  =  (error nowUsed, x)
                              use x  =  (error nowUsed, x)
                              nowUsed =  name' ++ ": already expired"
                              nowUsed =  name' ++ ": already expired"
                              name'  =  if all isSpace name then "(unknown)"
                              name'  =  if all isSpace name then "(unknown)"
                                           else name
                                           else name


invokes#               :: Monomo a => String -> IO# a -> OI# -> a
asUO#                   :: Monomo a => String -> STRep s a -> UO# s -> a
(name `invokes#` act) h = case act (noDuplicate# (h name)) of (# _, t #) -> t
asUO# name act h       = let !(# _, t #) = act (noDuplicate# (h name)) in t
 
type IO# a              = State# RealWorld -> (# State# RealWorld, a #)
</haskell>
</haskell>


:Some notes:
:Some notes:
:* the ''elementary'' reuse-error reporting is optional;
:* the ''elementary'' reuse-error reporting is optional;
:* the use of the <code>Monomo</code> in <code>invokes</code> leverage Haskell's type system to provide an extra measure of safety, by restricting any type-polymorphism in the result: for more information, look into the history of Standard ML.  
:* the [[Monomorphism by annotation of type variables|use of]] <code>Monomo</code> in <code>asUO</code> leverage Haskell's type system to provide an extra measure of safety, by restricting any type-polymorphism in the result: for more information, look into the history of Standard ML.  
 
* Using the parametric <code>UO</code> type, an [https://lukepalmer.wordpress.com/2009/09/14/io-free-splittable-supply encapsulated unique-name supply] can be defined:


* Using the reformulated <code>OI</code> type, an unique-name supply is easily defined:
:<haskell>
:<haskell>
data Fresh a = Fresh (OI -> a) OI
data Fresh a = forall s . Fresh (UO s -> a) (UO s)


instance Partible (Fresh a) where
instance Partible (Fresh a) where
     parts (Fresh g u) = [ Fresh g v | v <- parts u ]
     parts (Fresh g u) = [ Fresh g v | v <- parts u ]


afresh :: (OI -> a) -> OI -> Fresh a
afresh :: (UO s -> a) -> UO s -> Fresh a
afresh g u = Fresh g u
afresh g u = Fresh g u


Line 163: Line 134:
instance Functor Fresh where
instance Functor Fresh where
     fmap f (Fresh g u) = Fresh (f . g) u
     fmap f (Fresh g u) = Fresh (f . g) u
runFresh :: (forall a. Eq a => Fresh a -> b) -> b
runFresh f =  f (runUO (freshNew (\n -> n)))
freshNew :: (Int -> a) -> UO s -> Fresh a
freshNew conv u = let !(u1, u2) = partUO u
                      uvar      = asUO "uvar" (newSTRef 0) u1
                      incr n    = (n + 1, n)
                      gensym    = asUO "gensym" (atomicModifySTRef uvar incr)
                  in  Fresh (conv . gensym) u2
-- NB: may also need to define atomicModifySTRef; check your Haskell implementation
</haskell>
* Another possible abstract partible type is the generic ''exception-thrower'':
:<haskell>
data Throw e
instance Partible (Throw e) where
    part = partThrow
partThrow :: Throw e -> (Throw e, 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
</haskell>
</haskell>


Line 203: Line 199:
Therefore, because of their void values:
Therefore, because of their void values:


* <haskell>[] :: [a]</haskell>
* <code>[] :: [a]</code>


* <haskell>Nothing :: Maybe a</haskell>
* <code>Nothing :: Maybe a</code>


instances for for the list or <code>Maybe</code> types are at best dubious:
instances for for the list or <code>Maybe</code> types are at best dubious:


instance Partible a => Partible [a] where
:{|
    part [] = ([], [])  -- !?
|<pre>
             .
instance Partible a => Partible [a] where
            .
  part [] = ([], [])  -- !?
            .
            
 
</pre>
instance Partible a => Partible (Maybe a) where
|-
    part Nothing = (Nothing, Nothing)  -- ?!
|<pre>
             .
instance Partible a => Partible (Maybe a) where
            .
  part Nothing = (Nothing, Nothing)  -- ?!
            .
            
</pre>
|}


An alternative is to repurpose their non-void values to form a new type e.g:
An alternative is to repurpose their non-void values to form a new type e.g:


<haskell>
:<haskell>
data Some a = Only a | More a (Some a)
data Some a = Only a | More a (Some a)


Line 230: Line 228:
     parts (More u us) = zipWith More (parts u) (parts us)
     parts (More u us) = zipWith More (parts u) (parts us)
</haskell>
</haskell>


[[Category:Code]]
[[Category:Code]]

Latest revision as of 00:40, 8 March 2025

What is partible?

Partible types are specific forms of pseudo-data whose values satisfy the following properties:

  • they are all unique: no two values will ever be the same;
  • they are monousal: if it is used, each value can only be used once;
  • their splitting is disjoint: the resulting new values are independent.

A matter of nomenclature: why splittable isn't always enough

In Efficient and Portable Combined Random Number Generators, Pierre L'Ecuyer suggests the disjoint splitting of random numbers into independent subsequences. But for entities like unique-name supplies, disjoint splitting is an absolute necessity! To avoid having to repeatedly specify it, an alternate terminology is needed - one which clearly indicates that for some pseudo-data types, the "disjointedness" of splitting is mandatory, instead of just being very convenient.

The Partible class

Depending on how it's corresponding partible type is defined, the disjoint splitting of an unused value can either be a pair or list of new values:

part_uniquesupply  :: uniquesupply -> (uniquesupply, uniquesupply)
|| or ||
parts_uniquesupply :: uniquesupply -> [uniquesupply]

As each method can be defined using the other:

part_uniquesupply u = (u1, u2) where u1:u2:_ = parts_uniquesupply u
|| or ||
parts_uniquesupply u = u1 : parts_uniquesupply u2 where (u1, u2) = part_uniquesupply u

they can both be overloaded in Haskell using default 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

(Of course if it's more efficient to do so, part and parts can both be defined.)

Ideally, each partible type in Haskell should also satisfy the partible laws.

Examples

  • Using State in Haskell as a guide, an encapsulated single-use type can be defined as follows:
{-# LANGUAGE BangPatterns, RankNTypes, UnboxedTuples, MagicHash #-}
module UseOnce(UO, Monomo, part, runUO, useUO, asUO) where
import Prelude(String, Eq(..))
import Prelude((.), ($), (++), error, all)
import Data.Char(isSpace)
import Partible
import Monomo
import GHC.Base(State#, MutVar#)
import GHC.Base(runRW#, newMutVar#, noDuplicate#)
import GHC.Exts(atomicModifyMutVar#)
import GHC.ST(ST(..), STRep)

data UO s               =  UO (UO# s)

instance Partible (UO s) where
    part = partUO

partUO                  :: UO s -> (UO s, UO s)
partUO (UO h)           =  let !(# h1, h2 #) = partUO# h in (UO h1, UO h2)

runUO                   :: (forall s . UO s -> a) -> a
runUO g                 =  let !(# _, r #) = runRW# (useUO# (g . UO)) in r

useUO                   :: (UO s -> a) -> ST s a
useUO g                 =  ST (\s -> useUO# (g . UO) s)

asUO                    :: Monomo a => String -> ST s a -> UO s -> a
asUO name (ST act) (UO h)
                        =  asUO# name act h

 -- local definitions --
 --
type UO# s              =  String -> State# s

partUO#                 :: UO# s -> (# UO# s, UO# s #)
partUO# h               =  let !s            = h "partUO"
                               !(# s', h1 #) = dispense# s
                               !(# _,  h2 #) = dispense# s'
                           in  (# h1, h2 #)

useUO#                  :: (UO# s -> a) -> STRep s a
useUO# g s              =  let !(# s', h #) = dispense# s
                               !r           = g h
                           in  (# s', r #)

dispense#               :: STRep s (UO# s)
dispense# s             =  let !(# s', r #) = newMutVar# () s
                           in  (# s', expire# s' r #)

expire#                 :: State# s -> MutVar# s () -> String -> State# s
expire# s r name        =  let !(# s', () #) = atomicModifyMutVar# r use s
                           in  s'
                           where
                               use x   =  (error nowUsed, x)
                               nowUsed =  name' ++ ": already expired"
                               name'   =  if all isSpace name then "(unknown)"
                                          else name

asUO#                   :: Monomo a => String -> STRep s a -> UO# s -> a
asUO# name act h        =  let !(# _, t #) = act (noDuplicate# (h name)) in t
Some notes:
  • the elementary reuse-error reporting is optional;
  • the use of Monomo in asUO leverage Haskell's type system to provide an extra measure of safety, by restricting any type-polymorphism in the result: for more information, look into the history of Standard ML.
data Fresh a = forall s . Fresh (UO s -> a) (UO s)

instance Partible (Fresh a) where
    parts (Fresh g u) = [ Fresh g v | v <- parts u ]

afresh :: (UO s -> a) -> UO s -> Fresh a
afresh g u = Fresh g 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

runFresh :: (forall a. Eq a => Fresh a -> b) -> b
runFresh f =  f (runUO (freshNew (\n -> n)))

freshNew :: (Int -> a) -> UO s -> Fresh a
freshNew conv u = let !(u1, u2) = partUO u
                      uvar      = asUO "uvar" (newSTRef 0) u1
                      incr n    = (n + 1, n)
                      gensym    = asUO "gensym" (atomicModifySTRef uvar incr)
                  in  Fresh (conv . gensym) u2

 -- NB: may also need to define atomicModifySTRef; check your Haskell implementation
  • Another possible abstract partible type is the generic exception-thrower:
data Throw e

instance Partible (Throw e) where
    part = partThrow

partThrow :: Throw e -> (Throw e, 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
  • Instances for various standard Haskell types are also a simple matter:
instance (Ix a, Partible b) => Partible (Array a b) where
    part arr = case unzip (map part' (assocs arr)) of
                 (al1, al2) -> (new al1, new al2)
               where
                   new          = array (bounds arr)
                   part' (i, u) = case part u of
                                    (u1, u2) -> ((i, u1), (i, u2))

instance (Partible a, Partible b) => Partible (Either a b) where
    parts (Left u)  = map Left (parts u)
    parts (Right v) = map Right (parts v)

instance (Partible a, Partible b) => Partible (a, b) where
    parts (u, v) = zip (parts u) (parts v)

instance (Partible a, Partible b, Partible c) => Partible (a, b, c) where
    parts (u, v, w) = zip3 (parts u) (parts v) (parts w)

instance (Partible a, Partible b, Partible c, Partible d) => Partible (a, b, c, d) where
    parts (u, v, w, x) = zip4 (parts u) (parts v) (parts w) (parts x)

instance (Partible a, Partible b, Partible c, Partible d, Partible e) => Partible (a, b, c, d, e) where
    parts (u, v, w, x, y) = zip5 (parts u) (parts v) (parts w) (parts x) (parts y)

 -- etc.

No list or Maybe instances

The unit type () is clearly not partible, because of its single value:

-- instance Partible () where part () = ((), ())  {- WRONG! -}

Therefore, because of their void values:

  • [] :: [a]
  • Nothing :: Maybe a

instances for for the list or Maybe types are at best dubious:

instance Partible a => Partible [a] where
   part [] = ([], [])  -- !?
             ⋮
instance Partible a => Partible (Maybe a) where
   part Nothing = (Nothing, Nothing)  -- ?!
             ⋮

An alternative is to repurpose their non-void values to form a new type e.g:

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)