Hacker News new | ask | show | jobs
by turboponyy 1472 days ago
You would have to write a wrapper class for an integer that can only be ever constructed with a positive integer without it throwing an exception, and then have it implement some PositiveInteger interface. The consumer would then have to trust that the provider has held true to the contract.

Needless to say, this code would be very verbose and ugly - what you would actually want is dependent typing, which solves this problem at the type system level.

Here is the implementation for Nat in Idris, for example:

    data Nat =
      Z
      S Nat
With dependent typing, you can specify constraints on the values of function parameters, and have the compiler prove that only such values can be passed to those functions. For example, the following function only takes non-zero natural numbers, since the S constructor used in the parameter implies that the element can not be Z:

    addTwoNonZero : (S n) -> Nat
    addTwoNonZero = (+) 2