[bitc-dev] constraining bitc's type system

[Swaroop Sridhar]

Sam Mason wrote:
> On Mon, Sep 18, 2006 at 04:23:54PM -0400, Swaroop Sridhar wrote:
>> The correct annotation for what you mean is:
>>
>> (define foo:(forall ((refType 'a)) (fn (foo 'a) 'a))
>>     ... )
>>
>> and I think this will achieve what you want.
> 
> The last email was a bit rushed, I'm sorry that it was all so confused.
> 
> Humm, it still looks a bit strange though.  I'm having a lot of trouble
> with the syntax, it was supposed to be something like the following
> Haskell code.
> 

There is a bug in what I wrote.  Also, `fn' is a keyword in BitC, and 
you cannot have a function named fn. Other than that, there is a direct 
direct correspondence to the Haskell code you have written.

>   data Foo a = Foo Bool Int a (Foo a)
> 
>   fn :: RefType z => Foo z -> z
>   fn (Foo x y z p) =
>     if x
>       then fn p
>       else z

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


> I'm still interested in how you will link BitC and C code (or any other
> language's code) as you've probably got much more coherent ideas about
> it than me.  But then again, I guess you'll work it out when you get to
> it and I should just be more patient.

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.

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.

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

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.

Swaroop.