Difference between revisions of "Plainly partible"
(Initial contents, with crosssover from elsewhere) 
(Reference to "Partible laws" added) 

Line 88:  Line 88:  
(Of course if it's more efficient to do so, <code>part</code> and <code>parts</code> can both be defined.) 
(Of course if it's more efficient to do so, <code>part</code> and <code>parts</code> can both be defined.) 

+  
+  Ideally, each partible type in Haskell should also satisfy the [[Partible lawspartible laws]]. 

== Examples == 
== Examples == 
Revision as of 07:57, 8 April 2021
Contents
What is partible?
Partible types are specific forms of pseudodata (a generalisation of oracles) 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.
Why splittable isn't always enough
Further developments
Since its advent, pseudodata (or aspects thereof) have appeared, or can be recognised in other contexts:
 In Simon Peyton Jones's 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 tvname) for a type checker, using the type name_supply:
  page 188 of 458
 next_name :: name_supply > tvname
 deplete :: name_supply > name_supply
 split :: name_supply > (name_supply, name_supply)
 The crucial point here is the absence of trees  they have been reduced to an implementation detail, oblivious to the users of name_supply values.
 In 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 On generating unique names with their concept implementation for a singleuse variant of Hancock's uniquename supply  each one can only be used once, if at all:
 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
 In contrast to the example by John Launchbury and Simon Peyton Jones in State in Haskell (see pages 3940 of 51), this monousal strategy completely obviates the need for trees (or other intermediary structured values such as streams).
 Nobuo Yamashita uses a singleuse type similar to pseudodata in his
IO
alternative oi package: see the 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 uniquename 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 Partible
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:
 part_uniquesupply :: uniquesupply > (uniquesupply, uniquesupply)
  or 
 parts_uniquesupply :: uniquesupply > [uniquesupply]
As each definition can be defined with 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
 Yamashita's singleuse type can be made partible:
data OI = OI OI# instance Partible OI where part = partOI partOI :: OI > (OI, OI) partOI (OI h) = case part# h of (# h1, h2 #) > (OI h1, OI h2) runOI :: (OI > a) > IO a runOI g = IO $ \s > case dispense# s of (# s', h #) > seq# (g (OI h)) s' invokes :: Monomo a => String > IO a > OI > a (name `invokes` IO act) (OI h) = (name `invokes#` act) h class Monomo a  local definitions   type OI# = String > State# RealWorld part# :: OI# > (# OI#, OI# #) part# h = case h "partOI" of s > case dispense# s of (# s', h1 #) > case dispense# s' of (# _, h2 #) > (# h1, h2 #) dispense# :: IO# OI# dispense# s = case newMutVar# () s of (# s', r #) > (# s', expire# s' r #) expire# :: State# s > MutVar# s () > String > State# s expire# s r name = case atomicModifyMutVar# r use s of (# s', () #) > s' where use x = (error nowUsed, x) nowUsed = name' ++ ": already expired" name' = if all isSpace name then "(unknown)" else name invokes# :: Monomo a => String > IO# a > OI# > a (name `invokes#` act) h = case act (noDuplicate# (h name)) of (# _, t #) > t type IO# a = State# RealWorld > (# State# RealWorld, a #)
 Some notes:
 the elementary reuseerror reporting is optional;
 the use of the
Monomo
ininvokes
leverage Haskell's type system to provide an extra measure of safety, by restricting any typepolymorphism in the result: for more information, look into the history of Standard ML.
 Using the reformulated
OI
type, an uniquename supply is easily defined:
data Fresh a = Fresh (OI > a) OI instance Partible (Fresh a) where parts (Fresh g u) = [ Fresh g v  v < parts u ] afresh :: (OI > a) > OI > 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
 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 nonvoid 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)