diff --git a/Changelog.md b/Changelog.md new file mode 100644 --- /dev/null +++ b/Changelog.md @@ -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 diff --git a/exhaustive.cabal b/exhaustive.cabal --- a/exhaustive.cabal +++ b/exhaustive.cabal @@ -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 diff --git a/src/Control/Exhaustive.hs b/src/Control/Exhaustive.hs --- a/src/Control/Exhaustive.hs +++ b/src/Control/Exhaustive.hs @@ -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)) diff --git a/src/Control/Exhaustive/Internal.hs b/src/Control/Exhaustive/Internal.hs deleted file mode 100644 --- a/src/Control/Exhaustive/Internal.hs +++ /dev/null @@ -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))