exhaustive 1.0.0 → 1.1.0

raw patch · 4 files changed

+248/−163 lines, 4 filesdep +template-haskellPVP ok

version bump matches the API change (PVP)

Dependencies added: template-haskell

API changes (from Hackage documentation)

Files

• Changelog.md +9/−0
• exhaustive.cabal +9/−4
• src/Control/Exhaustive.hs +230/−25
• src/Control/Exhaustive/Internal.hs +0/−134

@@ -0,0 +1,9 @@+## 1.1.0++* New API new using Template Haskell to provide named constructors. Users should+  check the latest documentation for 'Control.Exhaustive' to see how the new API+  is used.++## 1.0.0++* Initial release

@@ -1,5 +1,5 @@ name:                exhaustive-version:             1.0.0+version:             1.1.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@@ -10,13 +10,18 @@ -- copyright: category:            Control build-type:          Simple--- extra-source-files:+extra-source-files: Changelog.md cabal-version:       >=1.10 +source-repository head+  type: git+  location: git://github.com/ocharles/exhaustive+ library-  exposed-modules:     Control.Exhaustive, Control.Exhaustive.Internal+  exposed-modules:     Control.Exhaustive   -- 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+  build-depends:       base >=4.7 && <4.8, generics-sop >=0.1 && <0.2, transformers >=0.3 && <0.4, template-haskell   hs-source-dirs:      src   default-language:    Haskell2010+  ghc-options: -Wall

