[bitc-dev] define, deftype

[Jonathan S. Shapiro]

We have a number of changes coming in BitC 0.5. This note synopsizes a
discussion with Swaroop today, with subsequent revision following a
discussion with MarkM.

Swaroop and I realized today that we had inadvertently removed the
ability to define recursive datatypes in BitC, and that we wanted that
back. In order to get this, we need some sort of LETREC-like construct
in which the identifiers on the left are unified with the free variables
on the right. We introduced DEFTYPE for this purpose.

We then examined DEFUN and DEFINE and noted that these can be reduced to
a single keyword if we can correctly state the pattern constraints. The
problem is that (a) we must not allow data structures with reference
loops, and (b) [noted by MarkM] we must not allow defining expressions
on the right hand side to be evaluated that rely on the fact that
identifiers on the left hand side are already defined.

The rule for DEFINE is now that DEFINE takes the form:

	(define <pattern> <expression>)

the constraints are:

  1. The expression must pattern match with the pattern.
  2. For each sub-expression that unifies with some
     free variable in the pattern, either
       (a) the expression is a lambda form, or
       (b) no free variable in the expression
           is also free in the pattern.

We decided that LAMBDA values should be overloaded. This restores the
complete equivalence of

  (define f (x) (+ x 1))
  (edfine f (lambda (x) (+ x 1))

Given which, we are hereby removing DEFUN from the language.

We then decided that DEFINE should be LETREC-like. This means that

  (define fact (lambda (x)
                  (cond ((< x 0) (- (fact (- x)))
                        ((= x 0) 1)
                        (#t (fact (- x 1))))))

is legal, because the inner call to 'fact' unifies with the in-progress
definition. However, this introduces the requirement for the DEFINE rule
above that came up in discussion with MarkM.

Finally, we decided to allow DEFINE and DEFTYPE to be used locally in
order to introduce local procedures and types, with the interpretation
that the newly defined symbols exist until the end of the current scope.
For this purpose, BEGIN is considered to introduce a new scope.

Given all of this, it is no longer necessary to have LET, LETREC, or
LET* in the language. We can also remove named let. The form

  (let name ((v1 e1) (v2 e2)) body)

becomes:

  (begin
    (define name (v1, v2) body)
    (name e1 e2))


All in all, this removes a lot of gorp from the language.

Memo to selves: it may be desirable to re-introduce a LOOP syntax of
some sort into the language, purely for the sake of usability.


shap