As the unofficial bibliography for this list, I'll just point out Barry Jay's past work on shape theory:
http://www-staff.it.uts.edu.au/~cbj/Publications/shapes.html He's looked at many of the questions surrounding shape polymorphism and the impact shapes have on compilation. While the breadth of subjects I've read about is disgusting, it's tougher to remember enough depth to be of real help given life constraints! I'll settle for helpful pointers when that's all I can afford. ;-) Sandro On 16/04/2012 7:49 PM, Jonathan S. Shapiro wrote: > This is an idea that I never got around to implementing, but I sort of > think is important. It's also pretty half-baked. > > I came to it from a simple question: How do we know when two instances > of something like List('a) are free to use the same underlying > implementation? The answer seems obvious enough: the same implementation > can be used for List('a) and List('b) when the types 'a and 'b have the > same size. This is true because lists handle their element types in a > very opaque way. What we would like is a way to describe this > semi-opaqueness. > > To view this another way, the type of a "CopyWord" operation in a VM can > *almost* be described as: > > HasSizeAndAlign('t, 4, 4) => > CopyWord(ref mutable 't, ref 't) > > > Except that we have dropped something here. CopyWord must ensure type > /agreement/, but it doesn't care what the type actually /is/ from an > operator point of view. Any type, so long as it is a four byte type at a > four byte alignment, can use the same _implementation_ of CopyWord. We > do not mean here: > > for ALL instantiations of 't meeting the constraints, this > parameterized function has an instantiation of 't that is the right > one to use. > > > We mean, instead: > > for EVERY instantiation of 't meeting the constraints, this function > IS the instantiation to use, REGARDLESS of the concrete > instantiation of 't > > > In effect, I'm trying to capture what is happening at the erasure > boundary, where we drop down to untyped machine instructions. The > distinction between FORALL('a) and EVERY('a) is that we don't need to > instantiate over 'a if we already have an instantiation where the other > constraints have been satisfied. > > This isn't existential type, because we need to know what the type is in > order to discharge the constraints. > > So in this (notional) view, the typing of List('a) becomes something like: > > union List('a) { > cons: { car: 'a; cdr: List('a) } > nil > } > every('a), HasSizeAndAlign('a, 'size::nat, 'align::nat) => List('a) > > > The intuition here is that instantiation is going to be driven by the > [implicit] forall on 'size and 'align, rather than being driven by the > 'a. In consequence, if you discover an instance with matching concrete > types for the 'size and 'align (note the clever/tricky use of the Nat > kind here), you are free to use that one. > > Please do not take me to school yet on the notation. I freely concede > that it stinks. As usual, the /absence/ of an every('a) marker means > that the type variable is universally quantified. > > > Now the interesting part of this (maybe) is the subsumption rules. In > particular: forall('a) subsumes every('a). So when we unify the > constraints in something like > > def list_sum(l) : Word > let list_sum_help(accumulator, l) > switch( cell = list ) { > nil: { accumulator } > else { list_sum_help(cell.cdr, 1 + accumulator) } > in > list_sum_help(0, l) > > > we would initially get: > > every('a), all('a), > HasSizeAndAlign('a, 'size::nat, 'align::nat), Arith('a) => list_sum: > 'a -> Word > > > but: > > * all('a) implies a requirement for concrete instantiation, therefore > subsumes every('a) > * concrete('a) implies known size and alignment, subsuming > HasSizeAndAlign('a, 'size::nat, 'align::nat) > > and that leaves us back with the expected type: > > Arith('a) => list_sum: 'a -> Word > > > This intuition, I believe, has straightforward extension to type > preservation when emitting untyped machine code, and also (in a > different way) to typing in the fragile base class problem. > > > shap > > > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
