Conversation

"Strong types" /= "Static types", and "Static types" /= "Contracts". Invalid states are often a runtime property. Contracts are a much better tool for representing valid value-states than types are.

Quote Tweet

Gabriella Gonzalez

@GabriellaG439

· Feb 17, 2018

Pervasive defensive programming is a symptom of a lack of strong types. If your language can make invalid states unrepresentable then you only need to validate input at the edges of your system

Gabriella Gonzalez

@GabriellaG439

Feb 17, 2018

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

Hillel

@hillelogram

Feb 17, 2018

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.

It's still not clear to me why you believe contracts are the better tool

Replying to

and

I'm also unclear as to why

@Hillelogram

perceives a massive difference in the approaches? I was of the impression that refinement types were providing static proof of contracts, perhaps in a simpler, clearer core calculus. Or am I missing something here?

1:21 PM · Feb 18, 2018Twitter Web Client

Replying to

and

Because contracts are a deep and sophisticated field with a lot of work and success behind it, and reducing it to just "refinement types" is like saying monads are just pipes.