CDuce/Types/Coercion

Upward static coercion let x = 7;; -> val x : 7 = 7 x has the value 7 and is of the type 7 (the singleton containing the integer seven) let y1 = (x : Int);; let y2 : Int = x;; These two upward coercions give the same thing: the value 7 of type Int. This is possible because the singleton 7 is a subset of the integers set. Dynamic coercion The static downward coercion is not possible type Positive = 1--* let y = (7 : Int);; let yp = (y : Positive);; -> This expression should have type: Positive but its inferred type is: Int which is not a subtype, as shown by the sample: *--0 But the dynamic downward coercion is possible: let yp1 :? Positive = y;; let yp2 = (y :? Positive);; An exception is raised at execution is coercion is not possible let ybad = (y :? Char);; -> Uncaught CDuce exception: "Value 7 does not match type Empty\n" The message contains "Empty" because the dynamic coercion give the conjunction type. This can be seen writing (7 : 1--8) :? 5--10;; which appears having the type 5--8 Note that for upward coercion the static nethod is more efficient and gives better error handling. Furthermnore, due to the conjunction mechanism, the upward coercion cannot be dynamic: (7 : 1--8) :? Int;; continues to be of type 1--8, not Int.