Tipos refinados

Un tipo refinado (refinement type) restringe un tipo base con un predicado logico. El compilador utiliza un solver SMT (Z3) para verificar que los valores satisfacen el predicado en tiempo de compilacion, detectando errores fuera de rango antes de que el programa se ejecute.

Sintaxis

type Positive = { x: i32 | x > 0 }
type Percentage = { p: f64 | p >= 0.0 && p <= 100.0 }
type NonEmpty<T> = { arr: [T] | len(arr) > 0 }

El predicado despues del | debe ser una expresion booleana pura sobre la variable ligada y constantes. El compilador delega esto a Z3 para la verificacion de satisfacibilidad.

Uso de tipos refinados

fn safe_divide(a: f64, b: { b: f64 | b != 0.0 }) -> f64 {
    a / b
}

fn main() -> i32 with IO {
    let result = safe_divide(10.0, 3.0)   // OK: 3.0 != 0.0 proven
    println(result)

    // safe_divide(10.0, 0.0)  // compile error: cannot prove 0.0 != 0.0
}

Cuando se pasa un literal, el solver puede verificar la restriccion inmediatamente. Cuando se pasa una variable, el solver usa los refinamientos conocidos de la variable desde su sitio de declaracion.

Ejemplo de dosificacion

Los tipos refinados son especialmente poderosos en dominios cientificos donde las restricciones fisicas son importantes:

type ValidDose = { dose: mg | dose > 0.0 && dose <= 2000.0 }

fn administer(patient_id: i64, dose: ValidDose) with IO {
    println("Administering dose")
}

fn main() -> i32 with IO {
    let dose: mg = 500.0
    administer(1, dose)     // OK: 500.0 within range

    // let bad: mg = 5000.0
    // administer(1, bad)   // compile error: 5000.0 > 2000.0
}

Interaccion con tipos epistemicos

Los predicados de refinamiento se componen con Knowledge<T>: un Knowledge<ValidDose> lleva tanto el envelope de incertidumbre como la restriccion de refinamiento. El compilador verifica ambos de forma independiente — el refinamiento se aplica sobre el valor nominal, y la propagacion de confianza rastrea la incertidumbre de medicion.

Donde vive la verificacion de refinamientos

• Chequeo de tipos refinados: self-hosted/check/refinements.sio
• Integracion SMT: compiler/src/smt/ (bindings de Z3, requiere el feature flag smt)
• El artefacto nativo verificado (souc-linux-x86_64) tiene SMT deshabilitado; la verificacion de refinamientos esta disponible al compilar con --features smt

Limitaciones actuales

• La integracion con Z3 requiere el feature flag smt en tiempo de compilacion.
• No todas las formas de predicado estan soportadas — el solver maneja comparaciones aritmeticas, conectivos booleanos y restricciones de longitud de arreglo. Las llamadas a funciones personalizadas dentro de predicados aun no estan soportadas.
• Existe un fallback de asercion en tiempo de ejecucion para predicados que no pueden verificarse estaticamente.