[bitc-dev] constraining bitc's type system

[Sam Mason]

On Fri, Sep 15, 2006 at 08:09:16PM -0400, Swaroop Sridhar wrote:
> Actually, I think it is not difficult to get what you want even in the 
> existing system. Prof. Shapiro had suggested a while ago that we should 
> have a special typeclass (say refType) to which all reference types 
> belong (that is, the compiler will automatically add relevant 
> instances). Now, you can write:
> 
> (define (f x:(forall ((refType 'a)) 'a) x)
> 
> This will ensure that the polymorphism is constrained to ref-types only, 
> and you can be sure that there will be no polyinstantiation due to the 
> polymorphism of 'a.

I think that would help a lot.  I've been thinking that one of the main
reasons for your current polyinstantiation heavy polymorphism would allow
you to have things like linked lists in the standard library that would
be implemented by normal code and not a messy set of macros that we have
to use in C at the moment.  C's macros would be inlined, but the effect
is about the same.

The main thing I was thinking of originally was being able to have some
sort of structure like:

  (defstruct (foo 'a)
    x:bool
    y:int32
    z:'a
    p:(foo 'a))

and being able to know that if I have a function like:

  (define (fn foo:(forall ((refType 'a)) (foo 'a)))
    (if (foo.x)
        (fn foo.p)
        (foo.z)))

hope that I've got the annotation correct, it's supposed to mean that
the parameter z of foo is a reference type.  I would not expect fn to be
polyinstantiated and is also what I mean by having only the polymorphic
members boxed.  The other types would remain unboxed and available for
use without polyinstantiation of the function.


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.


  Sam