search

mikera / magic

Experimental typed JVM Lisp inspired by Clojure
Eclipse Public License 1.0
32 stars 2 forks source link

Dependent types #6

Open mikera opened 7 years ago

mikera commented 7 years ago

Consider how to extend the type system to dependent types.

arrdem commented 7 years ago

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.

mikera commented 7 years ago

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?