Coercion forms a bridge

Consider the IvoryScript integer addition function:

      addInt :: Int -> Int -> Int
   

The constants in:

      addInt 7 6
   

have type Exp Int, while addInt requires values of type Int. Without coercion, the reductions would have to be denoted explicitly:

      addInt #!7 #!6
   

Such conversions would be intrusive in ordinary expressions.

IvoryScript instead performs syntactic coercion. After initial parsing, the abstract syntax tree is rewritten to insert a COERCE directive wherever the form of a value may require conversion. Conceptually:

      addInt (COERCE 7) (COERCE 6)
   

During type inference, each coercion is either eliminated if the source and destination types unify, or replaced by an explicit reduction of the applicable conversion:

      COERCE e  =>  e

      COERCE e  =>  #!(cast e)
   

The first rule requires no conversion. The second uses the Cast relationship between the supplied and required types, with #! explicitly denoting reduction of the cast application.

For the example above, reduction itself provides the required conversion:

      Exp Int => Int
   

so the simple source form:

      addInt 7 6
   

can retain its natural structure without weakening the distinction between Exp Int and Int.

Syntactic coercion is therefore a compile-time rewriting process. The source remains concise, while the resulting expression explicitly denotes any conversions required by its types.

More than reduction

Coercion is not restricted to the direct relationship:

         Exp a => a
      

Other Cast instances may provide other conversions. This becomes apparent in:

         sum [pi, 2]
      

where the list items must all have the same type. There is no strict cast instance from Double to Int so Double values are required. So given that pi has type Exp Double, while 2 has type Exp Int, the required relationships include:

         Exp Double => Double

         Exp Int => Int => Double
      

The recursive Cast machinery described earlier allows reduction and other conversions to be combined. The source expression need not expose those intermediate relationships.

Controlling coercion

Most coercions are introduced automatically by the syntactic rewriting described above. Source forms allow this behaviour to be controlled explicitly.

The unary form:

         ::e
      

introduces a coercion at a point where one would not normally be inserted.

A name occurrence, for example:

         x
      

simply has the value associated with the name in scope. Where coercion of that value is required by the surrounding type context, this can be written:

         ::x
      

Conversely:

         ¬::e
      

suppresses a coercion which would normally be introduced. This is sometimes useful where allowing coercion would leave the type of an expression underconstrained.

The binary form:

         e :: t
      

coerces e to the specified type t. The value so denoted is not itself subject to further coercion.

Thus the three forms provide local control:

         ::e        introduce coercion
         ¬::e       suppress coercion
         e :: t     coerce to type t
      

None changes the distinction between the types involved. Where coercion is present, the source and required destination types determine the applicable Cast.

Coercion does not make related values of different types interchangeable. It provides a bridge between them, either introduced by the normal syntactic rewriting or explicitly denoted in the source.