packages feed

exhaustive (empty) → 1.0.0

raw patch · 5 files changed

+288/−0 lines, 5 filesdep +basedep +generics-sopdep +transformerssetup-changed

Dependencies added: base, generics-sop, transformers

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Oliver Charles++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Oliver Charles nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ exhaustive.cabal view
@@ -0,0 +1,22 @@+name:                exhaustive+version:             1.0.0+synopsis:            Compile time checks that a computation considers producing data through all possible constructors+description: For a brief tutorial to @exhaustive@, check out the documentation for "Control.Exhaustive", which contains a small example.+homepage:            http://github.com/ocharles/exhaustive+license:             BSD3+license-file:        LICENSE+author:              Oliver Charles+maintainer:          ollie@ocharles.org.uk+-- copyright:+category:            Control+build-type:          Simple+-- extra-source-files:+cabal-version:       >=1.10++library+  exposed-modules:     Control.Exhaustive, Control.Exhaustive.Internal+  -- other-modules:+  other-extensions:    ConstraintKinds, FlexibleContexts, FlexibleInstances, FunctionalDependencies, GADTs, RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances+  build-depends:       base >=4.7 && <4.8, generics-sop >=0.1 && <0.2, transformers >=0.3 && <0.4+  hs-source-dirs:      src+  default-language:    Haskell2010
+ src/Control/Exhaustive.hs view
@@ -0,0 +1,100 @@+{-|++`exhaustive` is a library that guarantees that when building a parser, or some+other computation that produces data, /all/ possible constructors in a data type+are considered. You can think of this library as providing a symmetry to GHC's+built in @-fwarn-incomplete-patterns@ compile time warning, although this+library is stricter in that it produces compile time errors if a constructor is+omitted.++Usage of this library is intended to be straightforward, though admittedly the+types might have you think the opposite! To understand this library, an example+may be helpful.++To begin with, consider a simple data type for a "boolean expressions" language:++@+   import qualified "GHC.Generics" as GHC++   data Expr+     = ETrue+     | EFalse+     | EIf Expr Expr Expr+     deriving ('Eq', GHC.'GHC.Generic')+   instance 'Generic' Expr+@++Note that we have to make our data type an instance of both+"GHC.Generics".'GHC.Generics.Generic' /and/ "Generics.SOP".'Generic', though this only requires+boiler-plate code.++Next, we would like to build a parser for this language. Let's assume that we+have access to a @parsec@-like library, where we have one basic combinator:++* @symbol :: 'String' -> Parser 'String'@++Ordinarily, we would write our parser as++@+    parseExpr :: Parser Expr+    parseExpr = 'msum' [ETrue '<$' symbol \"True\"+                     ,EFalse '<$' symbol \"False\"+                     ,EIf '<$>' symbol \"if\" '*>' parseExpr+                          '<*>' symbol \"then\" '*>' parseExpr+                          '<*>' symbol \"else\" '*>' parseExpr+                     ]+@++However, nothing is making sure that we actually considered all constructors in+@Expr@. We could just as well write++@+    parseExpr :: Parser Expr+    parseExpr = 'msum' [ETrue '<$' symbol \"True\"+                     ,EFalse '<$' symbol \"False\"]+@++Although this is significantly less useful!++Using @exhaustive@, we can get exhaustivity checks that we are at least+considering all constructors:++@+    parseExpr :: Parser Expr+    parseExpr = 'produceFirst' '$'+      'construct' (\\f -> f '<$' symbol \"True\") ':*'+      'construct' (\\f -> f '<$' symbol \"False\") ':*'+      'construct' (\\f -> f '<$'> symbol "if" '*>' parseExpr+                         '<*>' symbol "then" '*>' parseExpr+                         '<*>' symbol "else" '*>' parseExpr) ':*'+      'Nil'+@++As you can hopefully see, @exhaustive@ requires only minimal changes to an+existing parser. Specifically, we need to:++1. Use 'produceFirst' instead of 'msum'+2. Wrap each constructor application with 'construct'.+3. Use the provided constructor function, rather than the named constructors in+the original data type.++-}+module Control.Exhaustive+  ( -- * Producing data+    -- | The following are the main entry points to the API, all providing functionality to produce data.+    produceM+  , produceFirst+  , produceAll++    -- * Constructing Data+    -- | In order to produce data, you need a way to construct it - once for each constructor in a data type.+  , construct++    -- * Re-exported+  , Generic)+  where++import Control.Applicative+import Control.Monad+import Generics.SOP+import Control.Exhaustive.Internal
+ src/Control/Exhaustive/Internal.hs view
@@ -0,0 +1,134 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+module Control.Exhaustive.Internal+  (Constructor, Producer, FunctorStack, produceM, produceFirst, produceAll, construct, Apply, apply )+  where++import Data.Maybe+import Data.Traversable+import Control.Applicative+import Data.Foldable+import Generics.SOP+import Generics.SOP.NP+import Data.Functor.Compose+import Generics.SOP.Constraint++-- | Internal machinery to build n-ary functions. As a user of `exhaustive`, you+-- generally shouldn't need to worry about this type class, other than knowing+-- that the type variable @b@ will correspond to a function of all types+-- mentioned in @a@.+class Functor f => Apply f a b | f a -> b where+  apply :: f a -> b++instance Apply ((->) a) b (a -> b) where+  apply = id++instance Apply I b b where+  apply (I a) = a++instance (Apply g a b,Apply f b c) => Apply (Compose f g) a c where+  apply (Compose x) = apply (fmap apply x)++-- | A 'Producer' is a lifted function (in the terms of @generics-sop@) that+-- instantiates a particular constructor of a data type, possibly using+-- the side-effects provided by @f@.+--+-- Most users will want to create 'Producer's using the smart constructor+-- 'construct'.+type Producer f code = Injection (NP I) code -.-> K (f (NS (NP I) code))++-- | A 'Constructor' is an n-ary function from all fields of a specific+-- constructor in a data type, to a generic representation.+type Constructor fields = forall r. Apply (FunctorStack fields) (NP I fields) r => r++-- | 'construct' builds a 'Producer' for a single constructor of a data type.+-- As you can see, the type is a little scary - but there are a few main parts+-- that will interest you, while the rest are unfortunate implementation+-- details.+--+-- * @f@ is the type of functor who's side effects you can use. For example,+-- you can choose @f@ to be 'IO', @(MyEnv ->)@, or even more complex+-- monad transformer stacks.+--+-- * @fields@ is a list of types that are used in the constructor.+--+--     As an example, given the data type+--+--     @data User = User { name :: 'String', age :: 'Int'}@+--+--     then @fields@ will correspond to @['String', 'Int']@.+--+-- The 'Constructor' argument is what you use to actually create your data type.+-- A 'Constructor' is an n-ary function from all field types. Continuing the+-- example with @User@ above, we would have+--+-- @Constructor fields@ == @Text -> Int -> out@+--+-- Thus a complete call to 'construct' would be+--+-- @'construct' (\\f -> f '<$>' parseName '<*>' parseAge)@+--+-- For a complete example of how this all fits together, user's are pointed+-- to the example at the top of this page.+construct :: forall fields code f.+             (Applicative f,SingI fields)+          => (Constructor fields -> f (NP I fields)) -> Producer f code fields+construct applyCtor =+  Fn (\(Fn f) ->+        (K (fmap (unK . f)+                 (applyCtor (apply (buildF (shape :: Shape fields)))))))++-- | This type family is internal, but provides the building block for building+-- n-ary functions. Most users will probably not need to work with this+-- directly.+type family FunctorStack (args :: [*]) :: * -> * where+  FunctorStack '[] = I+  FunctorStack (a ': as) = Compose ((->) a) (FunctorStack as)++data Dict (k :: Constraint) where+  Dict :: k => Dict k++-- | Prove that a 'FunctorStack' really is a 'Functor'.+isAFunctor :: Shape xs -> Dict (Functor (FunctorStack xs))+isAFunctor ShapeNil = Dict+isAFunctor (ShapeCons s) = case isAFunctor s of Dict -> Dict++-- | Given a list of types, build a stack of reader functors that represents+-- an n-ary function of all of those types.+buildF :: Functor (FunctorStack xs) => Shape xs -> FunctorStack xs (NP I xs)+buildF ShapeNil = I Nil+buildF (ShapeCons s) = Compose (\x -> case isAFunctor s of Dict -> fmap (I x :*) (buildF s))++-- | Keep attempting to construct a data type until a constructor succeeds. The+-- first constructor to successfully be constructed (in the order defined in the+-- original data type) will be returned, or 'empty' if all constructions fail.+produceFirst+  :: (code ~ Code a, SingI code, Generic a, Alternative f)+  => NP (Producer f code) code -> f a+produceFirst = asum . produceM++-- | Produce all successful constructions of a data-type. If any constructors+-- fail, they will not be included in the resulting list. If all constructors+-- fail, this will return 'pure' '[]'.+produceAll+  :: (code ~ Code a, SingI code, Generic a, Alternative f)+  => NP (Producer f code) code -> f [a]+produceAll = fmap catMaybes . sequenceA . map optional . produceM++-- | Build a list of computations, one for each constructor in a data type.+produceM+  :: (code ~ Code a, SingI code, Generic a, Applicative f)+  => NP (Producer f code) code+  -> [f a]+produceM fs =+  map (fmap (to . SOP))+            (collapse_NP (fs `hap` injections))