1.1 Typed language philosophy

In this document we refer to the standard Scheme language defined by the R6RS specifications as the standard language; we refer to the typed Scheme language defined by Vicare as the typed language.

To understand how Vicare represents the types of values, we must remember that every Scheme expression might return multiple values; so we can think of an expression evaluation as follows:

(call-with-values
     (lambda () ?epxr)
  (lambda ?formals ?body))

the return values of ?expr are bound to the ?formals and used in the ?body. For example, in the code:

(call-with-values
     (lambda () (values 1 2 3))
  (lambda (a b c) ?body))

while the expansion of ?body takes place: a typed language would annotate the syntactic bindings a, b and c with the information that the values are fixnums.

The tuple of type annotations associated to the ?formals is called type signature; a type signature represents informations about both the number of values and their type. We need a type signature to represent the types of values returned by an expression. We need a type signature to represent the types of the arguments accepted in a function application.

Given the call-with-values model of thinking to expressions evaluations: the whole purpose of a typed language is to verify, at expand–time, that the type signature of an expression matches the type signature of the arguments of a function.

The standard language already mandates that the operands in a function application must be validated at run–time; this means the type signature of the operands is matched, at run–time, with the type signature of the arguments. The typed language extends this feature to make it possible at expand–time.

Type annotations are not mandatory in the typed language, so some operands are validated and others are not.

To understand the role of Vicare’s typed language extensions, we have to consider that:

• Standard Scheme is dynamically typed: language implementations might perform application signatures validation at run–time every time a function is called, considering that the return values of a function application are discarded or become the arguments of another function application. For example the function flsin can be implemented as:

  #!r6rs
  (import (except (rnrs (6))
                  flsin)
    (vicare system $flonums))
  
  (define (flsin x)
    (assert (flonum? x))
    ($flsin x))
  

• It is possible to build a standard Scheme language implementation that performs compile–time type inference; with such implementation: occasionally the compiler can determine the type of operands and return values and collapse multiple validations into a single one. For example:

  #!r6rs
  (import (rnrs (6)))
  
  (define (flsomething x)
    (values (flsin x) (flcos x) (fltan x)))
  

  can be transformed into (pseudo–code):

  #!r6rs
  (import (rnrs (6))
    (vicare system $flonums))
  
  (define (flsomething x)
    (assert (flonum? x))
    (values ($flsin x) ($flcos x) ($fltan x)))
  

  or automatically defined safe and unsafe variants of the same function:

  #!r6rs
  (import (rnrs (6))
    (vicare system $flonums))
  
  (define (flsomething x)
    (assert (flonum? x))
    ($flsomething x))
  
  (define ($flsomething x)
    (values ($flsin x) ($flcos x) ($fltan x)))
  

  so that the unsafe $flsomething can be used later in place of the safe flsomething if we know that the argument is a flonum.

• The evaluation of a Scheme language program or library is defined to have two steps: expansion; compilation–and–evaluation or interpretation. Standard Scheme is a “high–level language” which is transformed into a “core language” by the process of expansion; the expander allows macros to implement customised high–level transformations. The core language expressions are handed to the compiler or the interpreter.
• Type inference does not blend well with standard Scheme macro expansion; it is, in general, impossible to infer the types of a macro use before fully expanding it, or, in special cases, at least partially expanding it. True type inference can be performed on the core language that is the result of fully expanding the standard language. This means we cannot integrate the powerful features of the expander in the code resulting from transformations made possible by type inference.
• Vicare is a language dialect whose purpose is to be a standard Scheme language with extensions; it allows mixed use of standard language syntax and extended language syntax. The language extensions are mostly implemented in the expander, to allow user code to customise the generation of core language.
• By explicitly specifying the types of lexical bindings: Vicare’s dialect allows some of the expand–time validations and transformations that would be possible in a language with full type inference.

Since there is no type inference: the code writer is invited to explicitly add type annotations to the syntaxes that establish syntactic bindings.