←back to thread

Parse, Don't Validate (2019)

(lexi-lambda.github.io)
389 points melse | 1 comments | 26 Jun 21 07:23 UTC | HN request time: 0.21s | source
Show context
adamlett ◴[26 Jun 21 12:35 UTC] No.27641319[source]▶
I think making this about the type checker is a bit of a red herring. There is nothing in this – otherwise excellent – advice that can’t be applied to a dynamically typed language like Ruby. It’s the same insight that leads OOP folks to warn against the Primitive Obsession code smell (http://wiki.c2.com/?PrimitiveObsession). It’s also the insight that leads to the Hexagonal Architecture ( https://en.wikipedia.org/wiki/Hexagonal_architecture_(softwa... ).
replies(3): >>27641644 #>>27646073 #>>27646525 #
1. garethrowlands ◴[26 Jun 21 21:30 UTC] No.27646073[source]▶
I don't think types are a red herring here. Because if you follow this advice, then just using logic and your source code, you can prove what data is valid. And, since types and (constructive) logic are so strongly related, then the types are, in some sense "there" even if you don't see them. To put it another way, it's nice if your computer can make the proofs but if it can't, does that make the theorems any less true?