@@ -1,3 +1,11 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+ {-|  `exhaustive` is a library that guarantees that when building a parser, or some@@ -60,41 +68,238 @@ considering all constructors:  @+    'makeExhaustive' ''Expr+     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'+    parseExpr =+      'produceFirst' '$'+        $('con' 'ETrue) '<$' symbol \"True\" '&:'+        $('con' 'EFalse) '<$' symbol \"False\" '&:'+        $('con' 'EIf) '<$>' (symbol \"if\" '*>' parseExpr)+                    '<*>' (symbol \"then\" '*>' parseExpr)+                    '<*>' (symbol \"else\" '*>' parseExpr) '&:'+        'finish' @  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.+2. Wrap each constructor application with the Template Haskell function+'con'. Note that you also need to quote the name of the constructor with a+single @'@.+3. Use '&:' to combine constructors, rather than list notation.+4. Explicitly state you are 'finish'ed.+5. Add a call to 'makeExhaustive' on our 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+module Control.Exhaustive+       (-- * Specifying Individual Constructions+        con,+        -- * Combining Constructions+        (&:), finish,+        -- * Producing Data+        produceM, produceFirst, produceAll,+        -- * Utilities+        makeExhaustive,+        -- * Implementation details+        -- | The following are implementation details, but exported to improve documentation.+        ConstructorApplication, Construction,+        Length)+       where  import Control.Applicative-import Control.Monad+import Data.Foldable+import Data.Maybe+import Data.Traversable+import GHC.TypeLits (Nat, type (+)) import Generics.SOP-import Control.Exhaustive.Internal+import Generics.SOP.NP+import Language.Haskell.TH+import Prelude hiding (foldr, sequence)++-- | Compute the length of a type level list.+type family Length (a :: [k]) :: Nat where+  Length '[] = 0+  Length (x ': xs) = 1 + Length xs++-- | A 'Construction' is an internal representation of a data type constructor. This type+-- is indexed by a natural number, which represents the constructor number,+-- and the list of types of fields of this constructor.+--+-- To create a 'Construction', use 'con'.+data Construction :: Nat -> [*] -> * where+  Construction :: NP I xs -> Construction n xs++-- | A 'ConstructorApplication' 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@.+--+-- To create and use 'ConstructorApplication's, use '&:'.+type ConstructorApplication f code = Injection (NP I) code -.-> K (f (NS (NP I) code))++name :: Con -> Name+name (NormalC n _) = n+name (RecC n _) = n+name (InfixC _ n _) = n+name (ForallC _ _ c) = name c++conFields :: Con -> [Type]+conFields (NormalC _ f) = map snd f+conFields (RecC _ f) = map (\(_, _, t) -> t) f+conFields (InfixC l _ r) = map snd [l,r]+conFields (ForallC _ _ c) = conFields c++typeVars :: [Type] -> [Name]+typeVars [] = []+typeVars (VarT v : vs) = v : typeVars vs+typeVars (_ : vs) = typeVars vs++parentName :: Info -> Maybe ParentName+parentName (DataConI _ _ parent _) = Just parent+parentName _ = Nothing++constructors :: Name -> Q (Maybe [Con])+constructors t =+  do info <- reify t+     case info of+       TyConI (DataD _ _ _ ctors _) ->+         return (Just ctors)+       TyConI (NewtypeD _ _ _ ctor _) ->+         return (Just [ctor])+       TyConI (DataInstD _ _ _ ctors _) ->+         return (Just ctors)+       TyConI (NewtypeInstD _ _ _ ctor _) ->+         return (Just [ctor])+       _ -> return Nothing+++-- | 'con' builds a 'Construction' for a single constructor of a data type.+-- Unfortunately, as this function is used via Template Haskell, the type+-- is not particularly informative -- though you can think of the produced+-- function having roughly the same type as the original constructor.+-- To clarify this, it's helpful to look at the type of 'con' applications:+--+-- @+--     $('con' \''Nothing') :: Construction 1 '[]+--     $('con' \''Just') :: a -> Construction 2 '[a]+--+--     data Record = Record { a :: String, b :: Int, c :: Char }+--     $('con' \'Record) :: String -> Int -> Char -> Construction 1 '[String, Int, Char]+-- @+--+-- For more examples of 'con', see the module documentation at the top of this page.+con :: Name -> Q Exp+con ctorName =+  do info <- reify ctorName+     parent <- maybe (fail (show ctorName ++ " is not a data type constructor"))+                     return+                     (parentName info)+     ctors <- maybe (fail ("Unable to determine constructors of " ++ show parent)) return =<<+              constructors parent+     let matching =+           filter ((ctorName ==) . name . snd)+                  (zip [0 ..] ctors)+     case matching of+       [] ->+         fail ("Failed to find constructor index of " ++ show ctorName)+       ((i,c):_) ->+         let fieldTypes = conFields c+             lambda =+               (do names <- sequence ((newName "x") <$+                                      fieldTypes)+                   return (LamE (VarP <$> names)+                                (AppE (ConE 'Construction)+                                      (foldr (\x y ->+                                                InfixE (Just x)+                                                       (ConE '(:*))+                                                       (Just y))+                                             (ConE 'Nil)+                                             (map (AppE (ConE 'I) .+                                                   VarE)+                                                  names)))))+             lType =+               (pure (ForallT (map PlainTV (typeVars fieldTypes))+                              []+                              (foldr (\l r ->+                                        AppT (AppT ArrowT l) r)+                                     (AppT (AppT (ConT ''Construction)+                                                 (LitT (NumTyLit (succ i))))+                                           (foldr (\l r ->+                                                     AppT (AppT PromotedConsT l) r)+                                                  PromotedNilT+                                                  fieldTypes))+                                     fieldTypes)))+         in sigE lambda lType+++-- | Signify that you will be performing exhaustive construction of a specific data type:+--+-- @+--     data Expr = ETrue | EFalse+--     makeExhaustive ''Expr+-- @+--+-- 'makeExhaustive' doesn't introduce any new symbols into scope, but it forces an+-- environment change, allowing you to write @$(con 'ETrue)@. If you are already using+-- other Template Haskell routines (such as @makeLenses@) then you can omit this call.+makeExhaustive :: Name -> Q [a]+makeExhaustive _ = return []++infixr 3 &:++-- | Combine multiple 'Construction's into a list of constructions for a data+-- type. This function is a lot like ':' for lists, but the types carry+-- considerably more information.+--+-- The type @n@ is used to carry the index of the constructor in the list of+-- constructors in the data type, while @xs@ is a list of types that are the+-- fields of that constructor.+--+-- The constraint on this function forces '&:' to be used to produce in-order+-- constructors. It may help to see this function through an example:+--+-- Given @data Bool = True | False@, we have two constructors. @True@ has index+-- 1, while the /code/ for this data type has length 2 (as there are two+-- constructors in total). Therefore after using the @True@ constructor we have to+-- use one more constructor. When we construct using @False@ we are done, as the+-- only way to satisfy the equation @2 + x = 2@ is to provide @x = 0@ -- the empty+-- list.+(&:) :: (Functor f, Length code ~ (n + Length xs))+     => f (Construction n x) -> NP (ConstructorApplication f code) xs -> NP (ConstructorApplication f code) (x ': xs)+(&:) f xs = construct f :* xs+  where construct constructed =+          Fn (\(Fn inject) ->+                (K (fmap (unK . inject . fields) constructed)))+        fields (Construction a) = a++-- | Assert that you have now used all constructors and are finished. If you've+-- made mistake, be prepared for a rather impressive type error!+finish :: NP f '[]+finish = Nil++-- | 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 (ConstructorApplication 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 (ConstructorApplication 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 (ConstructorApplication f code) code+  -> [f a]+produceM fs =+  map (fmap (to . SOP))+            (collapse_NP (fs `hap` injections))

@@ -1,134 +0,0 @@-{-# 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))