# Difference between revisions of "Plainly partible"

m |
m (Content updated using Augustsson-Rittri-Synek paper) |
||

Line 27: | Line 27: | ||

* 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. |
* 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 [ |
+ | * 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 [https://www.cambridge.org/core/services/aop-cambridge-core/content/view/763DE73EB4761FDF681A613BE0E98443/S0956796800000988a.pdf/functional_pearl_on_generating_unique_names.pdf On generating unique names] with their concept implementation for a ''single-use'' variant of Hancock's unique-name supply, where each one can only be used once, if at all - from page 4 of 7: |

+ | :<haskell> |
||

− | <tt> |
||

+ | module OneTimeSupplies( |
||

− | ::abstype uniquesupply |
||

+ | Name, NameSupply, initialNameSupply, getNameDeplete, splitNameSupply) |
||

− | ::with |
||

+ | where |
||

− | :::new_uniquesupply :: uniquesupply |
||

+ | gensym :: a —> Int —— implemented in assembler |
||

− | :::split_uniquesupply :: uniquesupply -> (uniquesupply, uniquesupply) |
||

+ | data Name = MkName Int deriving (Eq) |
||

− | :::get_unique :: uniquesupply -> unique |
||

+ | data NameSupply = MkNameSupply |
||

+ | initialNameSupply = MkNameSupply |
||

+ | getNameDeplete s = (MkName(gensym(s)), MkNameSupply) |
||

+ | splitNameSupply MkNameSupply = (MkNameSupply, MkNameSupply) |
||

+ | </haskell> |
||

⚫ | |||

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

* Nobuo Yamashita uses a type reminiscent of ''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. |
* Nobuo Yamashita uses a type reminiscent of ''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. |

## Revision as of 07:47, 8 February 2022

## What is partible?

*Partible types* are specific forms of *pseudodata* (a generalisation of oracle streams) 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`:

`
`

- 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*single-use*variant of Hancock's unique-name supply, where each one can only be used once, if at all - from page 4 of 7:

module OneTimeSupplies( Name, NameSupply, initialNameSupply, getNameDeplete, splitNameSupply) where gensym :: a —> Int —— implemented in assembler data Name = MkName Int deriving (Eq) data NameSupply = MkNameSupply initialNameSupply = MkNameSupply getNameDeplete s = (MkName(gensym(s)), MkNameSupply) splitNameSupply MkNameSupply = (MkNameSupply, MkNameSupply)

- In contrast to the
`HideGensym`

implementation found on the same page, this*monousal*strategy completely obviates the need for trees (or other intermediary structured values such as streams).

- Nobuo Yamashita uses a type reminiscent of
*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 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 *pseudodata* 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.

- the

- Defining a partible variant of Yamashita's single-use type then only requires a suitable argument:

{-# LANGUAGE CPP, UnboxedTuples, MagicHash #-} #define FauxWorld RealWorld module OutputInput(OI, Monomo, part, runOI, invokes) where import UseOnce import GHC.Base(IO(..), FauxWorld) import GHC.ST(ST(..)) type OI = UO FauxWorld runOI :: (OI -> a) -> IO a runOI g = case (useUO g) of ST m -> IO m invokes :: Monomo a => String -> IO a -> OI -> a (name `invokes` IO act) u = asUO name (ST act) u

- Using the parametric
`UO`

type, an encapuslated unique-name supply can also be defined:

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)