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.