Data types: Strict and lazy

Values carry information, but not all values carry the same kind of information. The integer value forty-two and the character value 'a' are different kinds of value. A data type identifies such a kind and the values which belong to it.

IvoryScript is statically typed. Some fundamental types are:

      Int
      Double
      Char
      Bool
      String
   

The distinction established earlier between a value and an expression with a potential value is reflected directly in the type system.

The integer value:

#!42

has type:

Int

whereas the expression:

42

has type:

Exp Int

Int is a strict type. Exp Int is its corresponding lazy type. More generally, for any type a:

      a
      Exp a
   

are distinct types. A value of type Exp a is not an unfinished value of type a. It is a different value, with a potential value of type a.

The distinction can be observed directly:

      #!42       :: Int
      42         :: Exp Int

      #!1.0      :: Double
      1.0        :: Exp Double
   

It is not restricted to constants. A function application, lambda, let expression, conditional or other expression form may similarly have a lazy type. The type describes the value, not the particular syntax used to express it.

Strict and lazy values

The distinction between strict and lazy values is therefore explicit in their types. A program can contain both an integer and an integer expression at the same time:

         #!42       :: Int
         42         :: Exp Int
      

Neither type is a temporary description of the other. Int and Exp Int are distinct types. Reduction provides a relationship between them, but does not make them interchangeable.

Lazy types may themselves contain lazy types:

Exp (Exp Int)

A single reduction of a value of this type may have type Exp Int. No further reduction is implied.

Functions

Functions are values and have types in the usual way. A function accepting an integer and returning an integer may have type:

Int -> Int

A function taking two integers may have type:

Int -> Int -> Int

The arrow associates to the right, so this means:

Int -> (Int -> Int)

This corresponds naturally with currying. Applying the function to one integer may leave a function of type:

Int -> Int

The distinction between strict and lazy values applies equally to functions. A function value may have type:

Int -> Int

while an expression with such a function as its potential value has type:

Exp (Int -> Int)

Functions therefore require no special exemption from the distinction between strict and lazy values.

Type variables

Types need not always name one particular kind of value. A type variable such as:

a

stands for a type which is not yet fixed. Thus:

Exp a

describes an expression with a potential value of type a, whatever that type may be.

Similarly:

a -> a

describes a function which accepts a value of some type and returns a value of that same type. The identity function is the familiar example:

\x -> x

Its useful property does not depend upon x being an integer, character or any other particular kind of value. The relationship between the argument and result types is what matters.

Type variables allow such relationships to be expressed without unnecessarily restricting the values involved.

Thunks

IvoryScript also provides a thunk, written using lambda syntax but without a parameter:

\ -> e

A thunk is not a function awaiting an argument. It is a value wrapped in a closure. The values associated with any free variables occurring in e are captured and retained with it.

For example:

let x = 42 in \ -> x

retains the value associated with x when the thunk value first arises. Its meaning does not depend upon a later lookup of x in another environment.

This property is shared with ordinary lambdas. Both functions and thunks are closures. A function introduces one or more parameters; a thunk does not.

A thunk containing a value of type a has unary-arrow type:

-> a

This is distinct from:

Exp a

The relationship between the two is provided by:

fromThunk :: (-> a) -> Exp a

This conversion is the only special semantics associated with the thunk type. A thunk is therefore neither an ordinary function nor another notation for a lazy value. It is a value together with the captured values required to preserve its context.

Constructed types

Types may themselves be formed from other types. Exp is one example: applying it to Int forms Exp Int.

Lists provide another:

         [Int]
         [Char]
      

The element type may itself be lazy:

[Exp Int]

which describes a list of integer expressions. This is quite different from:

Exp [Int]

which describes an expression with a list of integers as its potential value.

Types can therefore describe precisely where lazy values occur within larger values. The same principle applies to tuples, functions and other constructed data types.

Types of functions over expressions

Strict and lazy types may be combined freely in function types. For example:

         Exp Int -> Int
         Int -> Exp Int
         Exp Int -> Exp Int
      

describe respectively a function from an integer expression to an integer, a function from an integer to an integer expression and a function from one integer expression to another.

These distinctions matter because an expression value and its potential value are not interchangeable merely because they are related.

How IvoryScript can nevertheless move conveniently between suitable strict and lazy types will be considered separately.

Exp therefore makes laziness explicit in the type. It is not a general property imposed upon every value in the language. Strict and lazy values can coexist and be combined within the same program, while the type system retains the distinction between them.