[turboponyy]

You should use asserts or throw errors to prevent misuse of a procedure by the caller. Ideally, you could model these constraints at the type level. You can think of pre-conditions as a sort of pseudo-dependent typing.

Consider the following pseudocode:

    // Idris
    binarySearch : SortedList a -> a -> Maybe Nat
    binarySearch = ?implementation

    // Java
    int binarySearch(List<T> elems, T elem) {
        assert isSorted(elems);
        throw new NotImplemented();
    }

(The generic type parameter should also implement Comparable or similar, but I digress).

In this case, it would be nonsensical to pass an unsorted list to either procedure, so we prevent it - in Idris' case by using dependent typing; in Java's case by using assertions.

To contrast, consider the following:

    // Idris
    readLines : Path -> IO (Either FileError (List String))
    readLines = ?implementation

Here, the FileError represents a number of things that could go wrong: no file existing at the given path, lack of permissions, running out of memory during read and so on. However, this is not misuse of the procedure - these are all expected deviations from the happy path, and hence we model that in the type definition.

(I've omitted a corresponding Java example, as following a similar style would be terribly non-idiomatic. Java prefers throwing and catching exceptions to manage non-happy paths)

Note that we can't constrain the Path parameter to only resolve to files that exist. Doing so would require knowledge of the current filesystem state, e.g. the type signature would be something like the following:

    readLines : (fs : FileSystem) -> (p : Path) -> fileExists fs p -> IO (Either FileError (List String))
    readLines = ?implementation

To summarize, use preconditions, assertions or type-level constraints to prevent misuse of procedures. Return errors (using sum types, for example) when it is known and expected that the result of a procedure can deviate from the happy path. You may refrain from modeling conditions at the type level, even if possible in principle, as it may be prohibitively complex.