On Tue, Apr 7, 2015 at 3:30 AM, Keean Schupke <[email protected]> wrote: > I got more responses about my use of the term "type" for type - level - > objects (and wanting to stratify types), than I did about an actual working > implementation of type inference for arity-aware typing :-)
Well personally, I find it hard to stay on top of what your code is supposed to be doing, since you started it back when you were thinking about arity specialization in terms of subtyping, but now you seem to agree that we should use something like callvars. Also, it's just a type checker, right? Not also an evaluator. So there's no way to even test (let alone prove) the soundness of the type system through your implementation. If that's true, then implementing a type checker kind of seems to be jumping the gun. As far as "type" vs. "type-level object", I still don't know whether that's a weird philosophy of yours, or due to a misunderstanding somewhere. But as long as you can use the same terms as everyone else, there's no need to discuss it further. And for "stratifying" types, I assume you mean the Bool' = True | False Bool'' = True' | False' business. There may actually be a lesson there yet for practical programming languages. Namely, whether stratified vs. dependent type systems are actually more appropriate for programming. This question is complicated by the many styles of system that get called "dependent". BitC is tentatively a stratified system. For now, it seems to me that a dependent type system for BitC could totally be made that's workable, but it may not be worth it. Having something *as strong as if* there were a dependent type system, but with a less systems-y term language for type level, seems ideal. This would be kind of a combination of stratified and dependent, with exactly two "levels", where the type level is a dependent type system. Perhaps this combination should be called a "dependent kind system"? (You know, 'cause kinds can depend on type-level terms?) I'd like to pick up parts of our old discussion off-list, to see if we can learn something about stratified vs. dependent type systems. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
