Type Language

The type language, defined by

provides the type of static base values S and the type of dynamic values D. Function space construction comes in three variants indicated by : S denotes a completely static function, M a memoized function, and a function which is neither completely static nor memoized. We usually drop the subscript . describes constructed data, in our case argument lists. Finally, we have recursive types and type variables in order to have precise types for recursively constructed data. There will be no rules that explicitly introduce recursive types. Instead we adopt infinite regular type terms in the type language and adopt the notation for representing infinite types. Type variables only occur bound by the explicit construction, they never occur in infinite type terms.

Types are ordered by the strict inequalities shown in Fig. 2.

  

Figure 2: Ordering on types

All type constructors are monotonic (covariant) in all arguments with respect to the ordering.

The predicates static and memo on types are defined in Figures 3 and 4.

  

Figure 3: Completely static types

  

Figure 4: Memoizable types

The predicate static captures the type of completely static values. A completely static value does not refer to any dynamic value whatsoever. We will see later on how the typing rules constrain the derivation of completely static types.

The predicate memo characterizes the type of values which may be memoized. Its use specifies a demand, namely that we want to specialize a function with respect to some value. Such a value must have a memoizable type.

  

Figure 5: Two-level syntax of the subject language

  

Figure 6: Typing Rules for the first-order fragment

  

Figure 7: Typing Rules for functions with fixed arity

  

Figure 8: Typing Rules for variadic functions