2.1 Expressions

A complete specification of BitC expressions is provided in the BitC language specification [11].

2.2 Types

The type ϒτ is referred to in English text as maybe-mutable-τ or simply maybe-τ (interchangeably) in the rest of the document. Collections of such types shall be referred to as ``maybe mutable-types'' or simply ``maybe types'' (interchangeably).

(defstruct (pair 'a 'b):val fst: 'a snd: 'b)
struct pair: (pair 'a 'b)

(defunion (list 'a) nil (cons car:'a cdr:(list 'a)))
union list: (list 'a)

(defunion (optional 'a):val  none (some it:'a))
union optional: (optional 'a)

2.3 Type Expressions

This section introduces some operators that work on types. The meaning and purpose of these operators will become clear in the later sections of the document. All of the following operators have lower precedence than the type-constructors defined in the previous section.

4.1 Definition

When a value is copied onto a new location as the result of a copy operation, the type of the value stored in the new location is only required to be copy compatible with the type of the original value. Therefore, we define ≅ as:

• Ψτ ≅ τ -- shallow top level mutability compatibility.

• arr(Ψτ) ≅ arr(τ) -- since arrays are value types, and the entire array is copied by value.

• ⊖_∘(τ₁^*) ≅ ⊖_∘(τ₂^*) iff τ₁₁^* ≅ τ₂₁^* and τ₁₂^* = τ₂₂^*, where τ₁₁^* ∊τ₁^*, τ₂₁^* ∊τ₂^* are the set of type arguments that are not used within another reference type-constructor, and τ₁₂^* ∊τ₁^*, τ₂₂^* ∊τ₂^* are the rest of the type arguments.

  The mutability at the fields of structures and unions are determined by their corresponding definitions. However, we do have some freedom with the compatibility of the type-arguments of value structures and unions. For example: ⊗_∘^pair(τ₁,  τ₂) ≅ ⊗_∘^pair(Ψτ₁,  τ₂) ≅ ⊗_∘^pair(τ₁,  Ψτ₂) ≅ ⊗_∘^pair(Ψτ₁,  Ψτ₂). However, we cannot allow copy compatibility if the type-argument is used anywhere in the definition within another reference type. For example, for the following structure,

  (defstruct (St 'a 'b):val f1:'a f2:(vector 'b))
  struct St: (St 'a 'b)

  Two values whose types are parametrized over this structure are copy compatible if and only if their first type-arguments (that satisfy 'a above) are copy compatible and the second type-arguments (that satisfy 'b above) are strictly compatible.

4.2 Application

In theory, it is sufficient to require (only) copy compatibility at:

• A new binding.

• The argument and return positions of any expression that does not (respectively) expect or return a location.

The value returned by an expression returning a non-location will will invariably end up in an expression that does not expect a location, and will thus (in turn) invoke the copy compatibility rule. The main reason to allow copy compatibility here is to allow explicit type-qualification of the return values of applications with a different but copy compatible type. For example:

(define (id x) x)
val id:(fn ('a) 'a)

(define xyz (id 10:int32):(mutable int32))
val xyz: int32 

5.1 Unification

This section provides the algorithm for type unification in the presence of copy compatibility. The Unify() function will either fail with an error (⊥), or will succeed with a set of linkages of the unified types. These unification linkages are denoted by τ₁ ↪ τ₂, which can be understood to mean ``τ₁ resolves to τ₂ due to unification.''

All Unification rules are commutative. The unification linkages are just a mechanism of accumulating equality constraints among types. They are represented as (uni-directional) linkages so that it is easy to visualize the type obtained as the result of unification by just following the unification links. Moreover, we don't have to solve any equality constraints after unification -- they are instead ``solved'' incrementally, each time we form a linkage. If the set of linkages obtained as the result of unification has two linkages τ₁ ↪ τ₂ and τ₁ ↪ τ₃ where τ₂ ≠ τ₃ it is a contradiction, and hence a type error².

Note the order and manner in which maybe types are handled. Two types ϒτ₁ and ϒτ₂ must be linked even after τ₁ and τ₂ have unified, in order to ensure that their mutability also resolves the same way. Otherwise, all we have said is that the inner types must be strictly equal, and we might (due to further unification) end up in a situation where we infer Ψτ ↪ τ or τ ↪ Ψτ. We can, if we prefer, introduce such linkages for all other types as well. The mutability wrappers must be processed even before type-variable linkages are processed. Otherwise, we can end up having types like ϒΨτ, that is, (maybe (mutable τ)), which can later ``legally'' form the type (immutable (mutable τ)), which is a contradiction.

If the type of the lvalue argument of a set! has type ϒτ, we will infer the constraint (rather, the linkage) ϒτ ↪ Ψτ.

We will now define a function UnifiedType(), that unifies two types, and returns the final type obtained as the result of unification. That is, it returns the type obtained by transitively following linkages produced as a result of unification, or returns ⊥ if unification fails.

and

All functions that operate on types (including the Unifier itself)³ shall be understood to operate on types that are obtained after all unification linkages are followed. That is, f(τ) is a shorthand for f(τ, ℒ), wherein the first rule of the function is:

These details are not shown in subsequent functions in the interest of brevity. Also, the operation on constrained types is not explicitely shown. Application (of a function) on a constrained type is the same as applying the function on the unconstrained type, because following unification linkages will have the effect of performing resultant substitutions in the constraint set as well.

5.2 An Example

In this section, we illustrate our inference mechanism with the help of an example. Consider the following definition:

(define p:(pair (mutable int32) bool) 
  (pair (the int32 1) #t))
val p:(pair (mutable int32) bool)

In order to illustrate the types obtained after every step of inference, we will annotate this expression with [numbers] and then indicate the unification performed (if any) and the type obtained at each step. The annotations that use quoted numbers as in [n'] indicate the type inferred for the copy of the value at the corresponding unquoted annotation [n].

[12](define [6] [1]p: [5](pair [3](mutable [2]int32) [4]bool) 
        [11'] [11](pair [9'] [9](the [8]int32 [7]1) [10'] [10]#t))

[1] = α
[2] = int32
[3] = Ψint32
[4] = bool
[5] = ⊗_∘^pair(Ψint32,  bool)
[6] = UnifiedType([1], [5]) = ⊗_∘^pair(Ψint32,  bool)
[7] = β \ {IntLit(β)}
[8] = int32
[9] = UnifiedType([7], [8]) = int32
[9'] = ϒint32
[10] = bool
[10'] = ϒbool
[11] = ⊗_∘^pair(ϒint32,  ϒbool)
[11'] = ϒ⊗_∘^pair(ϒint32,  ϒbool)
[12] = UnifiedType([6], [11']) = ⊗_∘^pair(Ψint32,  bool)

5.3 Principality of Inferred Types

The main idea of maybe types is to keep the mutability status of types ``open'' to further unification, and thus infer most-general (or principal) types at every step of inference. However, at a let-boundary<sup>4</sup>, it is no longer possible to keep the mutability status of types ``open'' to further unification --- at least in the case of universally quantified types --- due to the value-restriction [12]. That is, in the case of the expression:

(let ((p nil)) ... )

we cannot give p the type: ∀α.ϒ⊕_⋆^list(α) due to the value restriction. We can either give p the polymorphic type ∀α.⊕_⋆^list(α), or the monomorphic type ϒ⊕_⋆^list(α). That is, in this system, there is no principal type that we can infer for p. Given this, we must ``default'' these maybe types to either mutable or immutable at a let-boundary. In the next section, we will identify some choices for defaulting these maybe types, and discuss their merits and limitations.

In contrast, ML infers principal types⁵ although it does not infer principal typings[6]. In order to achieve principality of inferred types, ML imposes the restriction that only references can be mutated, and all references must be mutable. This leaves the inference engine with exactly one choice (of the type to infer) when it looks at an expression. In BitC, we trade principality of inferred types in preference to a more expressive language (and type system). Section 5.5 deals with the various issues that arise due to this non-principality of inferred types.

It might be useful to note that this is not the only case in which we run into the non-principality problem in BitC. We do not infer structure types automatically from the field labels in the case of expressions like

s.fld
      

We cannot infer the type of s because, in BitC, we do not require field labels to be unique. So there is no principal type we can infer for the above expression, and it fails to type check. This problem is similar to SML's record selection using the # operator.

5.4 Interaction with ``Relaxed'' Value Restriction

In BitC, we adopt the relaxed Value Restriction proposed by Jacques Garrigue[1], which states that even in an expansive expression, type variables that occur purely in non-contravariant (non-argument) positions can be generalized. More formally, this means that, in an expansive expression e with type τ, the generalizable type variables are given by:

where:

However, in a language that has unboxed mutability and unboxed composite values, this restriction turns out to be insufficient to ensure soundness. For example:

(define p:(mutable bool, 'a) (#t, none))
val p: (mutable bool, (optional 'b)) ??

According to the above algorithm, we see that the value constructor none has the type ⊕_∘^optional(α), and the type variable α occurs in non-contravariant position, and can thus be generalized. Now, if we give p the type ∀α.⊗_∘^pair(Ψbool,  ⊕_∘^optional(α)), we can then write:

        
(let ((r1:(optional int8) p.snd)
       (r2:(optional double) p.snd)) ... )

which is clearly not OK because r1 and r2 have different sizes and this requires the polyinstantiation p.snd and thus its container p, which has other mutable components. Therefore, we cannot give p a polymorphic type here. In Section 6.1.3, we will describe a revised version of Garrigue's restriction, that is sound in the presence of composite value types. The idea is to make the value restriction propagate to enclosing container type until we reach a ref-boundary.

In SML, all type variables in expansive expressions are monomorphed. While this will solve our problem, we did not adopt this solution because we wanted to preserve as much polymorphism as possible (especially in the case of reference types). Many use cases for adapting the relaxed restriction including the need for polymorphism in accessor functions can be found in [1]. Cyclone solves this problem by imposing a stricter rule (rather reminiscent of Haskell's monomorphism restriction[3]) that only functions are given polymorphic types[2]. This is a reasonable thing to do in cyclone where most values are mutable, and where there is a distinction between functions and function values, but, is too restrictive for our purposes.

5.5 Inference Trade Offs

As we have seen in the previous section, we introduced maybe types in order to provide freedom of copy compatibility. However, in doing so, we ``lost'' precise mutability information about these types. This, combined with the fact that we must default these maybe types at a let-boundary, can result in inferred types that are quite surprising to the programmer. In this section we will consider the various issues in the trade-off between freedom and precision. In an ideal scheme, we should have:

• Soundness: The inferred types must be correct.

• Completeness: It should be possible to infer all possible sound types, albeit with qualifications.

• Less programmer annotations: The inference must be useful, and must not require excessive annotations in the ``common case.'' Since the ``common case'' is a subjective usability issue, we can approximate this to say: ``it must retain as much available information as possible.''

• Contained mutability: The inference engine must not infer mutable types in ways that are ``too surprising'' to the user. From the standpoint of good programming practice, this might be stated as ``mutability should not be promiscuously inferred.''

(let ((p (pair n:(mutable int32) (lambda (x) x)))
      (q #f)) body)
[Intermediate] p: (maybe (pair (maybe int32) (maybe (fn ('a) 'a))))
[Intermediate] q: (maybe bool)

(define (mut-c c) (set! c #\a) c)

(proclaim mut-c: (fn (char) char))

(define mut-c:(fn (char) char) (lambda (c) (set! c #\a) c)

(defstruct St fnxn: (fn (char) char))

(define xyz (St mut-c)

(deftypeclass (CL1 'a)
  fn1: (fn ('a) 'a))

(definstance (CL1 bool) 
  (lambda (x:bool) x))
(definstance (CL1 (mutable bool)) 
  (lambda (x:(mutable bool)) x))

(deftypeclass (CL2 'a)
  fn1: (fn ((vector 'a)) 'a))

(definstance (CL2 bool) 
  (lambda (x) (vector-nth x 0)))

(definstance (CL2 (mutable bool)) 
  (lambda (x) (vector-nth x 0)))

6.1 Formalization

(let (([1]p:[2]qual [3]expr)) body)

6.2 Some Examples

In this section, we will illustrate our scheme with some examples.

 
(define xyz:(mutable int32) 10)
val xyz:(mutable int32)

(define p:(mutable 'a) (pair xyz #t))
val p: (mutable (pair (mutable int32) bool))

Inn the above example, xyz clearly has the type Ψint32. Here is the annotated expression for the definition of p followed by the types inferred at at every step of inference:

 
[10] [9] [8](define [4]  [1]p:[3](mutable [2]'a) 
      [7'] [7](pair [5'] [5]xyz [6'] [6]#t))

Here are the types obtained after each step of inference:

In the rest of the examples, we will only show the expressions and the final type obtained. In the following expression:

(define r (vector (cons mTrue:(mutable bool) nil)))
val r: (vector (list (mutable bool)))

r gets the ``expected'' type vec(⊕_⋆^list(Ψbool)). However, it is still possible to get the type vec(⊕_⋆^list(bool)). for r through explicit qualification if one desires so.

(define r:(vector (list bool)) 
  (vector (cons mTrue:(mutable bool) nil)))
val r: (vector (list bool))

Finally, our list->vector also gets the ``correct'' type, without any type qualifications.

(import ls bitc.list)
(define (list->vector lst)
  (make-vector (length lst) 
    (lambda (n) (ls.list-nth lst n))))
val list->vector: (fn ((list 'a)) (vector 'a))

The type inferred for list->vector is ⊕_⋆^list(α) → vec(α), as is apparent from the definition, and not ⊕_⋆^list(α) → vec(β) \ {α ≅ β}.

We will now give some examples that illustrate our value-restriction scheme. In these examples, we will explicitly write the universal quantification of type variables in the case of polymorphic types. First, the example we considered in Section 5.4:

(define p:(mutable bool, 'a) (#t, none))
val p: (pair (mutable bool) (optional #X255))

is now well typed, because p is now given the non-polymorphic type ⊗_∘^pair(Ψbool,  ⊕_∘^optional(#X₂₅₅))⁸ and not ∀α.⊗_∘^pair(Ψbool,  ⊕_∘^optional(α)).

All the permissible cases in original (Garrigue) restriction are still preserved for reference types :

(define q:(mutable bool, (list 'a)) (#t, nil))
val q: (pair (mutable bool) (list 'a))

q: ∀α.⊗_∘^pair(Ψbool,  ⊕_⋆^list(α))

Type-variables wrapped in a reference type are OK even if they lie within an encompassing value type.

(define r:(mutable bool, 'c) (#t, (nil, nil)))
val r: (pair (mutable bool) (pair (list 'a) (list 'b)))

Type-variables wrapped in a value type must be removed even if they lie within an encompassing reference type.

(define m:(mutable bool, 'b) (#t, (vector none)))
val m: (pair (mutable bool) (vector (optional #X143)))

Otherwise, one could write:

(let ((mm1:(optional int8) (vector-nth m.snd 0))
      (mm2:(optional double) (vector-nth m.snd 0))) ... )

Accessor-like functions will work OK for reference types but will not work for value types.

(define (car x:(list 'a)) ... )
val car: (fn ((list 'a)) 'a)

(define fstElem (car (cons nil nil))
fstElem: (list 'a)

(define (fst x:('a, 'b)) x.fst)
val fst: (fn ((pair 'a 'b)) 'a)

(define fstPart: (fst (nil, nil))
val fstPart: (list #X432)

The right thing to do in this case is to define fst as a term and not as an ordinary functions whose application will be considered expansive.

6.3 Limitations

The algorithm proposed above is not a panacea. First, there is a peculiar kind of generality we have lost, which is impossible to recover even with explicit qualification (that is, with the facilities for qualification present in the current language specification). For example, there is no qualification for list->vector that we can use, in order to obtain the type ⊕_⋆^list(α) → vec(β) \ {α ≅ β}. That is, even if we re-write the definition as

(import ls bitc.list)
(define list->vector:(forall ((copy-compat 'a 'b)) (fn ((list 'a)) (vector 'b)))
  (lambda (lst)
    (make-vector (length lst) 
      (lambda (n) (ls.list-nth lst n)))))
val list->vector: (fn ((list 'a)) (vector 'a)))

we obtain the type ⊕_⋆^list(α) → vec(α) for list->vector according to the above algorithm since a statement copy compatibility does not preclude equlity.

6.4 Future Considerations

Function types can be generalized regardless of whether they contain any mutable or maybe types within them. Therefore, if an expression is a value (that is, not expansive), there is no reason to fix the maybe types contained within a function type in order to retain soundness or polymorphism. This way, we can retain the principality of types for functions definitions. This approach will --- among other things --- resolve the problem with the type of list->vector identified in the previous section.

(import ls bitc.list)
(define (list->vector lst)
  (make-vector (length lst) 
    (lambda (n) (ls.list-nth lst n)))))
val list->vector: (forall ((copy-compat 'a 'b)) (fn ((list 'a)) (vector 'b)))

The type of list->vector will now be ∀α.β\⊕_⋆^list(α) → vec([[β,  α]]) \ {α ≅ β}. That is, we obtain the fully generic type for list->vector, but also save a hint to resolve the types at use occurrences. Therefore, any use of list->vector will yield ``expected'' types, as in:

(define (lvm lst:(list (mutable bool))) (list->vector lst))
val lvm: (fn ((list (mutable bool))) (vector (mutable bool))) 

There is a further relaxation to the way we fix maybe types that can be considered. Whereas we need to fix the maybe-ness in the type itself, we may not have to fix the maybe-ness of the constraints on the type, in order to retain sound typing. This will facilitate cases like:

 
(deftypeclass (CL2 'a)
   zeroth: (fn ((vector 'a)) 'a))

(definstance (CL2 bool) 
  (lambda (x) (vector-nth x 0)))

(define p:(vector (mutable bool)) (vector (zeroth (vector #t))))
val p:(vector (mutable bool)) 

to type-check even though there is no instance CL2(Ψbool) because, for p, we initially obtain the type vec(Ψbool) \ {CL2([[ϒbool,  bool]])}⁹, and the constraint CL2([[ϒbool,  bool]]) can be satisfied by the instance CL2(bool), and we finally get the unconstrained type vec(Ψbool).