[bitc-dev] constraining bitc's type system

[Swaroop Sridhar]

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
>     none
>     val:(some 'a))
> 
> But I think it's probably:
> 
>   (defunion (optional 'a) :val
>     none
>     (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
> reconciled.

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
http://www.coyotos.org/pipermail/bitc-dev/2006-July/000746.html

> 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 
appropriately.

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)
>     p.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.

Swaroop.