Liquid Shplait🔗ℹ

Liquid Shplait implements “liquid” typing. Liquid types are a long line of work by Ranjit Jhala and collaborators, starting with this one. Liquid types are a form of refinement types, which were originally added to modern programming languages in this work. Here’s a more recent survey on the concept of refinement types. Liquid Shplait is directly inspired by and based on these ideas.

Liquid Shplait is a liquid extension to Shplait. A refinement attaches a predicate to a type. Thus, for instance, this example says that double takes only positive integers and returns positive integers:

#lang shplait/liquid

fun double({n :: Int | n > 0}) :: {y :: Int | y > 0}:
n * 2

While the program compiles, the checker turns every such claim into proof obligations and asks the Z3 solver to discharge them. If the body were n / 2 or n - 2, the program would not compile:

`double`, return: the claim `y > 0` is violated when n = 1

If, however, the function definition were changed to

#lang shplait/liquid

fun double({n :: Int | n > 2}) :: {y :: Int | y > 0}:
n - 2

then it would again type-check without any difficulty.

Checking refinements happens purely statically. The checker does not add run-time checks: any refinement that cannot be checked is rejected, not turned into a run-time check. Checking happens as part of type-checking, so if the program compiles (e.g., in DrRacket you see the REPL prompt), that means all the checks have passed.

#lang shplait/liquid

package: liquid-shplait

1 Installing Liquid Shplait

2 Running Programs

3 Refinements

4 What Liquid Shplait Proves

9 error, unreachable and assert

10 Polymorphic Functions

11 Mutable State

12 Checks at the Boundary

13 The Predicate Language

14 Timeout

15 Limitations

16 Examples

1	Installing Liquid Shplait
2	Running Programs
3	Refinements
4	What Liquid Shplait Proves
5	Rejections
6	Datatypes
7	Measure Functions
8	Checked Bodies
9	error, unreachable and assert
10	Polymorphic Functions
11	Mutable State
12	Checks at the Boundary
13	The Predicate Language
14	Timeout
15	Limitations
16	Examples