2 ms·

Or Idris dependent types, which allows you to prove properties of any value, not just numbers.

• zokier 5y ago
  Afaik refinement types (e.g. LiquidHaskell) are bit more appropriate than dependent types for this sort of thing