magic icon indicating copy to clipboard operation
magic copied to clipboard

Published 20 hours ago • verified publisher icon mikera

Dependent types

Open mikera opened this issue 8 years ago • 2 comments

Consider how to extend the type system to dependent types.

mikera avatar May 09 '17 05:05 mikera

Don't bother. As long as you have imperative semantics as opposed to lambda calculus normalization / evaluation in the dependent types predicate system, simplification (creating interior codepaths where all contracts can be proved to have been checked) is the best you're really gonna do. Most naive dependent type systems just preserve all contracts and check all of them all the time. No shame in doing that. Just add a "GuardedType" which has a guard function and call it good.

arrdem avatar May 09 '17 06:05 arrdem

I'm wondering if there is a way to defer this till later. As long as the interfaces/API to the type system allow for dependent types, it could be added later?

mikera avatar May 09 '17 08:05 mikera