The validations that you would normally put in a contract can exist at the type-level, too, and be verified using symbolic reasoning at compile-time. For example: haskellforall.com/2015/12/compil
Conversation
Sure, and you can force contacts to check for nulls. Doesn't mean it's the right tool.
For the record, many contracts can also be checked statically. Check out the work by with Whiley.
2
3
In general contracts on the type level are a limited form of contracts. One example, you can have contracts between parameters in a function, or postcondition on side effects
1
1
Liquid Haskell can do those, too. The post I linked contains examples of both of those (i.e. there is an example of a contract between input parameters and statically enforcing a postcondition on the result of a side effect is the exercise at the end of a post)
2
2
Liquid Haskell is still an experimental research project. Contracts have seen production use in safety critical systems for years now, via SPARK.
1
1
I think this is drifting a bit from my original point, which is that you should push runtime validation to the edge of the system. Whether or not a specific implementation of that ideal is sufficiently battle-tested is orthogonal
2
3
Your original point was that strong types obviates the need for lots of defensive programming. I'm saying that it may, but you're using the wrong ish tool: contracts are more suited for this specific use case. This is in part because we have practical data they do.
1
1
I guess my resistance might be due to a philosophical difference. I've always viewed attempts to make complex languages safe as solving the wrong problem. I believe we should instead be trying to make languages simpler and more constrained so that they are automatically safe.
1
6
Well, some would say that refinement types are too complex ;)
So from my understanding, you know very little about contracts. That goes both ways: many contracts people know very little about refinement types. PLT is super insular even with respect to itself.
2
I actually agree that even refinement types are too complex. I think they would not be necessary at all if the programming language were more constrained
1
Would be nice to see refinements operating at the the level of automation, elaborating into a core proof language. Perhaps if the proofs (both manual or via a solver) are too hard, explicitly fall back to runtime validation + property testing in the interim.