Dependent Types  

Instead of macros?

Dependent types enable support for compile time execution and code generation. Term-level macros are trivial. Type-level macros are nearly so, but require some splicing help for records, variants, and objects. Module level macros require one simple splicing operator.

Macros often desire call-by-name semantics, so we probably need a way to indicate a call-by-name parameter.

Instead of effects?

It seems like dependent types should be able to subsume the effect system, but I haven't figured out how yet.

There also is a negative here--the effect system is meant to clearly express intent. Encoding it in terms of dependent types may be harmful.

Other benefits

Dependent types have plenty of more pedestrian use cases, like array bounds checking.

Comments powered by Disqus