Refinement Types

Refinement types add predicates to types that are checked at runtime. They catch invalid values at function boundaries, making your code safer and more self-documenting.

Basic Syntax

A refinement type is a type alias with a predicate:

type Name = BaseType as binder | predicate

• BaseType — The underlying type being refined
• binder — A name bound to the value being checked
• predicate — An expression that must evaluate to True

Simple Refinements

Numeric Constraints

-- Positive integers: must be > 0
type Positive = Int as n | n > 0

-- Non-negative integers: must be >= 0
type NonNegative = Int as n | n >= 0

-- Probability: float in [0, 1]
type Probability = Float as p | p >= 0.0 && p <= 1.0

-- Percentage: integer in [0, 100]
type Percentage = Int as p | p >= 0 && p <= 100

Using Refined Types

fn sqrt_positive(x: Positive) -> Float
  sqrt(to_float(x))
end fn

fn format_probability(p: Probability) -> String
  "${to_stringf(p * 100.0)}%"
end fn

When you call these functions, the predicate is checked:

sqrt_positive(25)   -- OK: 25 > 0
sqrt_positive(-4)   -- ERROR: refinement violated

Error Messages

When a refinement fails, you get a clear error message that includes:

• The type name (if it's a named type alias)
• The actual value that failed
• The predicate that wasn't satisfied

refinement violated for type 'Positive': n = -4 does not satisfy (n > 0)

For list refinements:

refinement violated for type 'NonEmpty': xs = [] does not satisfy (length(xs) > 0)

List Refinements

You can refine collection types using predicate functions:

-- Non-empty lists
type NonEmpty = List[Int] as xs | length(xs) > 0

-- All elements positive
type AllPositive = List[Int] as xs | all(fn(x: Int) -> x > 0, xs)

-- Normalized vector (sum of squares = 1)
type UnitVector = List[Float] as xs | normalized(xs)

Using list refinements:

fn safe_head(xs: NonEmpty) -> Int
  head(xs) | unwrap  -- safe: we know xs is non-empty
end fn

fn process_positive(xs: AllPositive) -> Int
  sum(xs)  -- all elements guaranteed positive
end fn

Where Clauses

For constraints involving multiple parameters, use where clauses:

fn safe_divide(a: Int, b: Int) -> Int
where b != 0
do
  a / b
end fn

The where clause comes before do, which starts the function body.

Multi-Parameter Constraints

fn zip_equal(xs: List[Int], ys: List[Int]) -> List[Tuple[Int, Int]]
where length(xs) == length(ys)
do
  -- implementation knowing lists are same length
end fn

fn in_range(value: Int, min: Int, max: Int) -> Int
where min <= max && value >= min && value <= max
do
  value
end fn

Combining Refinements and Where Clauses

You can use both parameter refinements and where clauses:

fn normalize(xs: NonEmpty) -> List[Float]
where sum(xs) != 0
do
  total = to_float(sum(xs))
  map(fn(x: Int) -> to_float(x) / total, xs)
end fn

Predicate Functions

These built-in functions are useful in refinement predicates:

Function	Description
all(pred, list)	True if all elements satisfy predicate
any(pred, list)	True if any element satisfies predicate
length(list)	Number of elements
normalized(list)	True if sum of squares equals 1
is_power_of_2(n)	True if n is a power of 2

Important Notes

Runtime Checking

Refinements are checked at runtime when calling functions. They are not checked at compile time.

x = -5
-- No error here - just binding an Int
sqrt_positive(x)  -- ERROR happens here at runtime

Handling Failures

Refinement violations use the Fail[String] effect, which means you can catch them using the standard error handling mechanisms.

Catching refinement errors:

type Positive = Int as n | n > 0

fn sqrt_positive(x: Positive) -> Float
  sqrt(to_float(x))
end fn

fn try_sqrt(x: Int) -> Result[Float, String]
  catch sqrt_positive(x)
end fn

fn main() -> Unit using file_io
  match try_sqrt(-5)
    Ok(result) -> print("Result: ${to_stringf(result)}")
    Err(msg) -> print("Error: ${msg}")
  end match
end fn
-- Output: Error: refinement violated for type 'Positive': n = -5 does not satisfy (n > 0)

Providing a default value:

fn safe_sqrt(x: Int) -> Float
  catch sqrt_positive(x) else 0.0
end fn

Where clause errors also use the Fail effect and include the failing condition:

fn divide(a: Int, b: Int) -> Int
where b != 0
do
  a / b
end fn

fn main() -> Unit using file_io
  match catch divide(10, 0)
    Ok(n) -> print(to_string(n))
    Err(msg) -> print(msg)
  end match
end fn
-- Output: where clause violated: condition (b != 0) is false

No Implicit Subtyping

A refined type is not automatically usable where the base type is expected:

type Positive = Int as n | n > 0

fn takes_int(x: Int) -> Int
  x * 2
end fn

p: Positive = 5  -- This works
-- takes_int(p)   -- This would be a type error!

Why? This design prevents accidental loss of guarantees. If Positive were silently convertible to Int, you could pass it to a function that negates it, losing the "positive" property.

Working with refined types: The best approach is to design your functions to accept the refined type:

-- Instead of taking Int, take the refined type
fn double_positive(x: Positive) -> Int
  -- Inside this function, you know x > 0
  to_int_from_positive(x) * 2  -- hypothetical conversion
end fn

Current limitation: Kettle doesn't yet have a built-in way to "unwrap" a refined type to its base type. For now, use refinement types primarily at function boundaries for validation, rather than throughout your code:

-- Good: Validate at the boundary, then work with Int
fn process_positive_input(x: Positive) -> Int
  -- x is validated; work with it as Int inside
  x * 2  -- This works because the return type is Int
end fn

This limitation may be addressed in a future version with an unrefine function.

When to Use Refinements

Refinement types are ideal for:

• Input validation — Check values at API boundaries
• Domain constraints — Encode business rules in types
• Documentation — Make constraints visible in function signatures
• Defensive programming — Catch invalid states early

Example: Safe Division

type NonZero = Int as n | n != 0

fn divide(a: Int, b: NonZero) -> Int
  a / b
end fn

fn main() -> Unit using file_io
  print(divide(10, 2))   -- OK: 5
  print(divide(10, 5))   -- OK: 2
  -- print(divide(10, 0))  -- ERROR: refinement violated
end fn

Next Steps

• Linear Types — Another kind of type-level safety
• Effects System — How effects interact with refinements
• Capabilities — Compile-time guarantees