Известно, что функциональное программирование (ФП) помогает писать надежный (безошибочный) код. Ясно, что это максима.
Не бывает программ без ошибок.
Однако ФП в сочетании со строгой статической типизацией и развитием системы типов позволяет в значительной степени выявить неизбежные ошибки программиста на этапе компиляции.
Я говорю о Haskell, хотя, возможно, это относится и к OCaml. Однако если мы возьмемся писать надежный код, мы сразу обнаружим, что возможности Haskell не безграничны.
Не все, что существует для этой цели (построение безопасного кода) в других языках, легко реализуется в Haskell. Хорошо бы здесь поправиться, но, увы.
В первую очередь, конечно, следует обратить внимание на язык Ada, специально созданный для надежного кодирования (в меньшей степени, родственный ему Pascal).
И хотя идеология Ады, на мой взгляд, давно устарела, синтаксис напоминает окаменелости из 80-х, а некоторые идеи, якобы повышающие безопасность кода, сейчас вызывают у меня смех.
Несмотря на все это, в Ada имеется развитая система статической и динамической проверки данных для заданных условий ( валидация данных , проверка ограничений ).
Проще говоря, каждый раз, когда обновляется переменная, компилятор может добавить к выходному коду выполнение указанной нами проверки.
Самый простой и распространенный случай: проверка диапазона – значение выходит за указанные пределы.
В Паскале тоже есть такой контроль.
Не претендуя на замену Ады (это стандарт в армии, в авионике и т.д.), мы попытаемся приблизиться к стандартам безопасности Ады, выполнив для начала: проверка диапазона в Хаскеле.
Очевидно, что вам необходимо перегрузить арифметические функции (как минимум) класса Число , настроив их контролировать диапазон и выдавать исключения при выходе за его пределы.
Сразу сталкиваемся с проблемой — в арифметических функциях класса Num вида
нет места для установки границ проверяемого диапазона.(+) :: a -> a -> a
Что может быть сделано? Опция 1 .
Создайте запись из трёх чисел — границ диапазона и обрабатываемого значения и определите (создайте экземпляр) для такой записи Число .
Недостаток очевиден.
Нам нужно было бы хранить границы диапазона только в одном экземпляре для каждого типа, а не для каждого значения (которых может быть 100 000).
Вариант 2 .
Мы можем определить проверки жестких границ в классе, созданном с использованием Template Haskell. Этот вариант вполне возможен.
С TH мы можем все.
Но давайте попробуем найти способ установить границы диапазона во время компиляции каким-нибудь другим способом.
Вариант 3 .
Относительно недавно, начиная с GHC 7.8, если я не путаю, появилась возможность под названием Литералы уровня типа , т.е.
указание констант в описаниях типов, которые к тому же можно использовать в функциях.
Давайте попробуем реализовать проверка диапазона используя этот механизм.
Для контролируемого числа мы не будем экономически создавать полный тип данных; мы напишем тот, который потребует меньше накладных расходов во время выполнения, newtype. newtype RgVld (lo :: Nat) (hi :: Nat) a = RgVld { unRgVld :: a }
deriving (Eq, Ord)
RgVld — это аббревиатура от проверка диапазона .
А вот И привет , имеющий тип Нат (определено в GHC.TypeLits ) — это те же константы в определении типа — границы диапазона.
Здесь они целые числа (преобразованные в Integer, но, увы, не могут быть отрицательными).
Есть еще строковые — но описывать ограничения строкой и конвертировать их в строки во время выполнения — нет, в скрипте не пишем.
Собственно, этот тип и есть суть реализации проверка диапазона .
Для него теперь вы можете создать: 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 $ l-r
(RgVld l) * (RgVld r) = chkVld "(*)" $ RgVld $ l*r
fromInteger n = chkVld "fromInteger" $ RgVld $ fromInteger n
abs = id
signum (RgVld v) = RgVld $ signum v
Сорт ЗнайНат также определено в 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
Для типа РгВлд давайте реализуем классы одновременно Показывать , Читать , и довольно простой, но явно полезный в данном случае Ограниченный .
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, 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)
Т.
к.
мы говорили о языке Ада, который прочно ассоциируется с «военным», то будем считать, что наша программа управляет МБР с разделяющейся боеголовкой.
Допустим, они нумеруются начиная с единицы, но всего их 20, и каждый, естественно, несет атомную бомбу – А-бомбу, «йич-бомбу».
Давайте сократим его до 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 l) -.
r = chkVld "(-.
)" $ RgVld $ l-r (RgVld l) *.
r = chkVld "(*.
)" $ RgVld $ l*r
Функции (+.
),(-.
),(*.
) аналогичны обычным, но они работают с типами диапазонов и обычными числами.
Пример: *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>
- О, нет, нет, нет. Они налили!
К сожалению, "благодаря" ограничениям используемой "технологии" - Литералы уровня типа диапазон по-прежнему задается целыми числами.
Может авторы 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 l) - (RgVld r) = chkVld "(-)" $ RgVld $ l-r (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' 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 l) -.
r = chkVld "(-.
)" $ RgVld $ l-r (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 w s 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
Теги: #haskell #Литералы уровня типа #проверка диапазона #haskell
-
Сравнение Opengl И Direct3D
19 Oct, 24 -
Конец Работы - Портал 2 Вышел
19 Oct, 24
