Hacker News Reader

That is the dependent typed aspect mentioned. This is actually done in Idris with VerifiedSemigroup and other verified instances.

View on HN

OK. I'm afraid I don't know enough to make the connection. Actually, I never understood the point of dependent types. They seem to do away with the neat order that types introduce. ¯\_(ツ)_/¯

Reply on news.ycombinator.com