type-level range enforcement

Interval.hs

{-|

This module provides types for clamping data in a given range or
interval.

-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Interval
  ( InRange
  , inRange
  , getInRange
  , InInterval
  , inInterval
  , getInInterval
  , NatRat(..)
  )
  where

import Data.Proxy
import Data.Ratio
import GHC.TypeLits


-- | Simple interval type that only supports Natural bounds.
-- Things still get weird if @lo > hi@.
newtype InRange (lo :: Nat) (hi :: Nat) a = InRange { getInRange :: a }
  deriving (Show)

-- | Construct an 'InRange' value
inRange
  :: forall lo hi a. (KnownNat lo, KnownNat hi, Num a, Ord a)
  => a -> InRange lo hi a
inRange =
  let
    lo = fromIntegral $ natVal (Proxy :: Proxy lo)
    hi = fromIntegral $ natVal (Proxy :: Proxy hi)
  in
    InRange . max lo . min hi


-- | Rational number.  Because both numerator and denominator are
-- @Nat@, the @Bool@ parameter indicates whether the number is
-- positive (@True@) or negative (@False@).
data NatRat = NatRat Bool Nat Nat

-- | The 'InInterval' type supports ranges whose limits are
-- fractional numbers (possibly negative).  The increased
-- flexibility makes it somewhat more burdensome to use.
newtype InInterval (lo :: NatRat) (hi :: NatRat) a = InInterval {getInInterval :: a }
  deriving (Show)

-- | Construct an 'InInterval' value.  Denominators must be
-- greater than zero (enforced by type system).
inInterval
  :: forall loSign loNum loDen hiSign hiNum hiDen a.
    ( KnownBool loSign, KnownNat loNum, KnownNat loDen, 1 <= loDen
    , KnownBool hiSign, KnownNat hiNum, KnownNat hiDen, 1 <= hiDen
    , Fractional a, Ord a
    )
  => a
  -> InInterval ('NatRat loSign loNum loDen) ('NatRat hiSign hiNum hiDen) a
inInterval =
  let
    lo = natRatToFractional (Proxy :: Proxy ('NatRat loSign loNum loDen))
    hi = natRatToFractional (Proxy :: Proxy ('NatRat hiSign hiNum hiDen))
  in
    InInterval . max lo . min hi

natRatToFractional
  :: forall sign a b frac.
      (KnownBool sign, KnownNat a, KnownNat b, 1 <= b, Fractional frac)
  => Proxy ('NatRat sign a b) -> frac
natRatToFractional _ =
  let
    f = if boolVal (Proxy :: Proxy sign) then id else negate
    rational = natVal (Proxy :: Proxy a) % natVal (Proxy :: Proxy b)
  in fromRational (f rational)

class    KnownBool (b :: Bool) where boolVal :: Proxy b -> Bool
instance KnownBool True        where boolVal _ = True
instance KnownBool False       where boolVal _ = False


type MinusPointFive = 'NatRat False 1 2
type PlusPointFive = 'NatRat True 1 2
type Bogus = 'NatRat True 2 0

main :: IO ()
main = do
  print (inRange 1000 :: InRange 0 365 Integer)
  print (inRange 0.6  :: InRange 0 1 Float)
  print (inInterval 20 :: InInterval MinusPointFive PlusPointFive Float)
  print (inInterval 0.3 :: InInterval MinusPointFive PlusPointFive Double)
  print (inInterval (-0.3) :: InInterval MinusPointFive PlusPointFive Rational)

  --    this would result in type error    vvvvv
  -- print (inInterval (-20) :: InInterval Bogus PlusPointFive Rational)