interface Embed a b where
embed : a -> bInjection sans perte : le type source tient dans le type cible. Nat s'injecte dans Int car tout Nat est un Int valide.
PréludeChargé par défaut — aucun
import nécessaire.Interfaces de coercition
Synopsis
interface Cast a b where
cast : a -> bConversion potentiellement avec perte. Int se convertit en Double (sans problème de précision pour les petits entiers).
interface TryCast a b where
tryCast : a -> Maybe bConversion pouvant échouer, renvoyant Maybe. Un Int négatif ne peut pas devenir un Nat.
isFinite : Double -> BoolVrai pour un Double de valeur réellement finie — exclut NaN et ±Infini. C'est le test de représentabilité que tryCast utilise ci-dessous : un Double fini est exactement l'ensemble des valeurs que truncate peut transformer en Int fidèle.
Conversions de commodité
toInt : Nat -> IntConvertit un Nat en Int (sans perte).
natToInt : Nat -> IntConvertit un Nat en Int (sans perte) — toInt sous le nom que suggère la conversion inverse (intToNat). natToInt 3 = 3.
toNat : Int -> Maybe NatTente de convertir un Int en Nat (échoue s'il est négatif).
toDouble : Int -> DoubleConvertit un Int en Double.
parseInt : String -> Maybe IntAnalyse un entier décimal signé depuis une chaîne ; Nothing si ce n'en est pas un. Le pendant SÛR de cast : String -> Double (qui est total et avec perte — il renvoie 0.0 sur n'importe quoi). parseInt "42" = Just 42, parseInt "x" = Nothing, parseInt "3.5" = Nothing.
parseDouble : String -> Maybe DoubleAnalyse un double fini depuis une chaîne ; Nothing s'il est inanalysable ou non fini (inf/nan). parseDouble "3.14" = Just 3.14, parseDouble "x" = Nothing.