Pal sent this to me privately, but it belongs on the list.
From: Pal-Kristian Engstad
Date: Thu, 16 Oct 2008 16:47:08 -0700
Hi,
I think it is a wise choice. Single-chained inheritance brings with it a
lot of baggage that you have to solve. What to do about
contra-/co-variance? What to do about differentiation of class type and
value types. And so on, and so on.
For me, sub-typing really only comes to play looking at array bounds. It
would be nice to be able to infer that an array with 256 elements is
safe to access using a U8 type. And to know that the result of clamp(x,
0, array.size) is a safe index into an array. It would be nice to know
that if you have an enumeration enum Idx { first, second, third }, that
an array with three elements indexed over this enum would always be safe.
If you toss out inheritance, then you would probably have to look into
existential quantifiers again, perhaps?
Thanks,
PKE.
Jonathan S. Shapiro wrote:
> For some time now, I have been saying that we intended to do subtypes,
> primarily to support some single inheritance patterns. It is now clear
> that this isn't going to work. In this note I'm going to explain why and
> in the next note I'm going to try to explain what we have in mind to do
> instead.
>
> The problem, in brief, is that subtypes and union types do not get
> along. Type classes are a form of union types[*]. To avoid confusion
> with DEFUNION I'm going to write these as A|B meaning "either type A or
> type B".
>
> [*] This is confusing. The DEFUNION construct creates something that
> is referred to in the type literature as a sum type. DEFTYPECLASS
> constructs something that is referred to in the type literature as
> a union type. Confused yet?
>
> To see why this is a problem, consider a situation where we have:
>
>
> (forall ((some-constraint 'b))
> (define (eager-if tst thn:'a els:'b)
> (if tst thn els):'c))
>
> then we would get the constraints:
>
> 'b <= 'c
> 'a <= 'c
> (some-constraint 'b)
>
> and these do not simplify. Actually, there seem to be a lot of subtype
> cases that do not simplify, but the interaction between "some T1 that
> must be a subtype of T" with "something that must be admissible under
> constraint (some-constraint T1)" can get very awkward very quickly.
>
> Mathematically there is no problem with any of this; in fact, it's
> straightforward. Pragmatically, the result is altogether illegible.
>
> As we poked at this today we became progressively more unhappy, until
> finally we asked ourselves whether this was really a good idea and why
> we needed it at all.
>
> Answers: (a) it's really NOT a good idea
> (b) it doesn't look like we need it.
>
> 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
