6 Datatypes🔗ℹ

A datatype field may carry a refinement. This is proved at every constructor application, and assumed wherever a match pattern binds the field:

type Shape

| circle(radius :: {r :: Int | r > 0})

| square(side :: {s :: Int | s > 0})

fun area(sh :: Shape) :: {a :: Int | a > 0}:

match sh

| circle(r): 3 * r * r

| square(s): s * s

area(circle(2))          // accepted

area(circle(0))          // rejected: 0 > 0 is false

A field’s predicate may mention the constructor’s other fields:

type Span

| span(lo :: Int, hi :: {h :: Int | h >= lo})

A limitation of Liquid Shplait is that it can only establish the refinement check at direct constructors. In the example above, a call like map(circle, xs) would result in an error.