Haskell Range Control Arithmetic with Type-Level Literals
Functional programming (FP), as is well known, contributes to writing reliable (error-free) code.
Clearly this is a maxim. There are no programs without errors. However, the OP in combination with the strict static typification and development of the type system allows, to a large extent, to reveal the inevitable errors of the programmer at the compilation stage. I'm talking about Haskell, although it probably also applies to OCaml.
However, if we set ourselves the goal of writing reliable code, we will immediately discover that the possibilities of Haskell are not endless here. Not everything that exists for this purpose (building secure code) in other languages is easily implemented in Haskell. It would be nice if they corrected me here, but alas
First of all, of course, you should pay attention to the Hell language (to a lesser extent, related to her pascal), which was specially developed for reliable code writing. And although the ideology of Ada, in my opinion, has long been outdated, the syntax draws fossils from the 80s, and some ideas that supposedly increase the security of the code now cause a grin. For all of this, Ada has a developed system of static and dynamic data verification for given conditions ( data validation , constraint validation ). Simply put, every time a variable is updated, the compiler can add to the output code the execution of the test we set. The simplest and most common case is range validation - the value is outside the specified limits. Such control is in pascal. Without claiming to replace Ada (it is a standard in the military, in avionics, etc.), we will try to get closer to Ada’s safety standards by making Haskell range validation , for a start. Obviously, it is necessary to overload the arithmetic functions (this is at least) of the class Num , by setting the range control in them and throwing exceptions when it exceeds its limits.
Immediately we run into the problem - in the arithmetic functions of the class Num, of the form
There is no place to set the boundaries of the tested range. What can be done?
')
Option 1 . Create a record of three numbers - the boundaries of the range and value to be processed, and determine (instantiate) for such a record Num . The disadvantage is obvious. It would be enough for us to store the boundaries of the ranges in one copy for each type, but not for each value (there may be 100,000).
Option 2 . We can specify checks with hard boundaries in the class generated by Template Haskell. This option is quite possible. With the help of TH, we can do everything. But let's try to find a way to set the boundaries of the range at compile time in some other way.
Option 3 . Relatively recently, starting from GHC 7.8, if I do not confuse, an opportunity has appeared, called the Type-Level Literals , i.e. assignments of constants in the description of types, which, moreover, can be used in functions.
Let's try to implement range validation using this mechanism.
For a controlled number, we will not economically start a full data type, we will write, requiring less expense during the execution of a newtype.
RgVld is short for range validation . And lo and hi , having the type Nat (defined in GHC.TypeLits ) are the very constants in the definition of the type - the boundaries of the range. Here they are integers (converted to Integer, but can not be negative, alas). There are more string - but to describe the restrictions of the string and convert to string in runtime - no, we do not write in the script.
Actually, this type is the essence of the implementation of range validation . For him, you can now create:
The KnownNat class is also defined in GHC.TypeLits . Since checks of the resulting values are the same, for them you can create an auxiliary class
Naturally, you need to remember to create the exception class itself:
For the RgVld type, we also implement the Show , Read classes, and quite simple, but obviously useful in this case, Bounded .
Since Since the Ada language, which is strongly associated with the “military”, we assume that our program controls the ICBM with divided warheads. Suppose they are numbered from one, but there are only 20 of them, and each, of course, carries an atomic bomb - A-bomb, “H-bombs”. Reduce to ab. And here is an auxiliary function for creating an e-bomb:
The variable is the number of the bomb in the MBR, in the range from 1 to 20. If the rocket is upgraded, then the number 20 will need to be changed only in this auxiliary function. Check it out.
- here and control ranges in Haskell.
The attentive reader may argue: "Usually we do not add two numbers in the range, but add an offset to the range type." Actually, this is not important for this implementation - not the input values of the operations are checked, but only the output values, therefore it will not cause interruptions.
But, sort of, like, and not beautifully obtained. We introduce an additional class
Functions (+.), (-.), (*.) Are similar to ordinary ones, but perform actions with a range type and a regular number. Example:
Naturally, the range type is not required to be integer. Create a helper function to determine the level of fuel.
And check the work of the range type when refueling:
Unfortunately, “due to” the limitations of the “technology” used - the Type-Level Literals range is still set to integers. Maybe the authors of the GHC will improve it (although, in general, it is somewhat conceived by them for another). In the meantime, we will be happy and with what we met.
Full example code:
Clearly this is a maxim. There are no programs without errors. However, the OP in combination with the strict static typification and development of the type system allows, to a large extent, to reveal the inevitable errors of the programmer at the compilation stage. I'm talking about Haskell, although it probably also applies to OCaml.
However, if we set ourselves the goal of writing reliable code, we will immediately discover that the possibilities of Haskell are not endless here. Not everything that exists for this purpose (building secure code) in other languages is easily implemented in Haskell. It would be nice if they corrected me here, but alas
First of all, of course, you should pay attention to the Hell language (to a lesser extent, related to her pascal), which was specially developed for reliable code writing. And although the ideology of Ada, in my opinion, has long been outdated, the syntax draws fossils from the 80s, and some ideas that supposedly increase the security of the code now cause a grin. For all of this, Ada has a developed system of static and dynamic data verification for given conditions ( data validation , constraint validation ). Simply put, every time a variable is updated, the compiler can add to the output code the execution of the test we set. The simplest and most common case is range validation - the value is outside the specified limits. Such control is in pascal. Without claiming to replace Ada (it is a standard in the military, in avionics, etc.), we will try to get closer to Ada’s safety standards by making Haskell range validation , for a start. Obviously, it is necessary to overload the arithmetic functions (this is at least) of the class Num , by setting the range control in them and throwing exceptions when it exceeds its limits.
Immediately we run into the problem - in the arithmetic functions of the class Num, of the form
(+) :: a -> a -> a There is no place to set the boundaries of the tested range. What can be done?
')
Option 1 . Create a record of three numbers - the boundaries of the range and value to be processed, and determine (instantiate) for such a record Num . The disadvantage is obvious. It would be enough for us to store the boundaries of the ranges in one copy for each type, but not for each value (there may be 100,000).
Option 2 . We can specify checks with hard boundaries in the class generated by Template Haskell. This option is quite possible. With the help of TH, we can do everything. But let's try to find a way to set the boundaries of the range at compile time in some other way.
Option 3 . Relatively recently, starting from GHC 7.8, if I do not confuse, an opportunity has appeared, called the Type-Level Literals , i.e. assignments of constants in the description of types, which, moreover, can be used in functions.
Let's try to implement range validation using this mechanism.
For a controlled number, we will not economically start a full data type, we will write, requiring less expense during the execution of a newtype.
newtype RgVld (lo :: Nat) (hi :: Nat) a = RgVld { unRgVld :: a } deriving (Eq, Ord) RgVld is short for range validation . And lo and hi , having the type Nat (defined in GHC.TypeLits ) are the very constants in the definition of the type - the boundaries of the range. Here they are integers (converted to Integer, but can not be negative, alas). There are more string - but to describe the restrictions of the string and convert to string in runtime - no, we do not write in the script.
Actually, this type is the essence of the implementation of range validation . For him, you can now create:
instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a) => Num (RgVld lo hi a) where (RgVld l) + (RgVld r) = chkVld "(+)" $ RgVld $ l+r (RgVld l) - (RgVld r) = chkVld "(-)" $ RgVld $ lr (RgVld l) * (RgVld r) = chkVld "(*)" $ RgVld $ l*r fromInteger n = chkVld "fromInteger" $ RgVld $ fromInteger n abs = id signum (RgVld v) = RgVld $ signum v The KnownNat class is also defined in GHC.TypeLits . Since checks of the resulting values are the same, for them you can create an auxiliary class
class CheckValidation a where chkVld:: String -> a -> a (which can be useful for other types of checks) with a single function chkVld , which will pass values that fall into the range and throw an exception for values out of range. Its first argument is a substring in the exception message that shows the function that caused the exception. instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a) => CheckValidation (RgVld lo hi a) where chkVld whr r@(RgVld v) = let lo' = natVal (Proxy :: Proxy lo) hi' = natVal (Proxy :: Proxy hi) in if v < fromInteger lo' || v > fromInteger hi' then throw $ OutOfRangeException $ "out of range [" ++ show lo' ++ " .. " ++ show hi' ++ "], value " ++ show v ++ " in " ++ whr else r Naturally, you need to remember to create the exception class itself:
data OutOfRangeException = OutOfRangeException String deriving Typeable instance Show OutOfRangeException where show (OutOfRangeException s) = s instance Exception OutOfRangeException For the RgVld type, we also implement the Show , Read classes, and quite simple, but obviously useful in this case, Bounded .
instance (KnownNat lo, KnownNat hi, Show a) => Show (RgVld lo hi a) where show (RgVld v) = show v instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a, Read a) => Read (RgVld lo hi a) where readsPrec w = \s -> case readsPrec ws of [] -> [] [(v,s')] -> [(chkVld "readsPrec" $ RgVld v, s')] instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a) => Bounded (RgVld lo hi a) where minBound = fromInteger $ natVal (Proxy :: Proxy lo) maxBound = fromInteger $ natVal (Proxy :: Proxy hi) Since Since the Ada language, which is strongly associated with the “military”, we assume that our program controls the ICBM with divided warheads. Suppose they are numbered from one, but there are only 20 of them, and each, of course, carries an atomic bomb - A-bomb, “H-bombs”. Reduce to ab. And here is an auxiliary function for creating an e-bomb:
ab:: Int -> RgVld 1 20 Int ab = RgVld The variable is the number of the bomb in the MBR, in the range from 1 to 20. If the rocket is upgraded, then the number 20 will need to be changed only in this auxiliary function. Check it out.
*RangeValidation> ab 2 + ab 3 5 *RangeValidation> ab 12 + ab 13 *** Exception: out of range [1 .. 20], value 25 in (+) *RangeValidation> - here and control ranges in Haskell.
The attentive reader may argue: "Usually we do not add two numbers in the range, but add an offset to the range type." Actually, this is not important for this implementation - not the input values of the operations are checked, but only the output values, therefore it will not cause interruptions.
*RangeValidation> ab 20 + ab 0 20 *RangeValidation> But, sort of, like, and not beautifully obtained. We introduce an additional class
class Num' ab where (+.) :: a -> b -> a (-.) :: a -> b -> a (*.) :: a -> b -> a which implements arithmetic with operands of different types, and make RgVld its instance by defining instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a) => Num' (RgVld lo hi a) a where (RgVld l) +. r = chkVld "(+.)" $ RgVld $ l+r (RgVld l) -. r = chkVld "(-.)" $ RgVld $ lr (RgVld l) *. r = chkVld "(*.)" $ RgVld $ l*r Functions (+.), (-.), (*.) Are similar to ordinary ones, but perform actions with a range type and a regular number. Example:
*RangeValidation> ab 5 -. (3 :: Int) 2 *RangeValidation> - yes, the type of the number will have to be specified explicitly if this is a constant.Naturally, the range type is not required to be integer. Create a helper function to determine the level of fuel.
fuel:: Double -> RgVld 0 15 Double fuel = RgVld And check the work of the range type when refueling:
*RangeValidation> fuel 4.6 + fuel 4.5 9.1 *RangeValidation> fuel 9.1 + fuel 6 *** Exception: out of range [0 .. 15], value 15.1 in (+) *RangeValidation> - Oh no no no. Pour over!Unfortunately, “due to” the limitations of the “technology” used - the Type-Level Literals range is still set to integers. Maybe the authors of the GHC will improve it (although, in general, it is somewhat conceived by them for another). In the meantime, we will be happy and with what we met.
Full example code:
{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances #-} {-# LANGUAGE DeriveDataTypeable #-} module RangeValidation where import Data.Proxy import GHC.TypeLits import Data.Typeable import Control.Exception data OutOfRangeException = OutOfRangeException String deriving Typeable instance Show OutOfRangeException where show (OutOfRangeException s) = s instance Exception OutOfRangeException class CheckValidation a where chkVld:: String -> a -> a instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a) => CheckValidation (RgVld lo hi a) where chkVld whr r@(RgVld v) = let lo' = natVal (Proxy :: Proxy lo) hi' = natVal (Proxy :: Proxy hi) in if v < fromInteger lo' || v > fromInteger hi' then throw $ OutOfRangeException $ "out of range [" ++ show lo' ++ " .. " ++ show hi' ++ "], value " ++ show v ++ " in " ++ whr else r newtype RgVld (lo :: Nat) (hi :: Nat) a = RgVld { unRgVld :: a } deriving (Eq, Ord) instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a) => Num (RgVld lo hi a) where (RgVld l) + (RgVld r) = chkVld "(+)" $ RgVld $ l+r (RgVld l) - (RgVld r) = chkVld "(-)" $ RgVld $ lr (RgVld l) * (RgVld r) = chkVld "(*)" $ RgVld $ l*r fromInteger n = chkVld "fromInteger" $ RgVld $ fromInteger n abs = id signum (RgVld v) = RgVld $ signum v infixl 6 +.,-. infixl 7 *. class Num' ab where (+.) :: a -> b -> a (-.) :: a -> b -> a (*.) :: a -> b -> a -- (/.) :: a -> b -> a instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a) => Num' (RgVld lo hi a) a where (RgVld l) +. r = chkVld "(+.)" $ RgVld $ l+r (RgVld l) -. r = chkVld "(-.)" $ RgVld $ lr (RgVld l) *. r = chkVld "(*.)" $ RgVld $ l*r instance (KnownNat lo, KnownNat hi, Show a) => Show (RgVld lo hi a) where show (RgVld v) = show v instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a, Read a) => Read (RgVld lo hi a) where readsPrec w = \s -> case readsPrec ws of [] -> [] [(v,s')] -> [(chkVld "readsPrec" $ RgVld v, s')] instance (KnownNat lo, KnownNat hi, Num a, Ord a, Show a) => Bounded (RgVld lo hi a) where minBound = fromInteger $ natVal (Proxy :: Proxy lo) maxBound = fromInteger $ natVal (Proxy :: Proxy hi) -- examples ab:: Int -> RgVld 1 20 Int ab = RgVld fuel:: Double -> RgVld 0 15 Double fuel = RgVld Source: https://habr.com/ru/post/253157/
All Articles