[bitc-dev] constraining bitc's type system

[Sam Mason]

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.

  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

looking at it now it probably needs some termination, but that's roughly
what my code before was supposed to do.  I was expecting this function
to be instantiated just once, but I'm not sure how much this sort of
thing would actually be used in practise.

> > I think that the sort of algorithms you are thinking about though are
> > the more generic containers that don't work very nicely in C without lots
> > of type casting.
> 
> I am a little confused about this paragraph. Are you talking about the C 
> code emitted by the compiler? Or, are you saying that this cannot 
> otherwise be done from C ? Or, are you concerned about linking C code 
> with instantiated procedures?

It would be tedious to write the sort of code natively in C that the
polymorphism in BitC allows you to.  It's obvious now, but before I
wrote the above paragraph I was still thinking in C mode and couldn't
see why you would need the polymorphism all the way down to value types.

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.


  Sam