Difference between revisions of "Partible laws"

From HaskellWiki
Jump to: navigation, search
m (Bang-pattern syntax corrected)
m (Conditions for well-defined "Partible" instance clarified)
 
(3 intermediate revisions by the same user not shown)
Line 12: Line 12:
 
* <i>old</i>(<code>u :: T</code>) means <code>u</code> was previously used by a member of ''S''(<code>T</code>);
 
* <i>old</i>(<code>u :: T</code>) means <code>u</code> was previously used by a member of ''S''(<code>T</code>);
   
* Each member of ''S''(<code>T</code>) uses one or more <code>T</code>-values ''strictly and exclusively'':
+
* Each member of ''S''(<code>T</code>) uses one or more <code>T</code>-values ''strictly'' and ''exclusively'':
::if <code>x</code> ≡ ⊥ or ''old''(<code>x</code>) causes <code>f</code> <b>…</b> (<code>x :: !T</code>) <b>…</b> ≡ ⊥, then <code>f</code> ∈ ''S''(<code>T</code>);
+
::if <code>f</code> ''S''(<code>T</code>), then <code>f</code> <b>…</b> (<code>x :: !T</code>) <b>…</b> ≡ ⊥:
  +
::* if <code>x</code> ≡ ⊥
  +
::* or ''old''(<code>x</code>);
   
 
* The <code>Partible</code> instance for <code>T</code> is ''well-defined'':
 
* The <code>Partible</code> instance for <code>T</code> is ''well-defined'':
::if <i>new</i>(<code>u</code>) and <code>part</code> ∈ ''S''(<code>T</code>), then <code>part u</code> ≡ <code>(u1, u2)</code>, where <i>new</i>(<code>u1</code>) and <i>new</i>(<code>u2</code>); <code>u</code>, <code>u1</code> and <code>u2</code> are distinct and disjoint;
+
::if <i>new</i>(<code>u</code>) and <code>part</code> ∈ ''S''(<code>T</code>), then <code>part u</code> ≡ <code>(u1, u2)</code>, where:
  +
::* <i>new</i>(<code>u1</code>) and <i>new</i>(<code>u2</code>)
  +
::* <code>u</code>, <code>u1</code> and <code>u2</code> are distinct
  +
::* <code>u1</code> and <code>u2</code> are disjoint;
   
 
* <code>g</code> is a strict function: <code>g</code> ⊥ ≡ ⊥
 
* <code>g</code> is a strict function: <code>g</code> ⊥ ≡ ⊥
Line 31: Line 31:
 
| ≡
 
| ≡
 
| <code>g u2</code>,
 
| <code>g u2</code>,
| <code>u1</code><code>u2</code>, <i>new</i>(<code>u1</code>), <i>new</i>(<code>u2</code>)
+
| <i>new</i>(<code>u1</code>) and <i>new</i>(<code>u2</code>); <code>u1</code> and <code>u2</code> are distinct and disjoint;
 
|-
 
|-
 
| <i>Left-easing:</i>
 
| <i>Left-easing:</i>
Line 102: Line 102:
 
:* LSE = <code>(\(!_) -> r) (part u)</code>
 
:* LSE = <code>(\(!_) -> r) (part u)</code>
 
:* RSE = <code>(\(!_) -> r) u</code>
 
:* RSE = <code>(\(!_) -> r) u</code>
:* conditions: <code>r</code> doesn't require <code>part u</code>, <code>u</code> is obtained from <code>part u0</code>, <i>new</i>(<code>u0</code>)
+
:* conditions: <code>r</code> doesn't require <code>part u</code>, <i>new</i>(<code>u</code>)
 
<sub> </sub>
 
<sub> </sub>
 
