Swaroop and I have been going back and forth on how to handle literal types.
We want to do this mainly for two reasons:
1. To be able to build generic type classes for operations like LENGTH
2. To handle low-level I/O on arrays
The latter use case is pretty compelling.
My original proposal was to write something like:
(forall ((i:int32))
(define (add-literal-i x:i y)
(+ x y)))
add-literal-i: (forall ((i:int32)) (fn i int32 -> int32))
A more consistent notation would use (forall ((literal 'i int32)) ...), and
I will use that in future.
Given this sort of type, the array type constructor is now typed as:
(forall ((literal 'w word))
(array 'a 'w))
Note that there is a substantive change here. Previously, the array type
constructor required a literal *expression* of type word as its second
argument. Now, it requires a literal *type* as its second argument. This is
consistent with dependent type intuitions, but it leaves us with some
challenges. We would like to be able to write and assign types to things
like:
(lambda (w) (array int32 w))
or:
(array T2 (array-length otherArray))
and these present problems. It is very easy to change the type of
array-length to be
(forall ((literal 'w word))
(fn (array 'a 'w) -> 'w))
but array-length produces a value rather than a type, and the array type
constructor requires a unitary literal type.
LIFTING
Swaroop has proposed that we should resolve this by the following expedient:
Where a literal type is required, an expression producing a value of
compatible literal type may be provided, and the value will be "lifted"
to the corresponding literal type.
At the moment, the only forms I can see where this arises are the vector and
array type constructors and the bitfield type constructors. And the only
part of this that is moderately head-scratching is to explain why (a)
array-length is considered a literal, and (b) an argument of literal type
can be passed to a type constructor.
COPY COMPATIBILITY
A value of type 'w that is constrained by (literal 'w T) may be passed where
a value of type T is expected. That is:
(forall ((literal 'w 'a)) (CopyFromTo 'w 'a))
Note this is not quite the same as copy compatible in the current scheme,
because CopyFromTo is not symmetric. CopyFromTo states that a copy is legal
from the source (here 'w) to the destination (here 'a). It makes no
statement about the legality of copies in the reverse direction. The
current, symmetric (CopyCompat 'a 'b) is equivalent to writing (CopyFromTo
'a 'b) and also (CopyFromTo 'b 'a). That is: CopyFromTo subsumes CopyCompat,
and could now be implemented in the usual way by:
(forall ((CopyFromTo 'a 'b) (CopyFromTo 'b 'a))
(deftypeclass (CopyCompat 'a 'b)))
(definstance (CopyCompat 'a 'b))
As it happens, we were not relying on the symmetry of copy compatibility
anywhere, and the proposal here is to drop the built-in CopyCompat
constraint and replace it with CopyFromTo.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
