How to constrain a type field to a power of two in a type system?

Question

There is this in some JavaScript code:

function allocate(bits) {
  if ((bits & (bits - 1)) != 0) {
    throw "Parameter is not a power of 2";
  }
  ...
}

Essentially, there is a constraint on the input bits, that it is a power of two. Or instead of calling it a "constraint", you could say there is a validation on the input that it is a power of two.

Sidenote, I saw in SQL you can do these sorts of constraints:

CREATE TABLE dbo.Payroll 
    (
     ID int PRIMARY KEY, 
     PositionID INT, 
     Salary decimal(9,2),
     SalaryType nvarchar(10),  
     CHECK  (Salary > 10.00 and Salary < 150000.00) 
    );

ALTER TABLE dbo.Payroll WITH NOCHECK  
  ADD  CONSTRAINT CK_Payroll_SalaryType_Based_On_Salary
  CHECK  ((SalaryType = 'Hourly' and Salary < 100.00) or
          (SalaryType = 'Monthly' and Salary < 10000.00) or
          (SalaryType = 'Annual'));

But in both the SQL and JavaScript examples, this code executes at runtime to check if it is valid. I'm sure of the JS, not totally sure of the SQL, but I imagine it is a runtime thing.

What I'd like to know is how in a robust type system such as TypeScript or some other programming language with types you can express this "power of two" constraint. Ideally so it is a compile-time constraint. Is this possible? If so, how is it done in some language? Any language will do, mainly looking for inspiration on how to implement this in a custom language with its own type system. Not entirely sure how this would work as a compile-time constraint. It is a "type", the "type of power of two integers", but not sure how to express that.

Answer 1

There isn’t exactly a single best method of solving this, since there are a variety of approaches with varying tradeoffs. Here are a few major styles used in Haskell.

“Correct by Construction”

Instead of accepting a more general type like Int and trying to constrain it after the fact, introduce a type that can only represent valid powers of two, either by encapsulating the validation:

allocate :: PowerOfTwo -> …

module PowerOfTwo
  ( PowerOfTwo  -- Abstract type
  , powerOfTwo  -- Smart constructor
  , toInt
  ) where

newtype PowerOfTwo = PowerOfTwo Int

powerOfTwo :: Int -> Maybe PowerOfTwo
powerOfTwo n
  | isPowerOfTwo n = Just (PowerOfTwo n)
  | otherwise = Nothing

toInt :: PowerOfTwo -> Int
toInt (PowerOfTwo n) = n

Or by the principle of make invalid states unrepresentable, which can sometimes be done by convention:

-- | @'allocate' n@ allocates @2^n@ bits…
allocate :: Word -> …

Or structurally:

allocate :: PowerOfTwo -> …

-- | This type can /only/ represent 2^n.
-- (Ignore for the moment that it’s quite inefficient!)
data PowerOfTwo
  = One
  | Twice PowerOfTwo

toInt :: PowerOfTwo -> Int
toInt One = 1
toInt (Twice n) = 2 * n

Proofs and Singletons

Along with an input, require a proof that the input has already been validated by the caller; a proof is just a value that can only be constructed if you perform the validation.

In the simplest case, this is identical to the newtype solution above: PowerOfTwo is a pair of an Int and an implicit proof that it’s been validated.

But you can also make those proofs explicit, which is often done in dependently typed languages, but can be done in any language with a way of representing existential types, as in the singletons library or Ghosts of Departed Proofs style:

-- A type-level proposition that n is a power of 2.
data IsPo2 n

-- A classification of whether a value is a power of 2.
data WhetherPo2 n
  = Po2 (Proof (IsPo2 n))
  | NotPo2 (Proof (Not (IsPo2 n)))

-- Assertion that proposition ‘p’ is true.
data Proof p = TrustMe

-- Encapsulated validation, like above,
-- but now it gives back a “proof” value.
validate :: Named n Int -> WhetherPo2 n
validate (Named n)
  | isPowerOfTwo n = Po2 TrustMe
  | otherwise = NotPo2 TrustMe

In order to call ‘allocate’, you must give a proof that you validated the input:

allocate
  :: Named n Int
  -> Proof (IsPo2 n)
  -> …

And the only way to get one is from validate:

-- ‘name’ from the paper gives a type-level name to a value.
name 64 $ \ n -> case validate n of

  -- If we got a proof, we can proceed.
  Po2 p -> allocate n p

  -- Calling ‘allocate’ would be a type error here.
  NotPo2 np -> …

Dependently typed languages like Idris and ATS often use this style, with syntactic sugar like implicit parameters to help reduce the noise of passing these proof values around.

Refinements

Some languages and tools like LiquidHaskell incorporate solvers for refinement types, which are types like Int refined with propositions about them. Here, the input of allocate could be given a type like { n:Int | isPowerOfTwo n }, which is a more compact way of encoding the proof above.

A refinement type checker typically uses a combination of explicit proofs, implicit flow-sensitive analysis, and numerical solving (SMT) to verify that you have tested the conditions that ensure the propositions hold. This style has the advantage of being easy to read, but unfortunately it can be hard to predict when verification will fail with heuristic solver-based approaches for complex propositions.

---

Something I like about all of these styles is that they don’t need to repeatedly perform validation; once you have a proof that some invariant holds, either as a structural invariant or a literal proof object, then you can assume it holds, and use more efficient code that would otherwise be unsafe.