Refinements

The Refinements module provides refinement types that constrain values beyond what the base type system expresses. Refinement types add predicates to base types, ensuring values meet specific criteria at the type level.

import Refinements

# A function that requires a positive integer
sqrt-int : PositiveInt -> Float
sqrt-int = fn(n) => sqrt (to-float n)

# A function that requires a non-empty string
first-char : NonEmptyString -> Char
first-char = fn(s) => String.char-at 0 s

Refinement Type Syntax

Refinement types use the syntax: {binding: BaseType | predicate}

# Define a refinement type for positive integers
type PositiveInt = {n: Int | n > 0}

# Define a refinement type with multiple constraints
type Percentage = {p: Float | p >= 0.0 and p <= 100.0}

# Define a refinement type for non-empty lists
type NonEmptyList a = {xs: [a] | length(xs) > 0}

Numeric Refinements

Type	Definition	Description
PositiveInt	{n: Int | n > 0}	Integers greater than zero
NonNegativeInt	{n: Int | n >= 0}	Integers greater than or equal to zero
NegativeInt	{n: Int | n < 0}	Integers less than zero
NonZero	{n: Int | n != 0}	Integers not equal to zero
PositiveFloat	{f: Float | f > 0.0}	Floats greater than zero
NegativeFloat	{f: Float | f < 0.0}	Floats less than zero
NonZeroFloat	{f: Float | f != 0.0}	Floats not equal to zero
FiniteFloat	{f: Float | Float.finite? f}	Floats that are neither NaN nor infinite

Usage Examples

# Safe division that can't divide by zero
safe-div : (Int, NonZero) -> Int
safe-div = fn(a, b) => a / b

# Square root that only accepts positive numbers
safe-sqrt : PositiveFloat -> Float
safe-sqrt = fn(x) => sqrt x

# Array index that's always valid (for arrays of at least n elements)
safe-nth : (NonNegativeInt, List a) -> Option a
safe-nth = fn(i, xs) => nth i xs

Bounded Numerics

Type	Definition	Description
Byte	{n: Int | n >= 0 and n <= 255}	Integers in the range 0-255 (unsigned byte)
Percentage	{p: Float | p >= 0.0 and p <= 100.0}	Floats in the range 0-100

Usage Examples

# RGB color using bytes
type RGB = {r: Byte, g: Byte, b: Byte}

red = {r: 255, g: 0, b: 0}

# Progress indicator using percentage
show-progress : Percentage -> String
show-progress = fn(p) => "${p}% complete"

String Refinements

Type	Definition	Description
NonEmptyString	{s: String | length(s) > 0}	Strings with at least one character

Usage Examples

# A name that can't be empty
type Name = NonEmptyString

# Greet function that's guaranteed to have a name
greet : NonEmptyString -> String
greet = fn(name) => "Hello, ${name}!"

# Get first character (always safe for NonEmptyString)
initial : NonEmptyString -> Char
initial = fn(s) => String.char-at 0 s

Collection Refinements

Type	Definition	Description
NonEmptyList a	{xs: [a] | length(xs) > 0}	Lists with at least one element
NonEmptyMap k v	{m: Map k v | not (Map.is-empty? m)}	Maps with at least one entry
NonEmptySet a	{s: Set a | not (Set.is-empty? s)}	Sets with at least one element

Usage Examples

# Head is always safe for NonEmptyList
safe-head : NonEmptyList a -> a
safe-head = fn(xs) => head xs

# Average of a non-empty list
average : NonEmptyList Int -> Float
average = fn(xs) => (sum xs) / (length xs)

# Get any key from a non-empty map
any-key : NonEmptyMap k v -> k
any-key = fn(m) => m |> Map.keys |> head

# Runtime validation to create a PositiveInt
to-positive : Int -> Result PositiveInt String
to-positive = fn(n) =>
  if n > 0 then
    Ok n
  else
    Err "Value must be positive"