There are two interesting extremes of platform independent programming language design. One maps to hardware operations without surprising overhead, and another maximizes code correctness and verifiability by obeying all expected mathematical and set theoretic properties.
-
-
Sub-turing doesn’t necessarily mean much. If you need to evaluate something that is not known to terminate at compile-time you are doing something pretty strange. Agda and Idris are both sub-turing.
-
Though sub-Turing, they do allow compile time computation of values to contribute to dependent types. Without that, common families of types require reinventing compile-time versions of things like integers, as in C++ pre constexpr.
End of conversation
New conversation -
-
-
Is there anything specific that you are missing? I’m so used to the Haskell typeclass system, so I don’t know what additional things will be more convenient with a full macro system (or whatever C++ templates are).
-
Haskell typeclasses seem like the right features for a high level language, but in something like Rust you really want the ability to treat the type system as a macro assembler for library-generated code. Hygenic macros are one approach, C++ templates and constexpr are another.
- 1 more reply
New conversation -
-
-
Rust added some of this recently:https://github.com/rust-lang/rfcs/blob/master/text/2000-const-generics.md …
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
true, I'm looking forward to Jai in that regard
-
Nim and D have had this for years.
- 3 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.