Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-25 20:34:11 -0800 (Tue, 25 Jan 2005)
Revision: 6506
Log message:
Ok, I've decided the semi-non-disjoint union scheme is the best.
Currently, sequents in mmc are defined as follows:
declare sequent [sequent_arg]
{ Exp : TyExp
| TyExp : KindExp
| Prop : Prop
>- Prop
} : Judgment
The restriction is that non-context variables cannot have union
types. Of course, it immediately becomes clear that this is not
quite enough (I should have seen this of course).
prim thin 'H :
('ext : sequent { <H>; <J> >- 'C }) -->
sequent { <H>; 'h; <J> >- 'C }
= 'ext
Here the type of 'h is indeed a union, and of course it doesn't
matter.
I still like this version, the source language is very nice.
I believe the solution may be to allow restricted union types.
In the rule above, perhaps 'h can have type (TyExp | KindExp | Prop).
During unification, we can:
- reject if we ever try to unify two non-similar union types.
- try to do something smarter.
Of course, the above rule is missing the binding vars.
It could be written as:
prim thin 'H :
('ext : sequent { <H>; <J> >- 'C }) -->
sequent { <H>; x : 'h; <J> >- 'C }
= 'ext
The question is, what is the type of x? Perhaps we can say that
the type is Term, since we know so little about it.