[Jtsummers]

> The way that the value floats through the system is checked statically, and the program can (and should) be designed so that the value with the appropriate type cannot be constructed unsafely.

Except that in the first example from the first link you sent me, there is no static guarantee that the inputs to the constructor are valid, thus the error branch (it would be unnecessary if static guarantees could be made regarding the use of the constructor). And that was my point, that you still end up with dynamic checks on the values which is where pre/post conditions step in to cover what static typing cannot (or, again, cannot easily in mainstream languages, which would not be Haskell).

[yakshaving_jgt]

Is there any reason you didn't address the second link that I shared?

[Jtsummers]

Mostly because, per my reading (as an admitted Haskell dabbler and not fluent), it looks like a variation on a theme rather than a totally different thing. It seems to be a more consistent and refined (har har) way of doing the same thing as the first link, and still has a dynamic check (at least in one form, refine vs refineTH) just like the smart constructors.

But also because we got derailed from my initial point and context.

> Pre/post conditions are complementary to a type system.

Do you disagree or agree with this statement? Because you never addressed it either.

> They can ensure logical properties that may not be encodable in your underlying type system

Note the "may", because that's important. I didn't say that there were no languages in which my example could be encoded in the type system. And maybe it wasn't the best example, but the point itself was that there is no type system (that I'm aware of, not even Idris as far as I know) which can prove in its static type system every piece of logic about a program. This means that some properties of the system will end up being checked (if you bother to) at runtime and not at compile time. That's where pre/post conditions are useful, they contain information (and in a more deliberate form in cases like the Clojure example) about the properties of the system that are hard or impossible to encode directly in the type system.

Different type systems (both static and dynamic) let you express more or less with them, which reduces the need/desire to have checks like these in your program. But I seriously doubt that any mainstream language will ever totally remove their utility, as complements to the rest of the type system.

[lmm]

> there is no type system (that I'm aware of, not even Idris as far as I know) which can prove in its static type system every piece of logic about a program.

Many static type systems can prove anything that can be proven. Notionally one might write a program that relies on something unproven like the Collatz conjecture, though I'm not sure that would happen in practice (e.g. it's easy to write a program that relies on the Collantz conjecture for numbers below 2^64, but that's quite provable). Whether it's actually worth writing out the proof is another question though.

> This means that some properties of the system will end up being checked (if you bother to) at runtime and not at compile time. That's where pre/post conditions are useful, they contain information (and in a more deliberate form in cases like the Clojure example) about the properties of the system that are hard or impossible to encode directly in the type system.

This is true but makes surprisingly little difference, because you still want to keep track of which values have or haven't had that runtime check applied. So you almost always want your postconditions expressed as types (even if they're just "marker" types that indicate that a given runtime check was passed). Put another way, any metadata you would want to be able to track about a function's argument values or return value, you almost always want to be able to carry that metadata around with that value before it's passed in or after it's returned - but at that point that metadata is a type, and it's easiest to represent it as one.

[yakshaving_jgt]

Sorry, I should have been clearer. I was referring to the Template Haskell part of that refinement types library, where the construction of values can indeed be statically checked at compile time.

> > Pre/post conditions are complementary to a type system.

> Do you disagree or agree with this statement? Because you never addressed it either.

I agree with it. I write web applications in Haskell for a living, and the very nature of web applications is that most values coming into the system are not known until runtime. It is not a reasonable design goal to want every possible value in the system to be verified at compile time. However, it is valuable to be able to statically verify the relationships between functions and values as those values — once they have been parsed at runtime into a more principled type — move through the system.