Difference between revisions of "Partible laws"
From HaskellWiki
m (Conditions for rule "parteasing" clarified) 
m (Conditions for welldefined "Partible" instance clarified) 

Line 18:  Line 18:  
* The <code>Partible</code> instance for <code>T</code> is ''welldefined'': 
* The <code>Partible</code> instance for <code>T</code> is ''welldefined'': 

−  ::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 
+  ::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> ⊥ ≡ ⊥ 
Latest revision as of 05:50, 14 September 2021
Contents
Preliminaries
 p ≡ q simply means that you can replace p with q and viceversa, and the behaviour of your program will not change: p and q are equivalent;

T
is a partible type, with an instance forPartible
;
 S(
T
) is the set of basic definitions forT
values (analogous to the set of primitive definitions for a builtin type);
 new(
u :: T
) meansu
has never been used by any member of S(T
);
 old(
u :: T
) meansu
was previously used by a member of S(T
);
 Each member of S(
T
) uses one or moreT
values strictly and exclusively:
 if
f
∈ S(T
), thenf
… (x :: !T
) … ≡ ⊥: if
x
≡ ⊥  or old(
x
);
 if
 if
 The
Partible
instance forT
is welldefined:
 if new(
u
) andpart
∈ S(T
), thenpart u
≡(u1, u2)
, where: new(
u1
) and new(u2
) 
u
,u1
andu2
are distinct 
u1
andu2
are disjoint;
 new(
 if new(

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
) …) …, wheref
∈ S(T
)g u
≡ ⊥, old(u
)
The laws
Substitutive:  g u1

≡  g u2 ,

new(u1 ) and new(u2 ); u1 and u2 are distinct and disjoint;

Lefteasing:  g (fst (part u))

≡  g u ,

new(u )

Righteasing:  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 Kleislicomposition:
 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
 LSE =
_{ }
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 notquitepartible 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 counterintuitive program behaviour resulting from seeminglyinnocuous changes such as rearranging calls to
part
or how values of some supposedlypartible type are used...
Examples
Proving the parteasing rule
 LSE =
(\(!_) > r) (part u)
 RSE =
(\(!_) > r) u
 conditions:
r
doesn't requirepart u
, new(u
)
 LSE =
_{ }
(\(!_) > 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: Lefteasing] = RSE
Proving the monad laws
...Kleislicomposition 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: parteasing] 
=  \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: Righteasing] 
=  \u > h x u

[rule: trivial case] 
=  h x

[etasubstitution] 
=  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: parteasing] 
=  \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: Lefteasing] 
=  \u > f x u

[rule: trivial case] 
=  f x

[etasubstitution] 
=  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: functioncase] 
=  \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
 Functional programming, program transformations and compiler construction; Alexander Augusteijn.
 The GRIN Project: A Highly Optimising Back End for Lazy Functional languages; Urban Boquist and Thomas Johnsson.
 Transformation and Analysis of Functional Programs; Neil Mitchell.