Hacker News Reader

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!

View on HN

At 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/Api...

Coq 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).

Reply on news.ycombinator.com