Checked- Inbuilt checking for ultra reliable computing

Safe HaskellNone



A checked value is a value, potentially wrapped in a warning, i.e. a non-fatal exception.

Where the checked value looks like (Right value), the value is within limits Where the checked value looks like (Left (warning, cause, value)), the value is out of limits

Warning is ("warning message", severity), and cause is also a (Left (warning, cause value)) which allows a "linked list" of warnings to be set up

Run your code within a Checked monad to benefit from real time checking

To retrofit checking to an existing function myFunc :: MyType1 -> MyType2 -> MyType3:

(a) define a type which is a tuple of the parameters to myFunc

    type  MyFuncParams = (MyType1, MyType2)

(b) define the test for validity of the parameters expected by myFunc:

     instance Checkable MyFuncParams where
       check params = .. Checked (Right params) -- if OK
                      .. Checked (Left (pack "Invalid params to myFunc", 20), Nothing, params) -- if params are out of whack

(c) define the test for validity of the output type, or any type in your code:

     instance Checkable MyType3 where
       check v = .. Checked (Right v) -- if OK
                 .. Checked (Left (pack "Type MyType3 is out of range", 20), Nothing, v) -- if the value is out of whack for this type

(d) define a wrapper function for myFunction for myFunc which accepts a parameter of type MyFuncParams:

     myFunc' :: MyFuncParams -> MyType3
     myFunc' (a, b) = myFunc a b
 * Looking to automate this step, perhaps with TH *

(e) run your function within the Checked monad, using applyWithParamsCheck as the function calls, and check to check the output values

 code :: MyType1 -> MyType2 -> Checked MyType4
 code a b = do
     f <- applyWithCheckedParams myFunc' (a, b)
     g <- check y
     h <- applyWithCheckedParams myFunc1' g
     check h



type Warning = (Text, Integer)Source

A warning that the value is not within limits, with a measurable indication of severity

data Checked a Source

A wrapper type indicating that the value is or is not within limits


forall b . Checked (Either (Warning, Maybe (Checked b), a) a) 


Monad Checked

The monadic values also combine like the Applicative

Functor Checked

The function is simply applied to the value within the checked wrapper

Applicative Checked

Checked values combine as you would expect, except that two Left values combine to set up a trace of warnings

Show a => Show (Checked a)

for debugging

getCheckedValue :: Checked a -> aSource

Useful function

class Checkable a whereSource

This is implemented for types whose values will be checked


check :: a -> Checked aSource

applyWithParamsCheck :: Checkable a => (a -> b) -> a -> Checked bSource

This is needed because we need to select the correct check function for the parameters to this function We do this by capturing the parameters as a single type, for which we have defined a checkable instance