Fractional bound allow precise definition of upper and lower bounds of a particular number

FractionalBoundedExample.hs

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Lib where


import GHC.TypeLits
import Data.Proxy 

head' :: [a] -> Maybe a
head' []    = Nothing
head' (x:_) = Just x

exec :: IO ()
exec = putStrLn "micro850-parser from template"


data Sign = Pos | Neg

-- | we need to demote sign when needed
newtype SSign (s::Sign)= SSign Sign

class Signed (sign::Sign) where
  sSign :: SSign sign

instance Signed 'Pos where
 sSign = SSign Pos 

instance Signed 'Neg where
 sSign = SSign Neg

signVal :: forall sign proxy . Signed sign => proxy sign -> Sign 
signVal _ = case sSign :: SSign sign of
              SSign Pos -> Pos
              SSign Neg -> Neg


-- Bound Constraint for calculating a signed fractional boundary 
-- with a decimal part with no more infinitesimal fraction than  0.000000000000001

data Frac (sign::Sign) (whole :: Nat) (part :: Nat) 



class SignedBound  b where 
  signedLimit :: (RealFrac v) => proxy b -> v


instance forall whole part sign . (KnownNat whole,KnownNat part,Signed sign ) => SignedBound (Frac sign whole part ) where
  signedLimit _ = let
               sign = signVal (Proxy :: Proxy sign)
               whole = natVal (Proxy :: Proxy whole)
               part = natVal (Proxy :: Proxy part)
               applySign Neg = ( (-1) *)
               applySign Pos = ( 1 *)
               in applySign sign (fromIntegral whole + (fromIntegral part  / fromIntegral @Integer 1000000000000000))
-- Value layer

-- λ> signedLimit test
-- -0.11

test :: Proxy (Frac 'Neg 0 110000000000000)
test = Proxy :: (Proxy (Frac 'Neg 0 110000000000000))

newtype BoundNumber l u t = BoundNumber t
  deriving (Num,Show,Eq,Ord)
data BoundCreationError = LowerBoundExceeded | UpperBoundExceeded 
 deriving (Show,Eq,Ord)
 
buildBoundNumber :: forall lowerWhole lowerPart upperWhole upperPart t  lowerSign upperSign.

                    KnownNat upperWhole =>
                    KnownNat upperPart   =>
                    Signed upperSign => 
                    RealFrac t => 
                    SignedBound (Frac lowerSign lowerWhole lowerPart) =>
                    t -> Either BoundCreationError (BoundNumber (Frac lowerSign lowerWhole lowerPart ) (Frac upperSign upperWhole upperPart) t) 


buildBoundNumber t = let
  lowerBound = signedLimit (Proxy :: Proxy (Frac lowerSign lowerWhole lowerPart)) 
  upperBound = signedLimit (Proxy :: Proxy (Frac upperSign upperWhole upperPart))
  checkT 
    | t < lowerBound = Left LowerBoundExceeded
    | t > upperBound = Left UpperBoundExceeded
    | otherwise = Right $ BoundNumber t
  in checkT

-- Bound between weak pi approximation
type ExampleBoundNumber  = BoundNumber (Frac 'Neg 3 141590000000000) (Frac 'Pos 3 141590000000000) Double
                                                  --110000000000000               110000000000000

buildExampleBoundNumber :: Double -> Either BoundCreationError ExampleBoundNumber
buildExampleBoundNumber v = buildBoundNumber v