# Simple Refinement Types

# Simple Refinement Types

Refinement Types = *Types* + *Predicates*

# Example: Integers equal to `0`

Refinement types via special comments `{-@ ... @-}`

# Example: Natural Numbers

# Exercise: Positive Integers

**Q:**First, can you fix`Pos`

so`poss`

is**rejected**?**Q:**Next, can you modify`poss`

so it is**accepted**?

# Type Checking

```
{-@ 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
```

# A Term Can Have *Many* Types

What *is* the type of `0`

?

```
{-@ zero :: Zero @-}
zero = 0
{-@ zero' :: Nat @-}
zero' = zero
```

# SMT Automates Implication Checking

**Eliminates boring proofs** ... makes verification practical.

# Contracts: Function Types

# Pre-Conditions

No value satisfies `false`

\(\Rightarrow\) **no valid inputs** for `impossible`

Program type-checks \(\Rightarrow\) `impossible`

**never called at run-time**

# Exercise: Pre-Conditions

Let's write a **safe division** function

**Q:** Yikes! Can you **fix the type** of `safeDiv`

to banish the error?

# Precondition Checked at Call-Site

**Precondition**

```
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
```

**Verifies As**

\[{(v = 2) \Rightarrow (v \not = 0)}\]

# Precondition Checked at Call-Site

**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?

# Recap

**Refinement Types** Types + Predicates

**Specify Properties**

Via Refined Input- and Output- Types

**Verify Properties**

Via SMT based Implication Checking

# Unfinished Business

How to describe **non empty lists**?

```
{-@ avg :: {v:[a]| 0 < length v } -> Pos @-}
```

Next: How to **describe properties of** structures [continue...]