The Type Language

The language of basic types in MrSpidey is defined as follows:

  
  type is one of:
     set-variable 
     empty 
     zeroary-constructor 
     (constructor type    type) 
     (union type    type) 
     (rec ([set-variable type]   ) type) 
     (class [ivar type]   ) 
     (object [ivar type]   ) 
     function-type 
     type-abbreviation

  set-variable is:
     identifier

  zeroary-constructor is one of:
     nil num sym str char void true false bool eof

  constructor is one of:
     zeroary-constructor 
     vec box promise mvalues iport oport Unary constructors 
     cons                                Binary constructors 
     define-structure-constructor 
     user-defined-constructor

  define-structure-constructor is:
     identifier

  user-defined-constructor is:
     identifier

  function-type is one of:
     (type    type -> type) 
     (type    type *-> type) Rest argument 
     (type    type ->* type) Return value list
     (type    type *->* type) Rest argument and 
                                                           return value list 
     (lambda type type)                                    same as (type *->* type)

  type-abbreviation is one of:
     Abbreviates  
     (MU set-variable type) (rec ([set-variable type]) set-variable) 
     noarg nil 
     (arg type type) (cons type type) 
     (list type    type) (cons type (cons    (cons type nil))) 
     (listof type) (MU l (union (cons type l) nil)) 
     null nil 
     bool (union true false) 
     atom (union nil num sym str char bool) 
     sexp (MU x (union atom (cons x x) (vec x)))

The behavior of primitive operations is defined using multiple-arity schemas. For each reference to a primitive operation, MrSpidey retrieves the corresponding multiple-arity schema and selects the schema appropriate for the number of arguments given to the primitive (or the last schema if the primitive is used in a higher-order manner). It then instantiates the schema by replacing the quantified set variables by set variables, and converts the resulting basic type into a constraint system. Multiple-arity schemas are defined as follows:

  
  multiple-arity-schema is one of:
     schema 
     (case-> schema   )

  schema is one of:
     type 
     (forall (set-variable   ) type)

• Accurate Numeric Operations