tur/refine
named refinement types (predicate-annotated aliases).
Each alias below is a deftype bound to a contract type #refine{ x : T | p }. A parameter declared with one takes the BASE type at the C level, gets p as a runtime contract check on entry, and contributes p as a HYPOTHESIS the static discharger may use to prove the function's return refinement, in which case no runtime check is emitted for that return at all.
Static discharge is unconditional (the refined experiment graduated in v0.33.0; its --enable=refined / #lang turmeric refined shims were retired in v0.38.0 and are errors now). Nothing here takes a flag.
(import refine)
(defn double-pos [x : Pos] : #refine{ r : int | (> r 0) }
(* x 2)) ; return refinement proved statically; no check emitted
See docs/guides/refinement-types-guide.md.
Since: v1 (RT5b)
Nat
(deftype Nat #refine{ x : int | (>= x 0) })
a non-negative integer (>= 0).
(defn len-of [n : Nat] : int n) ; => callers must pass n >= 0
Since: v1
Pos
(deftype Pos #refine{ x : int | (> x 0) })
a strictly positive integer (> 0).
(defn halve [n : Pos] : int (/ n 2))
Since: v1
NonZero
(deftype NonZero #refine{ x : int | (not= x 0) })
an integer that is not zero. The canonical divisor type: a (/ n d) with d : NonZero can never divide by zero.
(defn safe-div [n : int, d : NonZero] : int (/ n d))
Since: v1
Neg
(deftype Neg #refine{ x : int | (< x 0) })
a strictly negative integer (< 0).
(defn abs-of-neg [n : Neg] : int (- 0 n))
Since: v1
Byte
(deftype Byte #refine{ x : int | (and (>= x 0) (<= x 255)) })
an integer in [0, 255].
(defn write-byte [b : Byte] : int b)
Since: v1
Percent
(deftype Percent #refine{ x : int | (and (>= x 0) (<= x 100)) })
an integer in [0, 100].
(defn scale [p : Percent] : int (/ (* p 255) 100))
Since: v1
NonNegFloat
(deftype NonNegFloat #refine{ x : float | (>= x 0.0) })
a non-negative float (>= 0.0). The domain of sqrt.
(defn root [x : NonNegFloat] : float (sqrt x))
Since: v1
PosFloat
(deftype PosFloat #refine{ x : float | (> x 0.0) })
a strictly positive float (> 0.0).
(defn recip [x : PosFloat] : float (/ 1.0 x))
Since: v1
UnitFloat
(deftype UnitFloat #refine{ x : float | (and (>= x 0.0) (<= x 1.0)) })
a float in [0.0, 1.0]; the usual interpolation parameter.
(defn lerp [a : float, b : float, t : UnitFloat] : float (+ a (* (- b a) t)))
Since: v1