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
