Функциональное программирование (ФП), как известно, способствует написанию надёжного (безошибочного) кода.
Ясно, что это максима. Программ без ошибок не бывает. Однако ФП в сочетании со строгой статической типизацией и развитостью системы типов позволяет, в значительной степени, выявлять неизбежные ошибки программиста ещё на стадии компиляции. Я говорю о Haskell, хотя, наверное, к OCaml это тоже относится.
Однако если мы зададимся целью написания надёжного кода, то немедленно обнаружим, что возможности Haskell тут не безграничны. Не всё, что существует для этой цели (построения безопасного кода) в других языках легко реализуется на Haskell. Хорошо бы меня тут поправили, но, увы.
В первую очередь, разумеется, стоит обратить внимание на специально разработанный для надёжного написания кода язык Ада (в меньшей степени, родственный ей паскаль). И хотя идеология Ады, на мой взгляд, давно устарела, синтаксис тянет за собой окаменелости из 80-х, а некоторые идеи, якобы повышающие безопасность кода, сейчас вызывают усмешку. При всё том в Аде имеется развитая система статической и динамической проверки данных на заданные условия (data validation, constraint validation). Попросту говоря, при каждом обновлении переменной компилятор может добавить в выходной код выполнение заданной нами проверки. Самый простейший и наиболее распространённый случай — это range validation – выход значения за заданные пределы. Такой контроль есть и в паскале. Не претендуя на замену Ады (она является стандартом у военных, в авионике, и т.п.) попробуем приблизиться к стандартам безопасности Ады, сделав, для начала, range validation в Haskell. Очевидно, нужно перегрузить арифметические функции (это уж, как минимум) класса Num, задав в них контроль диапазона и выбрасывать исключения при выходе за его пределы.
Сразу же упираемся в проблему – в арифметических функциях класса Num, вида
(+) :: a -> a -> a
нет места для задания границ проверяемого диапазона. Что можно сделать?
Вариант 1. Создать запись из трёх чисел – границ диапазона и обрабатываемого значения, и определить (инстанцировать) для такой записи Num. Недостаток очевиден. Нам достаточно было бы хранить границы диапазонов в одном экземпляре для каждого типа, а не для каждого значения (которых может быть 100000).
Вариант 2. Мы можем задавать проверки с жёсткими границами в классе, генерируемом с помощью Template Haskell. Такой вариант вполне возможен. С помощью TH мы можем сделать всё. Но, попробуем найти способ задания границ диапазона во время компиляции каким то другим путём.
Вариант 3. Относительно недавно, начиная с GHC 7.8, если не путаю, появилась возможность, называемая Type-Level Literals, т.е. задания констант в описании типов, которые, к тому же, можно использовать в функциях.
Попробуем реализовать range validation с помощью этого механизма.
Для контролируемого числа экономно не будем заводить полный тип data, напишем, требующий меньших издержек во время выполнения newtype.
newtype RgVld (lo :: Nat) (hi :: Nat) a = RgVld { unRgVld :: a }
deriving (Eq, Ord)
RgVld – это сокращение от range validation. А lo и hi, имеющие тип Nat (определённый в GHC.TypeLits) — это те самые константы в определении типа – границы диапазона. Здесь они целые (конвертируются в Integer, но не могут быть отрицательными, увы). Существуют ещё строковые – но описывать ограничения строкой и конвертировать в строки в runtime — нет уж, мы не на скрипте пишем.
Собственно, этот тип – суть реализации range validation. Для него теперь можно создать:
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 lo hi a
(RgVld l) - (RgVld r) = chkVld "(-)" $ (RgVld (l-r)) :: RgVld lo hi a
(RgVld l) * (RgVld r) = chkVld "(*)" $ (RgVld (l*r)) :: RgVld lo hi a
fromInteger n = chkVld "fromInteger" $ (RgVld (fromInteger n)) :: RgVld lo hi a
abs = id
signum (RgVld v) = (RgVld (signum v)) :: RgVld lo hi a
Класс KnownNat так же определен в GHC.TypeLits. Т.к. проверки получающихся значений одинаковы, для них можно создать вспомогательный класс
class CheckValidation a where
chkVld:: String -> a -> a
(который, может сгодится и для других типов проверок) с единственной функцией chkVld, которая будет пропускать через себя попадающие в диапазон значения и выбрасывать исключение для значений выходящих за диапазон. Её первый аргумент – подстрока в сообщении исключения показывающее функцию вызвавшую исключение.
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
Естественно, нужно не забыть создать и сам класс исключения:
data OutOfRangeException = OutOfRangeException String
deriving Typeable
instance Show OutOfRangeException where
show (OutOfRangeException s) = s
instance Exception OutOfRangeException
Для типа RgVld заодно реализуем классы Show, Read, и совсем простой, но очевидно полезный в данном случае 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 w s of
[] -> []
[(v,s')] -> [(chkVld "readsPrec" $ (RgVld v) :: RgVld lo hi a,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)
Т.к. речь шла о языке Ada, который прочно ассоциируется с «военкой», то мы предположим, что наша программа контролирует МБР с разделяющимися боеголовками. Допустим, их нумеруют с единицы, а всего их 20, и каждая, само собой, несёт атомную бомбу — A-bomb, «Эйч-бомб». Сократим до ab. А вот и вспомогательная функция для создания эйч-бомбы:
ab:: Int -> (RgVld 1 20 Int)
ab = RgVld
Переменная – номер бомбы в МБР, в диапазоне от 1 до 20. Если ракету модернизируют, то число 20 понадобится изменить только в этой, вспомогательной функции. Проверим.
*RangeValidation> ab 2 + ab 3
5
*RangeValidation> ab 12 + ab 13
*** Exception: out of range [1 .. 20], value 25 in (+)
*RangeValidation>
— вот и контроль диапазонов в Haskell.
Внимательный читатель может возразить: «Обычно мы не складываем два числа в границах диапазона, а прибавляем к диапазонному типу смещение». Вообще-то для данной реализации это не важно – проверяются не входные значения операций, а только выходные, поэтому не вызовет прерывания.
*RangeValidation> ab 20 + ab 0
20
*RangeValidation>
Но, вроде, как, и не красиво получается. Введём дополнительный класс
class Num' a b where
(+.) :: a -> b -> a
(-.) :: a -> b -> a
(*.) :: a -> b -> a
который реализует арифметику с операндами разного типа, и сделаем RgVld его экземпляром, определив
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 lo hi a
(RgVld l) -. r = chkVld "(-.)" $ (RgVld (l-r)) :: RgVld lo hi a
(RgVld l) *. r = chkVld "(*.)" $ (RgVld (l*r)) :: RgVld lo hi a
Функции (+.),(-.),(*.) схожи с обычными, но выполняют действия с диапазонным типом и обычным числом. Пример:
*RangeValidation> ab 5 -. (3 :: Int)
2
*RangeValidation>
— да, тип числа придётся указать явно, если это константа.
Естественно, диапазонный тип не обязан быть целым. Создадим вспомогательную функцию для определения уровня топлива.
fuel:: Double -> (RgVld 0 15 Double)
fuel = RgVld
И проверим работу диапазонного типа при дозаправке топливом:
*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>
— ай, яй, яй. Перелили!
К сожалению, «благодаря» ограничениям применяемой «технологии» — Type-Level Literals диапазон всё равно задаётся целыми числами. Может быть, авторы GHC её улучшат (хотя, вообще то она ими несколько для другого задумана). А пока будем рады и тому, с чем познакомились.
Код полного примера:
{-# 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 lo hi a
(RgVld l) - (RgVld r) = chkVld "(-)" $ (RgVld (l-r)) :: RgVld lo hi a
(RgVld l) * (RgVld r) = chkVld "(*)" $ (RgVld (l*r)) :: RgVld lo hi a
fromInteger n = chkVld "fromInteger" $ (RgVld (fromInteger n)) :: RgVld lo hi a
abs = id
signum (RgVld v) = (RgVld (signum v)) :: RgVld lo hi a
infixl 6 +.,-.
infixl 7 *.
class Num' a b 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 lo hi a
(RgVld l) -. r = chkVld "(-.)" $ (RgVld (l-r)) :: RgVld lo hi a
(RgVld l) *. r = chkVld "(*.)" $ (RgVld (l*r)) :: RgVld lo hi a
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 w s of
[] -> []
[(v,s')] -> [(chkVld "readsPrec" $ (RgVld v) :: RgVld lo hi a,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
Автор: KolodeznyDiver
