Τύποι εκλέπτυνσης

Ένας refinement type (τύπος εκλέπτυνσης) περιορίζει έναν βασικό τύπο με ένα λογικό κατηγόρημα. Ο compiler χρησιμοποιεί έναν SMT solver (Z3) για να ελέγξει ότι οι τιμές ικανοποιούν το κατηγόρημα κατά τη μεταγλώττιση, εντοπίζοντας σφάλματα εκτός ορίων πριν εκτελεστεί το πρόγραμμα.

Σύνταξη

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

Το κατηγόρημα μετά το | πρέπει να είναι μια καθαρή boolean έκφραση πάνω στη δεσμευμένη μεταβλητή και σταθερές. Ο compiler αναθέτει αυτό στο Z3 για έλεγχο ικανοποιησιμότητας.

Χρήση refinement types

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
}

Όταν περνάτε ένα literal, ο solver μπορεί να επαληθεύσει τον περιορισμό αμέσως. Όταν περνάτε μια μεταβλητή, ο solver χρησιμοποιεί τα γνωστά refinements της μεταβλητής από τη θέση δήλωσής της.

Παράδειγμα δοσολογίας

Οι refinement types είναι ιδιαίτερα ισχυροί σε επιστημονικούς τομείς όπου οι φυσικοί περιορισμοί έχουν σημασία:

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
}

Αλληλεπίδραση με επιστημικούς τύπους

Τα κατηγορήματα refinement συνδυάζονται με Knowledge<T>: ένα Knowledge<ValidDose> φέρει τόσο το περίβλημα αβεβαιότητας όσο και τον περιορισμό refinement. Ο compiler ελέγχει και τα δύο ανεξάρτητα — το refinement ισχύει στην ονομαστική τιμή, και η διάδοση εμπιστοσύνης παρακολουθεί την αβεβαιότητα μέτρησης.

Πού βρίσκεται ο έλεγχος refinement

• Έλεγχος refinement types: self-hosted/check/refinements.sio
• Ενσωμάτωση SMT: compiler/src/smt/ (Z3 bindings, απαιτεί smt feature flag)
• Το ελεγμένο native artifact (souc-linux-x86_64) έχει το SMT απενεργοποιημένο· ο έλεγχος refinement είναι διαθέσιμος κατά τη μεταγλώττιση με --features smt

Τρέχοντες περιορισμοί

• Η ενσωμάτωση Z3 απαιτεί το smt feature flag κατά τη μεταγλώττιση.
• Δεν υποστηρίζονται όλες οι μορφές κατηγορημάτων — ο solver χειρίζεται αριθμητικές συγκρίσεις, boolean συνδέσμους και περιορισμούς μήκους πίνακα. Οι κλήσεις custom συναρτήσεων σε κατηγορήματα δεν υποστηρίζονται ακόμα.
• Υπάρχει εναλλακτικό runtime assertion για κατηγορήματα που δεν μπορούν να επαληθευτούν στατικά.