3 ms·
Does it mean that languages should prohibit type-level programming (or type-valued functions), like in Idris?
by Hirrolot 4y ago
Does it mean that languages should prohibit type-level programming (or type-valued functions), like in Idris?
- Smaug123 4y agoIn Idris, you've typed your types. Much easier to deal with.
- CRConrad 4y ago>In Idris, you've typed your types. I've always typed not only my types, but functions, programs, tests, everything, in every language I've ever coded in. OK, sometimes I first write stuff (in pseudocode, or at least bad syntax) on paper first, but in the end I always type it into a code editor on the computer. Type type type, clickety click click clack...
- madsbuch 4y agoIt most certainly does not. It means that types are not subject to tests much like you don't test your tests. types / tests are usually written in a denominational way and keeps the operational semantics of the program in check.