[lkrubner]

In Clojure, I tend to put pre and post assertions on most of my functions, which is useful for checking errors in the schema of runtime data (very useful when dealing with 3rd party APIs) but it also offers the documentation that you are seeking:

    (defn advisories
    [config]
    {:pre [
         (map? config)
         (:download-advisories-dir config)
         ]
    :post [
            (map? %)
           ]
    }
    (let [
        dir (:download-advisories-dir config)
        ]

    ;; more code here

[anyfoo]

And now imagine the compiler would actually enforce that practice, and you have static typing, with less boilerplate.

[maleldil]

How is this any better than static types?

[Jtsummers]

Pre/post conditions are complementary to a type system. They can ensure logical properties that may not be encodable in your underlying type system (that is, essentially every mainstream statically typed language). Such as the relationship between two values in a collection. Trivial example, if you have a range such as [x,y] where x < y must hold, how would you convey that in any mainstream type system?

[yakshaving_jgt]

The Haskell-y way to do this is to use a smart constructor[0].

[0]: https://wiki.haskell.org/Smart_constructors

[Jtsummers]

The first part of that page demonstrates what amounts to pre/post conditions, but placed in the constructor. The range is checked dynamically, not statically.

The second part is using Peano numbers to enforce the constraint. I guess you could try and force that into some mainstream languages, probably C++. With its template programming you could get something going in this vein, though I'm not sure how well it would work if the number were calculated at runtime rather than compile time. You'd still end up with a dynamic check somewhere.

[yakshaving_jgt]

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.

If you need to statically check the construction of values in Haskell, there are things like refinement types[0].

[0]: http://nikita-volkov.github.io/refined/

[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).