Some expressions have no value

Most expressions considered so far have a potential value. Some expressions do not.

IvoryScript uses the type:

      Void
   

to denote the absence of a value. There is no Void value to pass as an argument, copy, store or otherwise manipulate.

This does not mean that an expression whose reduction has type Void can have no effect. A function may, for example, perform I/O or modify a pointer etc.:

      f :: a -> Void
   

The distinction becomes important with lazy types. Although there is no value of type:

      Void
   

there can be a perfectly valid expression value of type:

      Exp Void
   

Such an expression is a first class value in IvoryScript, even with no potential direct value.

This also explains a special case in an Order script. An expression normally has to be coercible to something which can be displayed, but an expression of type Exp Void has no resulting value to display. It is nevertheless a valid expression in the sequence.

Void and sequencing

Void is closely related to sequencing. The relevant reduction rule is:

         Reduce (SEQ e1 e2) ρ => ValOf e1 ρ; ValOf e2 ρ
      

Here ValOf e1 ρ must be Void.

SEQ is a primitive where, on reduction, its first argument must reduce to Void and then yield the value denoted by e2.

This is the precise role of Void: a reduction may contribute no value while still being required by the enclosing expression.

Exp Void is different. It is itself a value, representing an expression whose reduction has no value.

The simplest example of this is the Void data constructor. Like any other, it is lazy, so Void :: Exp Void, and #!Void is an ordinary reduction. Its reduction rule, however, yields no value.

The distinction is therefore simple:

         Void        absence of a value
         Exp Void    a value representing an expression with no value