{#simplerefinements} ======================= Simple Refinement Types ----------------------- <div class="hidden"> <pre><span class=hs-linenum>10: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--no-termination"</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>11: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>SimpleRefinements</span> <span class='hs-keyword'>where</span> <span class=hs-linenum>12: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Language</span><span class='hs-varop'>.</span><span class='hs-conid'>Haskell</span><span class='hs-varop'>.</span><span class='hs-conid'>Liquid</span><span class='hs-varop'>.</span><span class='hs-conid'>Prelude</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-varid'>abs</span><span class='hs-layout'>,</span> <span class='hs-varid'>max</span><span class='hs-layout'>)</span> <span class=hs-linenum>14: </span> <span class=hs-linenum>15: </span><span class='hs-comment'>-- boring haskell type sigs</span> <span class=hs-linenum>16: </span><span class='hs-definition'>zero</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class=hs-linenum>17: </span><span class='hs-definition'>zero'</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class=hs-linenum>18: </span><span class='hs-definition'>safeDiv</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>19: </span><span class='hs-definition'>abs</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>20: </span><span class='hs-definition'>nats</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-conid'>Int</span> <span class=hs-linenum>21: </span><span class='hs-definition'>evens</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-conid'>Int</span> <span class=hs-linenum>22: </span><span class='hs-definition'>odds</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-conid'>Int</span> <span class=hs-linenum>23: </span><span class='hs-definition'>range</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'>L</span> <span class='hs-conid'>Int</span> </pre> </div> Simple Refinement Types ======================= Types + Predicates ------------------ Example ------- Integers equal to `0` <br> <pre><span class=hs-linenum>45: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>EqZero</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>{</span><span class='hs-varid'>v</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>0</span><span class='hs-layout'>}</span> <span class='hs-keyword'>@-}</span> </pre> Example ------- Integers equal to `0` <br> <pre><span class=hs-linenum>57: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>zero</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>EqZero</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>58: </span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV == 0)}</span><span class='hs-definition'>zero</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:(Int#) -> {x2 : (Int) | (x2 == (x1 : int))}</span><span class='hs-num'>0</span></a> </pre> <br> <div class="fragment"> Refinement types via special comments `{-@ ... @-}` </div> <br> <div class="fragment"> <a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo</a> Lets take a look. </div> {#refinementsArePredicates} ============================ Refinements Are Predicates -------------------------- Refinements Are Predicates ========================== Subtyping is Implication ------------------------ [Predicate Subtyping](http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf) Subtyping is Implication ------------------------ <br> -------- --- --------------------------------------------- **If** : Refinement of `S` *implies* refinement of `T` **Then** : `S` is a *subtype* of `T` -------- --- --------------------------------------------- <br> Subtyping is Implication ------------------------ <br> -------- --- ---------------------------- **If** : `p => q` **Then** : `{v : t | p} <: {v : t | q}` -------- --- ---------------------------- Subtyping is Implication ------------------------ <br> -------- --- --------------------------------------------------- **As** : `v=0` *implies* `0<=v` ... via SMT **So** : `{v:Int | v=0} <: {v:Int | 0<=v}` -------- --- --------------------------------------------------- Example: Natural Numbers ------------------------ . <pre><span class=hs-linenum>134: </span><span class='hs-keyword'>type</span> <span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>{</span><span class='hs-varid'>v</span> <span class='hs-conop'>:</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>|</span> <span class='hs-num'>0</span> <span class='hs-varop'><=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span> </pre> <br> Via SMT, LiquidHaskell infers `EqZero <: Nat`, hence: <br> <pre><span class=hs-linenum>144: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>zero'</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Nat</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>145: </span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-definition'>zero'</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == 0) && (x3 == SimpleRefinements.zero)}</span><span class='hs-varid'>zero</span></a> </pre> {#universalinvariants} ======================= Types = Universal Invariants ---------------------------- (Notoriously hard with *pure* SMT) Types Yield Universal Invariants ================================ Example: Lists -------------- <div class="hidden"> <pre><span class=hs-linenum>164: </span><span class='hs-keyword'>infixr</span> <span class='hs-varop'>`C`</span> </pre> </div> <pre><span class=hs-linenum>169: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>N</span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>C</span> <span class='hs-varid'>a</span> <span class='hs-layout'>(</span><span class='hs-conid'>L</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> </pre> <br> <div class="fragment"> *Every element* in `nats` is non-negative: <pre><span class=hs-linenum>177: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>nats</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-conid'>Nat</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>178: </span><a class=annot href="#"><span class=annottext>(L {VV : (Int) | (VV >= 0)})</span><span class='hs-definition'>nats</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>{x14 : (Int) | (x14 >= 0) && (x14 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x14)} -> (L {x14 : (Int) | (x14 >= 0) && (x14 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x14)}) -> (L {x14 : (Int) | (x14 >= 0) && (x14 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x14)})</span><span class='hs-varop'>`C`</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>{x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)} -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}) -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (3 : int))}</span><span class='hs-num'>3</span></a> <a class=annot href="#"><span class=annottext>{x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)} -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}) -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>(L {x2 : (Int) | false})</span><span class='hs-conid'>N</span></a> </pre> </div> <br> <div class="fragment"> <a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo:</a> What if `nats` contained `-2`? </div> Example: Even/Odd Lists ----------------------- <pre><span class=hs-linenum>195: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>Even</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>{</span><span class='hs-varid'>v</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>v</span> <span class='hs-varid'>mod</span> <span class='hs-num'>2</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>0</span><span class='hs-layout'>}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>196: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>Odd</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>{</span><span class='hs-varid'>v</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>v</span> <span class='hs-varid'>mod</span> <span class='hs-num'>2</span> <span class='hs-varop'>/=</span> <span class='hs-num'>0</span><span class='hs-layout'>}</span> <span class='hs-keyword'>@-}</span> </pre> <br> <div class="fragment"> <pre><span class=hs-linenum>203: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>evens</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-conid'>Even</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>204: </span><a class=annot href="#"><span class=annottext>(L {VV : (Int) | ((VV mod 2) == 0)})</span><span class='hs-definition'>evens</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>{x17 : (Int) | ((x17 mod 2) == 0) && (x17 >= 0) && (x17 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x17)} -> (L {x17 : (Int) | ((x17 mod 2) == 0) && (x17 >= 0) && (x17 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x17)}) -> (L {x17 : (Int) | ((x17 mod 2) == 0) && (x17 >= 0) && (x17 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x17)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (2 : int))}</span><span class='hs-num'>2</span></a> <a class=annot href="#"><span class=annottext>{x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)} -> (L {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)}) -> (L {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (4 : int))}</span><span class='hs-num'>4</span></a> <a class=annot href="#"><span class=annottext>{x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)} -> (L {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)}) -> (L {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>(L {x2 : (Int) | false})</span><span class='hs-conid'>N</span></a> <span class=hs-linenum>205: </span> <span class=hs-linenum>206: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>odds</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-conid'>Odd</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>207: </span><a class=annot href="#"><span class=annottext>(L {VV : (Int) | ((VV mod 2) == 1)})</span><span class='hs-definition'>odds</span></a> <span class='hs-keyglyph'>=</span> <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>{x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)} -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}) -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (3 : int))}</span><span class='hs-num'>3</span></a> <a class=annot href="#"><span class=annottext>{x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)} -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}) -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (5 : int))}</span><span class='hs-num'>5</span></a> <a class=annot href="#"><span class=annottext>{x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)} -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}) -> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>(L {x2 : (Int) | false})</span><span class='hs-conid'>N</span></a> </pre> </div> <div class="fragment"> <a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo:</a> What if `evens` contained `1`? </div> {#functiontypes} ================= Contracts = Function Types -------------------------- Contracts: Function Types ========================= Example: `safeDiv` ------------------ <br> **Precondition** divisor is *non-zero*. <br> <div class="fragment"> <pre><span class=hs-linenum>237: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>NonZero</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>{</span><span class='hs-varid'>v</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>v</span> <span class='hs-varop'>/=</span> <span class='hs-num'>0</span><span class='hs-layout'>}</span> <span class='hs-keyword'>@-}</span> </pre> </div> <br> Example: `safeDiv` ------------------ <br> + **Pre-condition** divisor is *non-zero*. + **Input type** specifies *pre-condition* <br> <pre><span class=hs-linenum>254: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>safeDiv</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>NonZero</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>255: </span><a class=annot href="#"><span class=annottext>(Int) -> {VV : (Int) | (VV /= 0)} -> (Int)</span><span class='hs-definition'>safeDiv</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>{VV : (Int) | (VV /= 0)}</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) -> {x6 : (Int) | (((x1 >= 0) && (x2 >= 0)) => (x6 >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (x6 <= x1)) && (x6 == (x1 / x2))}</span><span class='hs-varop'>`div`</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == y) && (x3 /= 0)}</span><span class='hs-varid'>y</span></a> </pre> <br> <div class="fragment"> <a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo:</a> What if precondition does not hold? </div> Example: `abs` -------------- <br> + **Postcondition** result is non-negative + **Output type** specifies *post-condition* <br> <pre><span class=hs-linenum>278: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>abs</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-conid'>Nat</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>279: </span><a class=annot href="#"><span class=annottext>(Int) -> {VV : (Int) | (VV >= 0)}</span><span class='hs-definition'>abs</span></a> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>x</span></a> <span class=hs-linenum>280: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 <= x2))}</span><span class='hs-varop'><=</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == x)}</span><span class='hs-varid'>x</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> <span class=hs-linenum>281: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == x)}</span><span class='hs-varid'>x</span></a> </pre> {#dependentfunctions} ====================== Dependent Function Types ------------------------ + Outputs *refer to* inputs + *Relational* invariants Dependent Function Types ======================== Example: `range` ---------------- `(range i j)` returns `Int`s between `i` and `j` Example: `range` ---------------- `(range i j)` returns `Int`s between `i` and `j` <br> <pre><span class=hs-linenum>313: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>Btwn</span> <span class='hs-conid'>I</span> <span class='hs-conid'>J</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>{</span><span class='hs-varid'>v</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span><span class='hs-keyglyph'>|</span><span class='hs-layout'>(</span><span class='hs-conid'>I</span> <span class='hs-varop'><=</span> <span class='hs-varid'>v</span> <span class='hs-varop'>&&</span> <span class='hs-varid'>v</span> <span class='hs-varop'><</span> <span class='hs-conid'>J</span><span class='hs-layout'>)</span><span class='hs-layout'>}</span> <span class='hs-keyword'>@-}</span> </pre> Example: `range` ---------------- `(range i j)` returns `Int`s between `i` and `j` <br> <pre><span class=hs-linenum>324: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>range</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>i</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>j</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>L</span> <span class='hs-layout'>(</span><span class='hs-conid'>Btwn</span> <span class='hs-varid'>i</span> <span class='hs-varid'>j</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>325: </span><a class=annot href="#"><span class=annottext>i:(Int) -> j:(Int) -> (L {v : (Int) | (v < j) && (i <= v)})</span><span class='hs-definition'>range</span></a> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>j</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x10 : (Int) | (x10 >= i) && (i <= x10)} -> (L {x7 : (Int) | (x7 >= i) && (x7 >= x1) && (x7 < j) && (i <= x7) && (x1 <= x7)})</span><span class='hs-varid'>go</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == i)}</span><span class='hs-varid'>i</span></a> <span class=hs-linenum>326: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>327: </span> <a class=annot href="#"><span class=annottext>n:{VV : (Int) | (VV >= i) && (i <= VV)} -> (L {VV : (Int) | (VV >= i) && (VV >= n) && (VV < j) && (i <= VV) && (n <= VV)})</span><span class='hs-varid'>go</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= i) && (i <= VV)}</span><span class='hs-varid'>n</span></a> <span class=hs-linenum>328: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == n) && (x4 >= i) && (i <= x4)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}</span><span class='hs-varop'><</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == j)}</span><span class='hs-varid'>j</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == n) && (x4 >= i) && (i <= x4)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>{x20 : (Int) | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)} -> (L {x20 : (Int) | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)}) -> (L {x20 : (Int) | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>n:{VV : (Int) | (VV >= i) && (i <= VV)} -> (L {VV : (Int) | (VV >= i) && (VV >= n) && (VV < j) && (i <= VV) && (n <= VV)})</span><span class='hs-varid'>go</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == n) && (x4 >= i) && (i <= x4)}</span><span class='hs-varid'>n</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 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>329: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>(L {x2 : (Int) | false})</span><span class='hs-conid'>N</span></a> </pre> <br> <div class="fragment"> **Question:** What is the type of `go` ? </div> Example: Indexing Into List --------------------------- <pre><span class=hs-linenum>343: </span><span class='hs-layout'>(</span><span class='hs-varop'>!</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class=hs-linenum>344: </span><span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-keyword'>_</span><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>forall a. (L a) -> (Int) -> a</span><span class='hs-varop'>!</span></a> <span class='hs-num'>0</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a> <span class=hs-linenum>345: </span><span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-keyword'>_</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-varop'>!</span> <span class='hs-varid'>i</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>(L a)</span><span class='hs-varid'>xs</span></a> <a class=annot href="#"><span class=annottext>(L a) -> (Int) -> a</span><span class='hs-varop'>!</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>346: </span><span class='hs-keyword'>_</span> <span class='hs-varop'>!</span> <span class='hs-keyword'>_</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x1 : [(Char)] | false} -> {VV : a | false}</span><span class='hs-varid'>liquidError</span></a> <span class=hs-error><a class=annot href="#"><span class=annottext>{x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-str'>"Oops!"</span></a></span> </pre> <br> <div class="fragment">(Mouseover to view type of `liquidError`)</div> <br> - <div class="fragment">**Q:** How to ensure safety? </div> - <div class="fragment">**A:** Precondition: `i` between `0` and list **length**. <div class="fragment">Need way to [measure](#measures) *length of a list* ...</div>