Abstract Refinements {#composition} =================================== Very General Mechanism ---------------------- **Next:** Lets add parameters... <div class="hidden"> <pre><span class=hs-linenum>11: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>Composition</span> <span class='hs-keyword'>where</span> <span class=hs-linenum>12: </span> <span class=hs-linenum>13: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Prelude</span> <span class='hs-varid'>hiding</span> <span class='hs-layout'>(</span><span class='hs-layout'>(</span><span class='hs-varop'>.</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <span class=hs-linenum>14: </span> <span class=hs-linenum>15: </span><span class='hs-definition'>plus</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class=hs-linenum>16: </span><span class='hs-definition'>plus3'</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> </pre> </div> Example: `plus` --------------- <pre><span class=hs-linenum>25: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>plus</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>y</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-keyword'>_</span> <span class='hs-keyword'>| v=x+y}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>26: </span><a class=annot href="#"><span class=annottext>x:(Int) -> y:(Int) -> {v : (Int) | (v == (x + y))}</span><span class='hs-definition'>plus</span></a> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>y</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == x)}</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}</span><span class='hs-varop'>+</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == y)}</span><span class='hs-varid'>y</span></a> </pre> Example: `plus 3` ----------------- <br> <pre><span class=hs-linenum>36: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>plus3'</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span> <span class='hs-keyword'>| v = x + 3}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>37: </span><a class=annot href="#"><span class=annottext>x:(Int) -> {VV : (Int) | (VV == (x + 3))}</span><span class='hs-definition'>plus3'</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x2 : (Int) | (x2 == (x1 + x2))}</span><span class='hs-varid'>plus</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (3 : int))}</span><span class='hs-num'>3</span></a> </pre> <br> Easily verified by LiquidHaskell A Composed Variant ------------------ Lets define `plus3` by *composition* A Composition Operator ---------------------- <pre><span class=hs-linenum>53: </span><span class='hs-layout'>(</span><span class='hs-cpp'>#</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>c</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>c</span> <span class=hs-linenum>54: </span><a class=annot href="#"><span class=annottext>forall a b c. (a -> b) -> (c -> a) -> c -> b</span><span class='hs-layout'>(</span></a><span class='hs-cpp'>#</span><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>a -> b</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>a -> b</span><span class='hs-varid'>g</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>x</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>a -> b</span><span class='hs-varid'>f</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>a -> b</span><span class='hs-varid'>g</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a><span class='hs-layout'>)</span> </pre> `plus3` By Composition ----------------------- <pre><span class=hs-linenum>62: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>plus3''</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span> <span class='hs-keyword'>| v = x + 3}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>63: </span><a class=annot href="#"><span class=annottext>x:(Int) -> {VV : (Int) | (VV == (x + 3))}</span><span class='hs-definition'>plus3''</span></a> <span class='hs-keyglyph'>=</span> <span class=hs-error><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x2 : (Int) | (x2 == (x1 + x2))}</span><span class='hs-varid'>plus</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>((Int) -> (Int)) -> ((Int) -> (Int)) -> (Int) -> (Int)</span><span class='hs-cpp'>#</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x2 : (Int) | (x2 == (x1 + x2))}</span><span class='hs-varid'>plus</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (2 : int))}</span><span class='hs-num'>2</span></a></span> </pre> <br> Yikes! Verification *fails*. But why? <br> <div class="fragment">(Hover mouse over `#` for a clue)</div> How to type compose (#) ? ------------------------- This specification is *too weak* <br> <br> <pre><span class=hs-linenum>80: </span><span class='hs-layout'>(</span><span class='hs-cpp'>#</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>c</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>c</span><span class='hs-layout'>)</span> </pre> <br> Output type does not *relate* `c` with `a`! How to type compose (.) ? ------------------------- Write specification with abstract refinement type: <br> <pre><span class=hs-linenum>95: </span><span class='hs-keyword'>{-@</span> <span class='hs-layout'>(</span><span class='hs-varop'>.</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyword'>forall</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>b</span><span class='hs-keyglyph'>-></span><span class='hs-varid'>c</span><span class='hs-keyglyph'>-></span><span class='hs-conid'>Prop</span><span class='hs-layout'>,</span> <span class=hs-linenum>96: </span> <span class='hs-varid'>q</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-keyglyph'>-></span><span class='hs-varid'>b</span><span class='hs-keyglyph'>-></span><span class='hs-conid'>Prop</span><span class='hs-varop'>>.</span> <span class=hs-linenum>97: </span> <span class='hs-varid'>f</span><span class='hs-conop'>:</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>c</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>x</span><span class='hs-varop'>></span><span class='hs-layout'>)</span> <span class=hs-linenum>98: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>g</span><span class='hs-conop'>:</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>q</span> <span class='hs-varid'>x</span><span class='hs-varop'>></span><span class='hs-layout'>)</span> <span class=hs-linenum>99: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>y</span><span class='hs-conop'>:</span><span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>exists</span><span class='hs-keyglyph'>[</span><span class='hs-varid'>z</span><span class='hs-conop'>:</span><span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>q</span> <span class='hs-varid'>y</span><span class='hs-varop'>></span><span class='hs-keyglyph'>]</span><span class='hs-varop'>.</span><span class='hs-varid'>c</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>z</span><span class='hs-varop'>></span> <span class=hs-linenum>100: </span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>101: </span><a class=annot href="#"><span class=annottext>forall a b c <p :: b-> a-> Bool, q :: c-> b-> Bool>. (x:b -> {VV : a<p x> | true}) -> (x:c -> {VV : b<q x> | true}) -> y:c -> exists [z:{VV : b<q y> | true}].{VV : a<p z> | true}</span><span class='hs-layout'>(</span></a><span class='hs-varop'>.</span><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>x:a -> {VV : b | ((papp2 p VV x))}</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>x:a -> {VV : b | ((papp2 q VV x))}</span><span class='hs-varid'>g</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>y</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:a -> {VV : b | ((papp2 p VV x1))}</span><span class='hs-varid'>f</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x1:a -> {VV : b | ((papp2 q VV x1))}</span><span class='hs-varid'>g</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a><span class='hs-layout'>)</span> </pre> Using (.) Operator ------------------ <br> <pre><span class=hs-linenum>110: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>plus3</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span> <span class='hs-keyword'>| v = x + 3}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>111: </span><a class=annot href="#"><span class=annottext>x:(Int) -> {VV : (Int) | (VV == (x + 3))}</span><span class='hs-definition'>plus3</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x2 : (Int) | (x2 == (x1 + x2))}</span><span class='hs-varid'>plus</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a> <a class=annot href="#"><span class=annottext>forall <q :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>. (x:(Int) -> {x8 : (Int)<p x> | true}) -> (x:(Int) -> {x9 : (Int)<q x> | true}) -> x3:(Int) -> exists [z:{x9 : (Int)<q x3> | true}].{x8 : (Int)<p z> | true}</span><span class='hs-varop'>.</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x2 : (Int) | (x2 == (x1 + x2))}</span><span class='hs-varid'>plus</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (2 : int))}</span><span class='hs-num'>2</span></a> </pre> <br> <div class="fragment">*Verifies!*</div> Using (.) Operator ------------------ <br> <pre><span class=hs-linenum>123: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>plus3</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span> <span class='hs-keyword'>| v = x + 3}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>124: </span><span class='hs-definition'>plus3</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>plus</span> <span class='hs-num'>1</span> <span class='hs-varop'>.</span> <span class='hs-varid'>plus</span> <span class='hs-num'>2</span> </pre> <br> LiquidHaskell *instantiates* - `p` with `\x -> v = x + 1` - `q` with `\x -> v = x + 2` Using (.) Operator ------------------ <br> <pre><span class=hs-linenum>138: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>plus3</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span> <span class='hs-keyword'>| v = x + 3}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>139: </span><span class='hs-definition'>plus3</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>plus</span> <span class='hs-num'>1</span> <span class='hs-varop'>.</span> <span class='hs-varid'>plus</span> <span class='hs-num'>2</span> </pre> <br> To *infer* that output of `plus3` has type: `exists [z:{v = y + 2}].{v = z + 1}` <div class="fragment"> `<:` `{v:Int|v=3}` </div> Recap ----- 1. **Refinements:** Types + Predicates 2. **Subtyping:** SMT Implication 3. **Measures:** Strengthened Constructors 4. **Abstract:** Refinements over Type Signatures + <div class="fragment">*Dependencies* using refinement parameters</div>