True is a bad argument10 is a good argument0fib is an uninterpreted function0averagetakefibfib is an uninterpreted function
Refinement Types = Types + Predicates
0Refinement types via special comments {-@ ... @-}
Q: First, can you fix Pos so poss is rejected?
Q: Next, can you modify poss so it is accepted?
{-@ type Pos = {v:Int | 0 < v} @-}
{-@ poss :: [Pos] @-}
poss = [1, 2, 3]
Type Checking Via Implication Checking.
v = 1 => 0 < v
v = 2 => 0 < v
v = 3 => 0 < v
{-@ type Pos = {v:Int | 0 < v} @-}
Refinements Drawn from Decidable logics.
For automatic, decidable (and thus predictable) SMT type checking.
What is the type of 0 ?
{-@ zero :: Zero @-}
zero = 0
{-@ zero' :: Nat @-}
zero' = zero
In environment \(\Gamma\) the type \(t_1\) is a subtype of the type \(t_2\)
\[\boxed{\Gamma \vdash t_1 \preceq t_2}\]
Environment \(\Gamma\) is a sequence of binders
\[\Gamma \doteq \overline{\bindx{x_i}{P_i}}\]
\[\boxed{\Gamma \vdash t_1 \preceq t_2}\]
\[ \begin{array}{rll} {\mathbf{If\ VC\ is\ Valid}} & \bigwedge_i P_i \Rightarrow Q \Rightarrow R & (\mbox{By SMT}) \\ & & \\ {\mathbf{Then}} & \overline{\bindx{x_i}{P_i}} \vdash \reft{v}{b}{Q} \preceq \reft{v}{b}{R} & \\ \end{array} \]
\[ \begin{array}{rcrccll} \mathbf{VC\ is\ Valid:} & \True & \Rightarrow & v = 0 & \Rightarrow & 0 \leq v & \mbox{(by SMT)} \\ & & & & & & \\ \mathbf{So:} & \emptyset & \vdash & \Zero & \preceq & \Nat & \\ \end{array} \]
And so, we can type:
\[ \begin{array}{rcrccll} \mathbf{VC\ is\ Valid:} & x = 3 & \Rightarrow & v = x + 1 & \Rightarrow & 0 \leq v & \mbox{(by SMT)} \\ & & & & & \\ \mathbf{So:} & x = 3 & \vdash & \{v:Int\ |\ v = x + 1\} & \preceq & \Nat & \\ \end{array} \]
And so, we can type:
Eliminates boring proofs ... makes verification practical.
No value satisfies false \(\Rightarrow\) no valid inputs for impossible
Program type-checks \(\Rightarrow\) impossible never called at run-time
Let's write a safe division function
Q: Yikes! Can you fix the type of safeDiv to banish the error?
Precondition
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
Verifies As
\[{(v = 2) \Rightarrow (v \not = 0)}\]
Rejected as n can be any Nat
\[0 \leq n \Rightarrow (v = n) \not \Rightarrow (v \not = 0)\]
How to talk about list length in logic?
Refinement Types Types + Predicates
Specify Properties
Via Refined Input- and Output- Types
Verify Properties
Via SMT based Implication Checking
How to describe non empty lists?
{-@ avg :: {v:[a]| 0 < length v } -> Pos @-}
Next: How to describe properties of structures [continue...]