[nfoz]

With interface-typing, is there a right way to use the type system to declare "this function takes a (statically-certifiable) positive integer", not because it would fail to output a value for other numbers, but because its output would be incorrect or meaningless?

In scientific programming I've often wanted that, to push asserting particular constraints on values to the caller and/or the type system (whether that's compile-time or runtime type checks). But those constrained types would always match the interface of their unconstrained forms.

[turboponyy]

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

[iamevn]

I'd recommend looking into languages with either a contract system or dependent types.

https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Dependent_type

Contracts are ways to specify invariants for the runtime to verify. For example you could write a function with a contract saying that it takes a string containing all lowercase characters and returns a string containing all upper case characters. As far as the type system is concerned it just takes and returns strings but the runtime won't let a caller give you a value you don't want and won't let you return a value that doesn't match what you promised.

Dependent types essentially let you do the same but at the type level. For example you could have a function whose type says it takes a list of length N and a list of length M and returns a list of length N+M. Or maybe a type that represents a tuple containing a number N and a list of length N. Your code wouldn't type check unless the type system can prove the types. There's a lot of overlap with theorem provers in this space. Agda, Idris, and Coq are some decently popular languages in this category.

I find dependent types to be extremely powerful but sometimes the added overhead of figuring out how to encode an invariant into the type system is overwhelming.

[eyelidlessness]

A common approach in TypeScript, which doesn’t require a wrapping object or any runtime overhead, is called “branding” (or a variety of other names for similar concepts). It works by applying additional metadata about the value which makes it nominally incompatible with other values of the same underlying type. You can accomplish this a variety of ways, all of which have some tradeoffs. My (current) preference is to declare a class where the metadata is defined as a generic value assigned to a private property or a unique symbol, e.g.:

  declare class Branded<Meta> {
    private meta: Meta;
  }

  type Brand<T, Meta> = T & Branded<Meta>;

  type UInt = Brand<number, 'UInt’>;

[mbrodersen]

Yes. It’s called Refinement Types. I wish Rust came with Refinement Types from day one. That would have been a massive step forward instead of the much smaller step forward that Rust is currently taking.