Open zhangyuanlin opened 6 years ago
I've always felt that the restriction was arbitrary and interferes with reuse.
Scenario: sort A is populated by "normal" instances. sort B extends sort A with some additional state that documents "abnormal" instances of A. I should not have to create a subsort of A that holds the instances that are not in B.
May we can summarize the assumption behind the decisions as
I think it also draws forward the philosophical debate over using sets vs. categories as a foundation of mathematics. I have a tendency to see sorts more as kinds and categories than sets.
currently constants and instances are only allowed for source sorts.
An alternative is to allow constants and instances for non-source sorts. These constants/instances are taken as not in any of its descendent sorts.
Current Monkey banana program from ALM paper uses non-source sorts in defining constants and instances. They bugs by 1, but they are ok by 2.