refined (empty) → 0.1.0.0

raw patch · 4 files changed

+267/−0 lines, 4 filesdep +basedep +base-preludedep +template-haskellsetup-changed

Dependencies added: base, base-prelude, template-haskell

Files

LICENSE +22/−0
Setup.hs +2/−0
library/Refined.hs +189/−0
refined.cabal +54/−0

+ LICENSE view

@@ -0,0 +1,22 @@+Copyright (c) 2015, Nikita Volkov++Permission is hereby granted, free of charge, to any person+obtaining a copy of this software and associated documentation+files (the "Software"), to deal in the Software without+restriction, including without limitation the rights to use,+copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the+Software is furnished to do so, subject to the following+conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES+OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT+HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,+WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR+OTHER DEALINGS IN THE SOFTWARE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ library/Refined.hs view

@@ -0,0 +1,189 @@+module Refined+(+  Refined,+  refine,+  refineTH,+  unrefine,+  -- * Predicate Interface+  Predicate(..),+  -- * Standard Predicates+  -- ** Logical+  Not,+  And,+  Or,+  -- ** Numeric+  LessThan,+  GreaterThan,+  EqualTo,+  Positive,+  Negative,+  ZeroToOne,+)+where++import BasePrelude+import GHC.TypeLits+import qualified Language.Haskell.TH.Syntax as TH+++-- |+-- A refinement type, +-- which wraps a value of type @x@,+-- ensuring that it satisfies a type-level predicate @p@.+newtype Refined p x =+  Refined x+  deriving (Show, Read, Eq, Ord, Typeable, Data, Generic)++instance TH.Lift x => TH.Lift (Refined p x) where+  lift (Refined a) =+    [|Refined a|]++-- |+-- A smart constructor of a 'Refined' value.+-- Checks the input value at runtime.+{-# INLINABLE refine #-}+refine :: forall p x. Predicate p x => x -> Either String (Refined p x)+refine x =+  maybe (Right (Refined x)) Left $+  validate (undefined :: p) x++-- |+-- Constructs a 'Refined' value with checking at compile-time using Template Haskell.+-- E.g.,+-- +-- >>> $$(refineTH 23) :: Refined Positive Int+-- Refined 23+-- +-- Here's an example of an ivalid value:+-- +-- >>> $$(refineTH 0) :: Refined Positive Int+-- <interactive>:6:4:+--     Value is not greater than 0+--     In the Template Haskell splice $$(refineTH 0)+--     In the expression: $$(refineTH 0) :: Refined Positive Int+--     In an equation for ‘it’:+--         it = $$(refineTH 0) :: Refined Positive Int+-- +-- If it's not evident, the example above indicates a compile-time failure, +-- which means that the checking was done at compile-time, +-- thus introducing a zero runtime overhead compared to a plain value construction.+refineTH :: forall p x. (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x))+refineTH =+  fmap TH.TExp . either fail TH.lift . (refine :: x -> Either String (Refined p x))++-- |+-- Extracts the refined value.+{-# INLINE unrefine #-}+unrefine :: Refined p x -> x+unrefine =+  unsafeCoerce+  ++-- * Predicate+-------------------------++-- |+-- A class which defines a runtime interpretation of+-- a type-level predicate @p@ for type @x@.+class Predicate p x where+  -- |+  -- Check the value @x@ according to the predicate @p@,+  -- producing an error string if the value does not satisfy.+  validate :: p -> x -> Maybe String+++-- * Rules+-------------------------+++-- ** Logical+-------------------------++-- |+-- A logical negation of a predicate.+data Not r++instance Predicate r x => Predicate (Not r) x where+  validate _ =+    maybe (Just "A subpredicate didn't fail") (const Nothing) .+    validate (undefined :: r)++-- |+-- A logical conjunction predicate, composed of two other predicates.+data And l r++instance (Predicate l x, Predicate r x) => Predicate (And l r) x where+  validate _ x =+    fmap (showString "The left subpredicate failed with: ") +         (validate (undefined :: l) x) +      <|>+    fmap (showString "The right subpredicate failed with: ") +         (validate (undefined :: r) x)++-- |+-- A logical disjunction predicate, composed of two other predicates.+data Or l r++instance (Predicate l x, Predicate r x) => Predicate (Or l r) x where+  validate _ x =+    case (validate (undefined :: l) x, validate (undefined :: r) x) of+      (Just a, Just b) -> +        Just $ "Both subpredicates failed. First with: " <> a <> ". Second with: " <> b <> "."+      _ -> +        Nothing+++-- ** Numeric+-------------------------++-- |+-- A predicate, which ensures that a value is less than the specified type-level number.+data LessThan (n :: Nat)++instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where+  validate p x =+    if x < fromIntegral x'+      then Nothing+      else Just ("Value is not less than " <> show x')+    where+      x' = natVal p++-- |+-- A predicate, which ensures that a value is greater than the specified type-level number.+data GreaterThan (n :: Nat)++instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where+  validate p x =+    if x > fromIntegral x'+      then Nothing+      else Just ("Value is not greater than " <> show x')+    where+      x' = natVal p++-- |+-- A predicate, which ensures that a value equals to the specified type-level number.+data EqualTo (n :: Nat)++instance (Ord x, Num x, KnownNat n) => Predicate (EqualTo n) x where+  validate p x =+    if x == fromIntegral x'+      then Nothing+      else Just ("Value does not equal " <> show x')+    where+      x' = natVal p++-- |+-- A predicate, which ensures that the value is greater than zero.+type Positive =+  GreaterThan 0++-- |+-- A predicate, which ensures that the value is less than zero.+type Negative = +  LessThan 0++-- |+-- A range of values from zero to one, including both.+type ZeroToOne =+  And (Not (LessThan 0)) (Not (GreaterThan 1))+

+ refined.cabal view

@@ -0,0 +1,54 @@+name:+  refined+version:+  0.1.0.0+synopsis:+  Refinement types with static and runtime checking+description:+  For an extensive introduction to the library please follow to +  <http://nikita-volkov.github.io/refined this blog-post>.+category:+  Data+homepage:+  https://github.com/nikita-volkov/refined+bug-reports:+  https://github.com/nikita-volkov/refined/issues +author:+  Nikita Volkov <nikita.y.volkov@mail.ru>+maintainer:+  Nikita Volkov <nikita.y.volkov@mail.ru>+copyright:+  (c) 2015, Nikita Volkov+license:+  MIT+license-file:+  LICENSE+build-type:+  Simple+cabal-version:+  >=1.10+++source-repository head+  type:+    git+  location:+    git://github.com/nikita-volkov/refined.git+++library+  hs-source-dirs:+    library+  other-modules:+  exposed-modules:+    Refined+  ghc-options:+    -funbox-strict-fields+  default-extensions:+    Arrows, BangPatterns, ConstraintKinds, DataKinds, DefaultSignatures, DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric, DeriveTraversable, EmptyDataDecls, FlexibleContexts, FlexibleInstances, FunctionalDependencies, GADTs, GeneralizedNewtypeDeriving, ImpredicativeTypes, LambdaCase, LiberalTypeSynonyms, MultiParamTypeClasses, MultiWayIf, NoImplicitPrelude, NoMonomorphismRestriction, OverloadedStrings, PatternGuards, ParallelListComp, QuasiQuotes, RankNTypes, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TemplateHaskell, TupleSections, TypeFamilies, TypeOperators+  default-language:+    Haskell2010+  build-depends:+    template-haskell >= 2.9 && < 3,+    base-prelude >= 0.1.19 && < 0.2,+    base >= 4.7 && < 5