[bitc-dev] constraining bitc's type system

[Jonathan S. Shapiro]

On Fri, 2006-09-15 at 16:12 +0100, Sam Mason wrote:
> Hi,
> 
> 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. That is a bug in the example. Thanks!

> 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.  For example in the presence of elided tags, what
> representation gets picked for:
> 
>   (define x none)
>   id: (forall ('a) (optional 'a))
> 
> 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.

This type is not mutable, therefore polymorphic. The polyinstantiator
will end up instantiating it once per type. If you try to think of it as
template expansion you'll end up with the right understanding.

I do not expect that we will be able to restrict polyinstantiation for
value types. Carrying dictionary pointers introduces a hidden
performance cost, and for systems programs that should not happen
without the programmer knowing about it explicitly.

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

Actually, in this case the size isn't a problem, because you only copy
the fields that are in the active leg.

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

Yes.

> The only way I can see out of this is to require polymorphic members
> to be boxed.  I have a feeling that this is what Garrigue's restriction
> effectively does in BitC, but haven't entirely convinced myself of it yet.
> 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.

No no. This is precisely what must NOT happen. What needs to happen is
for the polyinstantiator to kick in.

> I hope that makes sense and is somewhat useful.

Good questions, and definitely useful!


shap