[bitc-dev] constraining bitc's type system

[Sam Mason]

On Tue, Sep 19, 2006 at 11:52:56AM -0400, Swaroop Sridhar wrote:
> (defstruct (Foo 'a) b:bol i:int32 z:'a p:(Foo 'a))
> 
> (define fnxn:(forall ((refType 'a)) (fn (Foo 'a) 'a))
>    (lambda (fooVal)
>       (if fooVal.b (fnxn fooVal.p) (fooVal.z))))
> 
> Hopefully, I got it right this time.

Yes, that looks much closer to what I was expecting.  I don't see a
reason to require polyinstantiation of this function, for reasons I try
and explain below.

> Here is what we have as of now:
> 
> i) For non-polymorphic values (functions or otherwise), we can declare 
> an external name for the definition or declaration.
> 
> ex:
> 
> (proclaim extFnxn: (fn (bool) bool) external "EXTFN")
> 
> The outside provider must just supply the function EXTFN in order to 
> link with this code.

Do you mean polymorphic, or polyinstantiated or any other technique
like dictionary passing that requires the compiler to do things in the
background that the programmer didn't directly ask for?

For example, I think it would be safe to have an external identity
function that worked for references:

  (proclaim extid:(forall ((refType 'a)) (fn 'a 'a)) external "EXTID")

This pattern is used extensively in existing libraries for passing
arguments to callback functions -- qsort for example.  Even malloc could
be given a type like this, in practise malloc probably wouldn't be used
as it's not safe but I'm sure you get the idea.

It feels nicer to give these functions a more accurate type, but I'm
not sure how useful it is in practise.

> The fact that the procedure was marked external does not preclude the 
> definition to be written in BitC. It just causes the C-emitter to emit 
> the definition to be emitted with that external name. So, C functions 
> can just use this definition with that name.

Not sure if this is the intention, but this implies that the "external"
flag could also be used for writing libraries in BitC and calling them
from C.

How you get everything into the right state, exception handlers spring
to mind, for this to work seems difficult.

> ii) For polymorphic definitions, we get into name mangling issues, 
> because -- in general -- a definition must be polyinstantiated, and all 
> relevant instantiations must be supplied, (or, the appropriate 
> instantiation must be used by outside code).

My current thinking is that you only need to check up to polymorphic
references to be safe.  I'm probably only thinking about my use cases,
but as far as I can tell it's safe and the "external" flag can be
honoured when a function is monomorphic up to references, otherwise an
error is generated.

I think the same technique can be applied to data as well (can definitions
be anything apart from a function or data?) -- I'm having trouble with
the terminology to describe it, but I'll try.

A structure containing a reference to a polymorphic type doesn't
sound very useful and I'm not sure if it's even possible to define one.
Unions having polymorphic references imply either the same as a structure
or that the chosen leg doesn't imply any specific type for the variable.
If the definition is immutable (functions seem to trivially fulfil this
requirement) then things seem to be OK.

> There is a mode in BitC compiler called ``header mode,'' in which we 
> only output the types and declarations of values for use by external 
> providers/users. Thus, the C code will have to use this header and 
> provide/use the appropriate definitions.

Sounds useful.


  Sam