Reduction as a type conversion

The distinction between IvoryScript's strict and lazy types provides another way to consider reduction.

A value of type:

      Exp a
   

has a potential value of type:

      a
   

Reduction therefore provides a conversion between values of different types:

      Exp a => a
   

IvoryScript expresses such conversions using the Cast type class:

      class Cast a, b where {
         cast :: a -> b
      }
   

Reduction is included directly:

      instance Cast Exp b, b where {
         inline cast x = #!x
      }
   

So a conversion from Exp b to b is therefore simply reduction. No separate mechanism is required to describe the relationship between a lazy value and its potential value.

The surface relationship is simple, but the type membership required to support more general conversions is less so:

      subordinate instance Cast Exp c, b | (not !c)  
                                           or !c
                                           and (instance StrictCast c, b) where {
         inline cast x = #!(cast (#!x))
      };
   

Although the type membership is complex, the significant part is the recursive form:

      #!(cast (#!x))
   

The inner #! denotes reduction of x. The resulting value is passed to cast, allowing the relationship between its type and the required type to be considered in turn. The outer #! denotes reduction of the cast application.

This allows reduction to expose another expression value, or a strict value requiring a further conversion, without changing the underlying model. Each reduction remains explicitly denoted and each conversion is determined by the types involved.

Reduction can therefore be regarded both as the transformation introduced earlier and as a particular form of type conversion. This becomes especially useful when the required conversion can be inferred from the surrounding type context.