[bitc-dev] constraining bitc's type system
swaroop.sridhar at gmail.com
Tue Sep 19 10:52:56 CDT 2006
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))
(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.
(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.
More information about the bitc-dev