[bitc-dev] constraining bitc's type system

[Sam Mason]

On Fri, Sep 15, 2006 at 03:40:57PM -0400, Swaroop Sridhar wrote:
> > 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.

By ``Types'' I'm assuming you mean the actual layout of types in memory.
polyinstantiation of the representation of the types has to happen at
some level, my concern is all the extra code that's being generated.
I must admit that I don't know if generating all of these differently
typed versions of functions is actually bad in practise but it feels
strange that the programmer doesn't have any control over it -- yet has
so much control elsewhere.

> 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

I remember reading these a while back, they are making more sense to me
now but don't seem to help with the profusion of code produced by the
polyinstantiation of functions.

I really think you're going to be stuck with polyinstantiating everything
because there are too many cases to handle.  If everything is going to
be written in BitC that is linked with BitC then this isn't going to be
much of a problem, but once you have to talk to other libraries I think
it's going to get awkward.

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

This is what that rule was about at the end of my email.  If you choose
a few rules now I think you will remove the need for polyinstantiation
of functions (and hence interoperability) while still allowing most
(all of the C style usages I could think of) of the useful instances of
polymorphism in data.

If it doesn't prove powerful enough then put the polyinstantiator for
functions back in.

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

Yes you would, but I'm just not sure when it would be useful to do
something like that.  I very rarely store structures in lists, I almost
always store references to structures (especially with the allocation
is initialisation style of programming) which would be allowed by my
rules and wouldn't require polyinstantiation.

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

Maybe I just like the low level control and the extra memory to store
all these versions and a bit more cache pressure to get them back
seems import.  How much this matters in reality I don't know though.

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

Which was what I was trying to point out.  I'm not sure this is a useful
pattern and if it gets thrown out by the compiler I don't think anybody
will mind.

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

And this will still need to happen at some level, I just think the
majority of this can be mitigated by moving stuff into the safety proofs
and out of the compiler (modulo the extra checks that would be done).

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

I agree that type classes are a different problem and need dictionaries.
But they are under the explicit control of the programmer and this
(in my view) makes it OK.

I'm only suggesting that the specific members that you want to use
polymorphically need to be boxed and if you're not writing completely
generic code not even that restriction need apply.   It's at this point
I realise that it wouldn't be polymorphism any more.  Humm.  I still
think it would be nice to be able to know that specific patterns wouldn't
result in polyinstantiation and so would have more predictable runtime
behaviour and the bonus of being able to interface with external code
without too much work.


  Sam