4 ms·
I've heard that technique described as "type tetris". I find myself trusting the type system to guide me a lot in Rust too -- it's very nice!
by cfallin 10y ago
I've heard that technique described as "type tetris". I find myself trusting the type system to guide me a lot in Rust too -- it's very nice!
- runeks 10y agoAt the end of that spectrum (moving away from values and towards types) are languages like Coq, where you have only types, no values, and it's the compiler that derives the implementation/values from the types you define. Like Haskell Servant[1], where you define your API as a type, and then you can derive functions from that type to query the API, because the type itself contains all the information necessary. Pretty fascinating stuff. [1] http://haskell-servant.readthedocs.io/en/stable/tutorial/ApiType.html http://haskell-servant.readthedocs.io/en/stable/tutorial/Api...
- cmrx64 10y agoCoq unifies terms and types, so that all you have a terms, but there's still a very concrete meaning of value: that which can be reduced no further (normalization, a property that the calculus of inductive constructions has).