← Back to Examples

07 Refinement Types Demo

Refinement Types Demo Demonstrates the syntax and usage of refinement types in Cure Refinement types allow adding constraints to base types using the syntax: {variable: BaseType | constraint} The constraint is a boolean expression that must hold for all values of that type. This enables compile-time verification of properties like: - Non-zero divisors - Positive numbers - Bounded values (percentages, years, etc.)

Source Code

# Refinement Types Demo
# Demonstrates the syntax and usage of refinement types in Cure
#
# Refinement types allow adding constraints to base types using the syntax:
#   {variable: BaseType | constraint}
#
# The constraint is a boolean expression that must hold for all values
# of that type. This enables compile-time verification of properties like:
#   - Non-zero divisors
#   - Positive numbers
#   - Bounded values (percentages, years, etc.)

module RefinementTypesDemo do
  export [main/0]
  
  # Example 1: NonZero integers for safe division
  # This refinement type ensures the divisor is never zero
  def safe_divide(a: Int, b: {x: Int | x != 0}): Int =
    a / b
  
  # Example 2: Positive integers
  # Useful for square roots, logarithms, etc.
  def process_positive(n: {x: Int | x > 0}): Int =
    n * 2
  
  # Example 3: Bounded integers (percentage)
  # Ensures values are between 0 and 100
  def make_percentage(value: {p: Int | 0 <= p and p <= 100}): Int =
    value
  
  # Example 4: Range constraints
  def process_year(year: {y: Int | y >= 1900 and y <= 2100}): Int =
    year
  
  # Example 7: Non-empty string  (would need string length)
  # def process_non_empty(s: {str: String | length(str) > 0}): String =
  #   s
  
  def main(): Int =
    # Demonstration of refinement types:
    # These calls are valid because arguments satisfy the refinements
    let result1 = safe_divide(10, 2)  # 2 != 0 ✓
    let result2 = process_positive(5)  # 5 > 0 ✓
    let result3 = make_percentage(50)  # 0 <= 50 <= 100 ✓
    let result4 = process_year(2025)  # 1900 <= 2025 <= 2100 ✓
    
    # These would FAIL at compile time (constraint violations):
    # let bad1 = safe_divide(10, 0)  # 0 == 0, violates x != 0
    # let bad2 = process_positive(0)  # 0 not > 0
    # let bad3 = make_percentage(101)  # 101 > 100
    # let bad4 = process_year(1899)  # 1899 < 1900
    
    result1
end