3 ms·
I've always dreamed about ML language with verification support and dependent types. Does it have something like Haskell's typeclasses or OCaml's modular implic
by ernst_klim 9y ago
I've always dreamed about ML language with verification support and dependent types. Does it have something like Haskell's typeclasses or OCaml's modular implicits? Does it support ad-hoc polymorphism in any way?
- lmm 9y agoWhat do you think of Idris?
- olzd 9y agoIdris certainly is nice but I doubt anyone uses it for real stuff.
- hiker 9y agoLean is quite nice dependently typed language https://leanprover.github.io/ https://leanprover.github.io/
- saosebastiao 9y agoIt's not intending to be a general purpose language, and as such doesn't have a lot of features that make software engineering easier. In fact, it intentionally has a phenomenally slow compiler, because the compiler is solving or attempting to solve various NP-Complete problems simultaneously. Think of it as a language that will help build tools, analyzers, and possibly linkable libraries for small scale but highly security-critical components, but not necessarily the language you want to use to build an app server.
- platz 9y agoalthough, if you don't use any refinement types in your program, i don't see why you can't write general purpose programs and extract code to Ocaml and F#