DefNat.hs

#!/usr/bin/env stack
{- stack
     --resolver lts-17.10
     --install-ghc
     exec ghci
     --package aeson
     -- -ignore-dot-ghci -XDataKinds -XTypeApplications
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

module DefNat
  ( DefNat
  , def
  , nat
  ) where

import Data.Aeson (FromJSON(parseJSON), ToJSON(toJSON))
import Data.Function (on)
import Data.Maybe (fromMaybe)
import Data.Proxy (Proxy(Proxy))
import GHC.Natural (Natural)
import GHC.TypeLits (KnownNat, Nat, natVal)
import Prelude

-- | 'DefNat' is a 'Natural' with a type-level default value.
--
-- > type MaxPageSize = DefNat 50
data DefNat (def :: Nat)
  = Default
  | Specific Natural

-- | The default 'DefNat'.
def :: (KnownNat def) => DefNat def
def = Default

-- | Get the 'Natural' out of a 'DefNat'.
nat :: forall def. (KnownNat def) => DefNat def -> Natural
nat = \case
  Default -> fromIntegral $ natVal $ Proxy @def
  Specific natural -> natural

instance (KnownNat def) => Show (DefNat def) where
  show = show . nat

instance (KnownNat def) => Num (DefNat def) where
  (+) a b = Specific $ ((+) `on` nat) a b
  (-) a b = Specific $ ((-) `on` nat) a b
  (*) a b = Specific $ ((*) `on` nat) a b
  abs = Specific . abs . nat
  signum = Specific . signum . nat
  fromInteger = Specific . fromIntegral

instance (KnownNat def) => FromJSON (DefNat def) where
  parseJSON json = do
    parseJSON json >>= \case
      Nothing -> pure def
      Just natural -> pure $ Specific natural

instance (KnownNat def) => ToJSON (DefNat def) where
  toJSON = \case
    Default -> toJSON $ nat @def def
    Specific natural -> toJSON natural