When I write Haskell I miss ML modules and eager evaluation. When I write ML I miss the modal distinction between expressions/computations and higher-kinded types. Does such a language (ML modules, eager, modal, higher kinds) exist?
Conversation
Agda has this. It's a much more Haskell-like experience than Coq. You can turn off the termination checker, and it has a pretty good FFI with Haskell or JavaScript.
2
1
7
It actually has true "first class modules" in a sense: since you can open records as modules, you can consume and produce modules in functions
1
3
When I originally posed this question I was imagining languages outside the realm of dependent types, but given the answers I've received (of course biased by my followers) maybe I should be wishing for a general-purpose dependently typed programming language.
3
2
Yeah, a general purpose dependently typed programming language with a high quality module system based on dependent records is something I really want!