:{|
 
:{|

Latest revision as of 05:50, 14 September 2021

Preliminaries

  • pq simply means that you can replace p with q and vice-versa, and the behaviour of your program will not change: p and q are equivalent;
  • T is a partible type, with an instance for Partible;
  • S(T) is the set of basic definitions for T-values (analogous to the set of primitive definitions for a builtin type);
  • new(u :: T) means u has never been used by any member of S(T);
  • old(u :: T) means u was previously used by a member of S(T);
  • Each member of S(T) uses one or more T-values strictly and exclusively:
if fS(T), then f (x :: !T) ≡ ⊥:
  • if x ≡ ⊥
  • or old(x);
  • The Partible instance for T is well-defined:
if new(u) and partS(T), then part u(u1, u2), where:
  • new(u1) and new(u2)
  • u, u1 and u2 are distinct
  • u1 and u2 are disjoint;
  • g is a strict function: g ⊥ ≡ ⊥
  • g's parameter is meant to be used strictly and exclusively by a member of S(T):
g x = (f (x :: !T) ) , where fS(T)
g u ≡ ⊥, old(u)

The laws

Substitutive: g u1 g u2, new(u1) and new(u2); u1 and u2 are distinct and disjoint;
Left-easing: g (fst (part u)) g u, new(u)
Right-easing: g (snd (part u)) g u, new(u)

Why the partible laws should be satisfied

  • In theory - they add to the set of valid transformations available for reasoning about the definitions of programs e.g. verifying Kleisli-composition:
Using:
(g >=> h) x  = \u -> case part u of
                       (u1, u2) -> case g x u1 of
                                     !y -> h y u2  

m >>= k      = \u -> case part u of
                       (u1, u2) -> case m u1 of
                                     !x -> k x u2
  • LSE = (g >=> h) x
  • RSE = g x >>= h

  g x >>= h
[RSE]
=
  \u -> case part u of
          (u1, u2) -> case g x u1 of 
                        !x -> h x u2
[application of (>>=)]
=
  \u -> case part u of
          (u1, u2) -> case g x u1 of 
                        !y -> h y u2
[bound variable renamed]
=
  (g >=> h) x
[definition of (>=>)]
= LSE
  • In practice - most optimising Haskell implementations use transformations like these to improve a program's performance, so a not-quite-partible type would lead to confusing runtime errors. But even if your Haskell implementation doesn't use them, you still want the laws for your own sake, just so you can avoid pulling your hair out over counter-intuitive program behaviour resulting from seemingly-innocuous changes such as rearranging calls to part or how values of some supposedly-partible type are used...

Examples

Proving the part-easing rule

  • LSE = (\(!_) -> r) (part u)
  • RSE = (\(!_) -> r) u
  • conditions: r doesn't require part u, new(u)

(\(!_) -> r) (part u)
[LSE]
=
(\(!_) -> r) (case part u of (u1, _) -> u1)
[scrutinee evaluated but not used in r]
=
(\(!_) -> r) (fst (part u))
[definition of fst]
=
(\(!_) -> r) u
[law: Left-easing]
= RSE

Proving the monad laws

...Kleisli-composition style:

Left identity:
return >=> h
h
Right identity:
f >=> return
f
Associativity:
(f >=> g) >=> h
f >=> (g >=> h)

Using:

return x     = \u -> case part u of !_ -> x

(g >=> h) x  = \u -> case part u of
                       (u1, u2) -> case g x u1 of
                                     !y -> h y u2

Left identity

  • LSE = (return >=> h) x
  • RSE = h x

  (return >=> h) x
[LSE]
=
  \u -> case part u of
          (u1, u2) -> case return x u1 of 
                        !y -> h y u2
[application of (>=>)]
=
  \u -> case part u of
          (u1, u2) -> case (case part u1 of !_ -> x) of 
                        !y -> h y u2
[application of return]
=
  \u -> case part u of
          (u1, u2) -> case (\t -> case t of !_ -> x) (part u1) of 
                        !y -> h y u2
[function abstraction]
=
  \u -> case part u of
          (u1, u2) -> case (\(!_) -> x) (part u1) of 
                        !y -> h y u2
[rule: trivial case]
=
  \u -> case part u of
          (u1, u2) -> case (\(!_) -> x) u1 of 
                        !y -> h y u2
[rule: part-easing]
=
  \u -> case part u of
          (u1, u2) -> case (\_ -> x) u1 of 
                        !y -> h y u2
[u1 not used anywhere else]
=
  \u -> case part u of
          (u1, u2) -> case x of
                        !y -> h y u2
[function application]
=
  \u -> case part u of
          (u1, u2) -> h x u2
[rule: trivial case; assuming x ≠ ⊥]
=
  \u -> case (\(u1, u2) -> u2) (part u) of 
          u2 -> h x u2
[definition of snd]
=
  \u -> case snd (part u) of 
          u2 -> h x u2
[definition of snd]
=
  \u -> case u of
          u2 -> h x u2
[law: Right-easing]
=
  \u -> h x u
[rule: trivial case]
=
  h x
[eta-substitution]
= RSE [assuming x ≠ ⊥]

Right identity

  • LSE = (f >=> return) x
  • RSE = f x

  (f >=> return) x
[LSE]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of
                        !y -> return y u2
[application of (>=>)]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of
                        !y -> case part u2 of !_ -> y
[application of return]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of
                        !y -> (\t -> case t of !_ -> y) (part u2)
[function abstraction]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of
                        !y -> (\(!_) -> y) (part u2)
[rule: trivial case]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of
                        !y -> (\(!_) -> y) u2
[rule: part-easing]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of
                        !y -> (\_ -> y) u2
[u2 not used anywhere else]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of 
                        !y -> y
[function application]
=
  \u -> case part u of
          (u1, u2) -> f x u1
[rule: trivial case; assuming f x … ≠ ⊥]
=
  \u -> case (\(u1, u2) -> u1) (part u) of 
          u1 -> f x u1
[function abstraction]
=
  \u -> case fst (part u) of 
          u1 -> f x u1
[definition of fst]
=
  \u -> case u of
          u1 -> f x u1
[law: Left-easing]
=
  \u -> f x u
[rule: trivial case]
=
  f x
[eta-substitution]
= RSE [assuming f x … ≠ ⊥]

Associativity

  • LSE = ((f >=> g) >=> h) x
  • RSE = (f >=> (g >=> h)) x

  ((f >=> g) >=> h) x
[LSE]
=
  \u -> case part u of
          (u1, u2) -> case (f >=> g) x u1 
                        of !y -> h y u2
[application of (>=>)]
=
  \u -> case part u of
          (u1, u2) -> case (case part u1 of
                              (u4, u5) -> case f x u4
                                            of !d -> g d u5) of 
                        !y -> h y u2
[application of (>=>)]
=
  \u -> case part u of
          (u1, u2) -> case part u1 of
                        (u4, u5) -> case (case f x u4 of
                                            !d -> g d u5) of 
                                      !y -> h y u2
[rule: case of case]
=
  \u -> case part u of
          (u1, u2) -> case part u1 of
                        (u4, u5) -> case f x u4 of
                                      !d -> case g d u5 of
                                              !y -> h y u2
[rule: case of case]
=
  \u -> case part u of
          (u1, u2) -> case part u2 of
                        (u4, u5) -> case f x u4 of
                                      !d -> case g d u5 of
                                              !y -> h y u1
[law: Substitutive]
=
  \u -> case part u of
          (u1, u2) -> case part u2 of
                        (u4, u5) -> case f x u1 of
                                      !d -> case g d u5
                                              of !y -> h y u4
[law: Substitutive]
=
  \u -> case part u of
          (u1, u2) -> case part u2 of
                        (u4, u5) -> case f x u1 of
                                      !d -> case g d u4 of
                                              !y -> h y u5
[law: Substitutive]
=
  \u -> case part u of
          (u1, u2) -> case part u2 of
                        (u4, u5) -> (\t -> case t of
                                             !d -> case g d u4 of
                                                     !y -> h y u5) 
                                      (f x u1)
[function abstraction]
=
  \u -> case part u of
          (u1, u2) -> (\t -> case t of
                               !d -> case part u2 of
                                       (u4, u5) -> case g d u4 of
                                                     !y -> h y u5) 
                        (f x u1)
[rule: function-case]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of
                        !d -> case part u2 of
                                (u4, u5) -> case g d u4 of
                                              !y -> h y u5
[function application]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of
                        !d -> (\b c u3 -> case part u3 of
                                            (u4, u5) -> case b d u4 of
                                                          !y -> c y u5) 
                                g h u2
[function abstraction]
=
  \u -> case part u of
          (u1, u2) -> case f x u1 of
                        !d -> (g >=> h) d u2
[definition of (>=>)]
=
  (f >=> (g >=> h)) x
[definition of (>=>)]
= RSE

(Note: those residual assumptions from the proofs for the identity laws are to be expected considering how return and (>=>) are defined - for more details, see section 3.4 of Philip Wadler's How to Declare an Imperative.)

References