12 Nov
2014
12 Nov
'14
10:46 a.m.
On Nov 11, 2014, at 2:06 PM, David Feuer
How (if at all) would you like these term-level natural numbers to relate to the type-level ones?
Not at all. It's my belief that there is exists some moderately remote future (2-3 years) in which all datatypes -- including ones with unboxed fields -- will be promotable. At that point, this new `Natural` will promote, too. That future may also contain overloaded numeric literals in types, in which case things would just work. The only problem would be that this `Natural` doesn't have the right inductive structure to reason about in types, but it's no worse than today's `Nat`s. My work for the next few years is to make that future a reality. :) Richard