[bitc-dev] `for-all' definitions

[Swaroop Sridhar]

This mail proposes a change in the syntax and semantics of the construct 
used to express type-class constraints in BitC. This syntax was proposed 
by Dr.Shapiro on Monday. The semantics closely follow the Haskell rules 
(I hope). I would appreciate corrections in case any of this is flawed.

-----

I) Remove (member constraints type) construct.

II) Introduce the `forall' form. However, this type-qualification can
occur only in quantified contexts, not at arbitrary type expressions (as 
was the case with the member form).

Specifically the allowed forall forms are:

1) Structure definition:
  (forall constraints
   (defstruct (struct-name tvars) fields))

2) Union definition:
(forall constraints
   (defunion (union-name tvars) fields))

3) Structure and union declarations:

(forall constraints
   (defstruct (struct-name tvars)))

(forall constraints
   (defunion (struct-name tvars)))

1) 2) and 3): The type-variables in `constraints' must be a subset of
                `tvars', otherwise the type is anyway ambiguous.

3) Value definitions:

(forall constraints
   (define pat expr)

The definition is entitled to use the type variables in the 
forall-constraints as well as new type-variables. It is an error if the 
type variables mentioned in the constraints cannot be generalized.

4) Value declarations:

(forall constraints
   (proclaim id type)

   The type is entitled to use the type variables in the 
forall-constraints as well as others. It is an error if the type 
variables mentioned in the constraints cannot be generalized. The type 
mentioned in the declaration must match the definition exactly, 
including *all* typeclass constraints. Otherwise, typing mutually 
recursive functions will be wrong.

5) Typeclass definitions:

(forall constraints-0
    (deftypeclass (tc-name tvars)
  	(tyfn-s)

    (forall constraints-1
	(member-1: type-1))

     ...

    (forall constraints-n
	(member-n: type-n))
)

In this case, I think we can get rid of (super ... ) clause because the 
(forall constraints-0) class can effectively achieve this.

6) Instances:

(forall (constraints)
    (definstance (class-name tvars)) ... )

III) Monomorphism

In keeping with the ML tradition, I think BitC should *not* impose the 
monomorphism restriction[*].

The main concern here is redundant computation. For example: (adapted 
from Haskell-98 report)

If we have a function Length: (forall (Num 'a) (fn (list 'b) 'a))

(define (lenlen x) (let ((len (Length x))) (len, len))
lenlen: (forall (Num 'a, Num 'b) ('a, 'b))

This may result in computation of the length twice, even though it is 
not evident to the programmer. However, my understanding is that this 
cannot alter the semantics of the program because mutation triggers the 
value restriction, and non-mutating functions should be fine.

Regarding concerns about ambiguous types, I think it is reasonable to 
report an error and ask that the programmer instantiate the expression 
to the intended type by providing a type signature, rather than 
monomnorphing it so that it later unifies to that intended type when used.

[*] BitC does not expose monomorphic types. Value-restricted types are 
instantiated to dummy types as in SML.
[*] The general philosophy in BitC has been to try to reduce the 
necessity for explicit type-qualification.


Swaroop.