[bitc-dev] constraining bitc's type system
swaroop at cs.jhu.edu
Fri Sep 15 14:40:57 CDT 2006
Sam Mason wrote:
> Just been reading though the BitC spec again and trying to understand
> Swaroop's latest mails and noticed that the definition of the "optional"
> union type looks a bit strange. It currently appears as:
> (defunion (optional 'a) :val
> val:(some 'a))
> But I think it's probably:
> (defunion (optional 'a) :val
> (some val:'a))
Yes. Thanks for the correction. Also, val is a keyword and cannot be
used as a field name. So, the correct definition is:
(defunion (optional 'a):val none (some it:'a))
> I'm having a lot of trouble getting my head around the semantics of
> types like "optional" -- i.e. polymorphic value unions. Not sure if
> it's just me or not.
> At the moment I assume this is where the polyinstantiator kicks in.
> I also assume that you don't want the polyinstantiator to be used quite
> as liberally in later versions of BitC, but I'm unsure how this can be
Types are always polyinstantiated, as it does not cost anything at
run-time. That is, (optional bool) will have the representation
| tag | bool |
and (optional (pair int32 int64)) will have the representation:
| tag | int32 | int64 |
If the 'a is specialized to a reference type, we may elide the tag due
to the Cardelli optimization (unless asked not to do so):
| none or |
| ptr ---|------>
The implementation of polymorphic values (including functions) is
currently done by polyinstantiation. But, in the case of polymorphic
functions, later versions of the compiler may employ other techniques
like coercions, dictionaries, or a hybrid of these techniques along with
polyinstantiation. A little more explanation about this can be found at:
Implementing Polymorphism in BitC
> For example in the presence of elided tags, what
> representation gets picked for:
> (define x none)
> id: (forall ('a) (optional 'a))
However, in the case of values like `x' above, we cannot avoid
polyinstantiation ever. If x is later used in the context of different
specializations, they are _different_ `x's.
That is, if we have:
(cons x:(optional int32) nil)
(cons x:(optional bool) nil),
we will have to polyinstantiate x's definition to two different
definitions x#optional_int32, and x#optional_bool and use them
Since `x' is immutable, there is no user-visible change here due to
polyinstantiation. Since function applications are not values, this will
not result in redundant computation.
However, this does result in disparity between user's ``apparent'' view
of the memory model and the actual memory usage, and we are considering
introducing extra constraints in this regard.
> Section 5.4 (Interaction with ``Relaxed'' Value Restriction) of the
> paper Swaroop is writing has the following example:
> (define p:(mutable bool, 'a) (#t, none))
> val p: (mutable bool, (optional 'b))
> (let ((r1:(optional int8) p.snd)
> (r2:(optional double) p.snd)) ... )
> which is a problem because optional is a value type and hence it's size
> is determined by its parameter type.
The main problem here is not the difference in sizes but that we will
require polyinstantiation of a mutable cell, which will alter the
_meaning_ of the program (i.e. which location gets set!ed). Therefore,
we cannot allow it.
> I've just realised another related
> problem, that of finding the location of a structure (or union) member.
> Given the type and function:
> (defstruct (pair 'a 'b)
> a:'a b:'b)
> (defun (fn p):(fn (pair 'a 'b) 'b)
> how does the compiler know the member `b's location. I guess the
> polyinstantiator kicks in again and spews out instances of the function
> where needed.
As I previously noted, polyinstantiation of immutable things are OK, and
functions are the easy case because we can use other techniques (also
noted above) to get the same effect.
> I have a feeling that this is what Garrigue's restriction
> effectively does in BitC, but haven't entirely convinced myself of it yet.
The Garriage restriction (and the Value restriction in general) -- as we
know -- is a way of preserving meaningful sharing (of locations) at the
same maintaining soundness. We had to impose some extra restrictions in
BitC because polyinstantiation happens in units of entire unboxed types,
and thus the ``tainting'' of monomorphism due to mutability propagates
to the enclosing value type.
> The only way I can see out of this is to require polymorphic members
> to be boxed.
> It guess it would be possible to allow functions to pass boxed types
> around with polymorphic members as long as they are treated as opaquely.
This approach is taken by ML, Cyclone, etc. We can also have only one
copy of a function to deal with all (instantiations over) reference
types, but will still need dictionaries to deal with type class instances.
More information about the bitc-dev