2 ms·

The ability to reason about code, to split it into modules that can be developed independently etc. is not dependent on having a static type system. It is depen

• nyssos 3y ago
  > "Types" is just one form of, in many languages quite limited, specs. That's the "Curry types" perspective described in the article, yes. "Church types" are syntax, not specification. In Haskell, for example main = print (5 + "foo") isn't a program that fails to conform to its spec, it's just not a program. It has no meaning and no behavior, not wrong behavior. You can (but should never) `unsafeCoerce` `5` to `String` or `"foo"` to `Int` and get something broken out - but they'll be different broken things, and neither will in any sense be the compiled form of the `main` function above.