1. 9

  2. 7

    It looks like this only works cleanly for literals: if you want to pass in non-literal inputs, you have to jump through a bunch of hoops and can only get runtime checking. It will also return an Either, not raise an error if violated.

    Another difference: require can relate params to each other, like require(amount > minimum).

    1. 4

      People have also called this pattern “pushing the type safety back” and “Parse, don’t validate”. I also remember another post that talked about it in terms of constraining the domain or expanding the range but I can’t find it, does anyone have a link?

      1. 2

        This sounds a lot like dependent types, and I think those are the next logical step in type-safe programming language evolution.

        1. 3

          Refinement types are a subset of dependent types. They’re a lot more tractable and don’t always need a full-on theorem prover to verify. See Liquid Haskell and Ada12 for examples of how it works in practice.

        2. 2

          What’s wrong with nonpositive bank transfer requests? Or if this isn’t a request but an action and you’re a bank, why there is not an upper bound?

          This description is not complete. The author doesn’t cover how to introduce refined values.

          1. 2

            What he calls an “Anti-Pattern” is really just a precondition check (part of “Design by Contract”). If you can express something directly in the type system it’s better, but sometimes the backup plan is assert or some sort of language-specific equivalent to a precondition check. DBC isn’t something you’ll necessarily see all the time, but I do see it in some situations such as code which is hard to test or the code has specific conditions where it’s usable.

            The function is not actually covering the entire domain of its inputs. If a function doesn’t do this, it should really be a PartialFunction so the caller knows it doesn’t cover the entire domain.

            The caller has no way of knowing these restrictions exist without looking at the function directly.

            Most of the time they’re documented but they’re cases where such inputs are an obvious error. You can either put the burden of satisfying input bounds on the caller, or on the callee. If there are not good ways of propagating or handling errors at the lower levels, using precondition checks can simplify the lower level code.

            There’s a good chance a caller won’t “safely” call this function (e.g. wrapped in a Try) so the thrown exception could actually crash your program 😬.

            That’s usually part of the point of these types of checks, especially if the results of proceeding could be extremely bad if given outputs out of range. Also if you get thrown into some gigantic hairball of code, or one with weird crashes, pre (and post) condition checking is one of the ways of eliminating possible sources of error and validating assumptions and then getting a break in the debugger when a precondition isn’t satisfied.

            1. 1

              And there are you going to use it? Against user input?

              1. 1

                The nice part about refined is that there are bindings for JSON libraries like circe, so you can use macros to derive (de)serializers using refinement types, and you don’t need to do any programmatic validation beyond the type declaration.

                Here’s an example of it in action. Pretty cool, huh? And that’s very basic stuff, refined lets you do all kinds of zany shit like user-defined predicates and so on.