История изменений
Исправление qnikst, (текущая версия) :
мне лень искать корень дискуссии:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
module Percent where
import GHC.TypeLits
import Data.Proxy
import Data.Function
data Percent (a :: Nat) where
Percent :: (KnownNat a, a <= 100) => Percent a
deriving instance Show (Percent a)
percent :: (KnownNat a, a <= 100) => Proxy a -> Percent a
percent = const $ Percent
unwrap :: KnownNat a => Percent a -> Integer
unwrap = natVal
sum1 :: (KnownNat (a+b), a + b <= 100) => Percent a -> Percent b -> Percent (a + b)
sum1 _ _ = Percent
toSome :: KnownNat a => Percent a -> SomePercent
toSome p = SomePercent $ SomeNat (toProxy p)
where toProxy :: Percent a -> Proxy a
toProxy g = Proxy
data SomePercent = SomePercent SomeNat
unwrapSome :: SomePercent -> Integer
unwrapSome (SomePercent (SomeNat x)) = natVal x
-- unwrapSome $ SomePercent (Percent :: Percent 70)
mkPercent :: Integer -> Maybe SomePercent
mkPercent i
| i >= 0 && i < 100 = fmap SomePercent (someNatVal i)
| otherwise = Nothing
sum2 :: SomePercent -> SomePercent -> Maybe SomePercent
sum2 = (mkPercent .). (+) `on` unwrapSome
тут есть тип «проценты» (на самом деле это просто тип чисел от 0 до 100). Соотв для известных на этапе компиляции все будет выполняться и работать, проверяя при этом арифметику без выполнения программы. Для данных получаемых из-вне и неизвестных, нужно явно использовать SomePercent (и никаких дурацких ворнингов). Реализация наверняка не идеальная, но покактит. Так же можно поизвращаться и выдавать SomePercent constraint, где constraint это всякие ограничения типа (<=50). Естественно проверка в компайлтайме без запуска программы.
Исходная версия qnikst, :
мне лень искать корень дискуссии:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
module Percent where
import GHC.TypeLits
import Data.Proxy
import Data.Function
data Percent (a :: Nat) where
Percent :: (KnownNat a, a <= 100) => Percent a
deriving instance Show (Percent a)
percent :: (KnownNat a, a <= 100) => Proxy a -> Percent a
percent = const $ Percent
unwrap :: KnownNat a => Percent a -> Integer
unwrap = natVal
sum1 :: (KnownNat (a+b), a + b <= 100) => Percent a -> Percent b -> Percent (a + b)
sum1 _ _ = Percent
toSome :: KnownNat a => Percent a -> SomePercent
toSome p = SomePercent $ SomeNat (toProxy p)
where toProxy :: Percent a -> Proxy a
toProxy g = Proxy
data SomePercent = SomePercent SomeNat
unwrapSome :: SomePercent -> Integer
unwrapSome (SomePercent (SomeNat x)) = natVal x
-- unwrapSome $ SomePercent (Percent :: Percent 70)
mkPercent :: Integer -> Maybe SomePercent
mkPercent i
| i >= 0 && i < 100 = fmap SomePercent (someNatVal i)
| otherwise = Nothing
sum2 :: SomePercent -> SomePercent -> Maybe SomePercent
sum2 = (mkPercent .). (+) `on` unwrapSome
тут есть тип «проценты» (на самом деле это просто тип чисел от 0 до 100). Соотв для известных на этапе компиляции все будет выполняться и работать, проверяя при этом арифметику без выполнения программы. Для данных получаемых из-вне и неизвестных, нужно явно использовать SomePercent (и никаких дурацких ворнингов). Реализация наверняка не идеальная, но покактит. Так же можно поизвращаться и выдавать SomePercent constraint, где constraint это всякие ограничения типа (<=50). Естественно проверка в компайлтайме без запуска программы.