diff --git a/.travis.yml b/.travis.yml index a31174a..5715f2a 100644 --- a/.travis.yml +++ b/.travis.yml @@ -8,7 +8,7 @@ # # For more information, see https://github.com/haskell-CI/haskell-ci # -# version: 0.10.2 +# version: 0.10.3 # version: ~> 1.0 language: c @@ -42,15 +42,6 @@ jobs: - compiler: ghc-8.6.5 addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.6.5","cabal-install-3.2"]}} os: linux - - compiler: ghc-8.4.4 - addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.4.4","cabal-install-3.2"]}} - os: linux - - compiler: ghc-8.2.2 - addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.2.2","cabal-install-3.2"]}} - os: linux - - compiler: ghc-8.0.2 - addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.0.2","cabal-install-3.2"]}} - os: linux before_install: - HC=$(echo "/opt/$CC/bin/ghc" | sed 's/-/\//') - WITHCOMPILER="-w $HC" @@ -99,8 +90,8 @@ install: - touch cabal.project - | echo "packages: ." >> cabal.project - - if [ $HCNUMVER -ge 80200 ] ; then echo 'package constraints-extras' >> cabal.project ; fi - - "if [ $HCNUMVER -ge 80200 ] ; then echo ' ghc-options: -Werror=missing-methods' >> cabal.project ; fi" + - echo 'package constraints-extras' >> cabal.project + - "echo ' ghc-options: -Werror=missing-methods' >> cabal.project" - | - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(constraints-extras)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done" - cat cabal.project || true @@ -126,8 +117,8 @@ script: - touch cabal.project - | echo "packages: ${PKGDIR_constraints_extras}" >> cabal.project - - if [ $HCNUMVER -ge 80200 ] ; then echo 'package constraints-extras' >> cabal.project ; fi - - "if [ $HCNUMVER -ge 80200 ] ; then echo ' ghc-options: -Werror=missing-methods' >> cabal.project ; fi" + - echo 'package constraints-extras' >> cabal.project + - "echo ' ghc-options: -Werror=missing-methods' >> cabal.project" - | - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(constraints-extras)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done" - cat cabal.project || true @@ -146,5 +137,5 @@ script: - rm -f cabal.project.local - ${CABAL} v2-build $WITHCOMPILER --disable-tests --disable-benchmarks all -# REGENDATA ("0.10.2",["constraints-extras.cabal"]) +# REGENDATA ("0.10.3",["constraints-extras.cabal"]) # EOF diff --git a/ChangeLog.md b/ChangeLog.md index ffbde96..f02a683 100644 --- a/ChangeLog.md +++ b/ChangeLog.md @@ -13,6 +13,8 @@ * Allow deriving instances with `deriveArgDict` for data and newtype family instances by supplying the name of one of its constructors * Support GHC 9.0.1 +* Overhaul to allow working with recursive GADTs. + ## 0.3.0.3 - 2020-06-22 * Update version bounds for GHC 8.10 diff --git a/README.md b/README.md index 70d3557..c72a77c 100644 --- a/README.md +++ b/README.md @@ -5,42 +5,68 @@ Example usage: -------------- ```haskell - +> {-# LANGUAGE ConstraintKinds #-} +> {-# LANGUAGE ExistentialQuantification #-} +> {-# LANGUAGE FlexibleContexts #-} +> {-# LANGUAGE FlexibleInstances #-} > {-# LANGUAGE GADTs #-} > {-# LANGUAGE KindSignatures #-} +> {-# LANGUAGE LambdaCase #-} +> {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE PolyKinds #-} +> {-# LANGUAGE QuantifiedConstraints #-} > {-# LANGUAGE ScopedTypeVariables #-} > {-# LANGUAGE TemplateHaskell #-} > {-# LANGUAGE TypeApplications #-} > {-# LANGUAGE TypeFamilies #-} -> {-# LANGUAGE FlexibleContexts #-} -> {-# LANGUAGE FlexibleInstances #-} -> {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE UndecidableInstances #-} -> {-# LANGUAGE ExistentialQuantification #-} +> {-# LANGUAGE UndecidableSuperClasses #-} +> +> {-# OPTIONS_GHC -Wno-unused-top-binds #-} > > import Data.Aeson +> import Data.Constraint > import Data.Constraint.Forall > import Data.Constraint.Extras > import Data.Constraint.Extras.TH > +``` + +A "simple" GADT. + +```haskell > data A :: * -> * where > A_a :: A Int > A_b :: Int -> A () > > deriveArgDict ''A -> +``` + +A GADT which uses `A`. + + +```haskell > data B :: * -> * where > B_a :: A a -> A a -> B a > B_x :: Int -> B Int > > deriveArgDict ''B -> +``` + +A GADT which has a non-`Type` parameter. + + +```haskell > data V :: (* -> *) -> * where > V_a :: A Int -> V A > > deriveArgDict ''V -> +``` + +Now let's actually use them + + +```haskell > data DSum k f = forall a. DSum (k a) (f a) > > -- Derive a ToJSON instance for our 'DSum' @@ -62,7 +88,125 @@ Example usage: > Some (f :: f a) <- parseJSON jf > g <- has' @FromJSON @g f (parseJSON jg) > return $ DSum f g +``` + +We can hand-write an instance for there being non-finite indices. + + +```haskell +> data SimpleExpr :: * -> * where +> SimpleExpr_BoolLit :: Bool -> SimpleExpr Bool +> SimpleExpr_IntLit :: Int -> SimpleExpr Int +> -- crude non-empty list +> SimpleExpr_ListLit :: SimpleExpr a -> [SimpleExpr a] -> SimpleExpr [a] +> +> class +> ( c Int +> , c Bool +> , (forall a. (forall c'. ConstraintsFor SimpleExpr c' => c' a) => c [a]) +> ) => ConstraintsForSimpleExpr c +> instance +> ( c Int +> , c Bool +> , (forall a. (forall c'. ConstraintsFor SimpleExpr c' => c' a) => c [a]) +> ) => ConstraintsForSimpleExpr c > +> instance ArgDict SimpleExpr where +> type ConstraintsFor SimpleExpr c = ConstraintsForSimpleExpr c +> argDictAll = go +> where +> go :: forall c a. ConstraintsFor SimpleExpr c => SimpleExpr a -> Dict (c a) +> go = \case +> SimpleExpr_BoolLit _ -> Dict +> SimpleExpr_IntLit _ -> Dict +> SimpleExpr_ListLit h _ -> hasAll h Dict +``` + +We have the instances we want: + + +```haskell +> abstractConstraintWitnesses :: Has c SimpleExpr => Dict (c Int, c Bool, c [Int], c [Bool], c [[Int]], c [[Bool]]) +> abstractConstraintWitnesses = Dict +``` + + +```haskell +> concreteClassSmokeTest :: Dict (Has Show SimpleExpr) +> concreteClassSmokeTest = Dict +``` + +Even in when we have no "slack" (instances beyond what `Has` requires): + + +```haskell +> class Minimal a +> instance Minimal Int +> instance Minimal Bool +> instance Minimal a => Minimal [a] +``` + +```haskell +> minimalWitness :: Dict (Has Minimal SimpleExpr) +> minimalWitness = Dict + +The funny "Leibnitz-style" `forall c'` is so fancier things than Minimal +(which also might not be satisfied for other args) also work: + + +```haskell +> class MinimalPing a +> class MinimalPong a +> instance MinimalPing Int +> instance MinimalPong Int +> instance MinimalPing Bool +> instance MinimalPong Bool +> instance MinimalPing a => MinimalPong [a] +> instance MinimalPong a => MinimalPing [a] + +> minimalPingPongWitness :: Dict (Has MinimalPing SimpleExpr, Has MinimalPong SimpleExpr) +> minimalPingPongWitness = Dict +``` + +We can also hand-write instances which take advantage of constructor's dictionaries + +```haskell +> data WithOrd a where +> WithOrd :: Ord a => WithOrd a +> +> -- class to avoid impredicativity +> class (forall a. Ord a => c a) => ConstraintsForWithOrd c +> instance (forall a. Ord a => c a) => ConstraintsForWithOrd c +> +> instance ArgDict WithOrd where +> type ConstraintsFor WithOrd c = ConstraintsForWithOrd c +> argDictAll WithOrd = Dict +``` + +Now we can use the constructor dictionary to discharge constraints. +We can get out `Ord a`: + + +```haskell +> useThisOrd :: WithOrd a -> a -> a -> Ordering +> useThisOrd wo x y = has @Ord wo $ x `compare` y +``` + +and things derivable from it: + + +```haskell +> useThisOrdImplication :: WithOrd a -> [a] -> [a] -> (Bool, Bool) +> useThisOrdImplication wo x y = +> ( has @Ord wo $ x == y -- implicit way +> , has' @Eq @[] wo $ x == y -- explicit way +> ) +``` + +Oh, and let's make this README build + + +```haskell > main :: IO () > main = return () ``` diff --git a/constraints-extras.cabal b/constraints-extras.cabal index c05e158..199f2e8 100644 --- a/constraints-extras.cabal +++ b/constraints-extras.cabal @@ -1,5 +1,5 @@ name: constraints-extras -version: 0.3.2.0 +version: 0.4 synopsis: Utility package for constraints description: Convenience functions and TH for working with constraints. See for example usage. category: Constraints @@ -13,7 +13,7 @@ copyright: Obsidian Systems LLC build-type: Simple cabal-version: 2.0 tested-with: - GHC ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1 || ==8.10.1 || ==9.0.1 || ==9.2.1 + GHC ==8.6.5 || ==8.8.1 || ==8.10.1 || ==9.0.1 || ==9.2.1 extra-source-files: README.md ChangeLog.md diff --git a/src/Data/Constraint/Extras.hs b/src/Data/Constraint/Extras.hs index 97228f6..1d39e81 100644 --- a/src/Data/Constraint/Extras.hs +++ b/src/Data/Constraint/Extras.hs @@ -1,12 +1,14 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoStarIsType #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} @@ -37,6 +39,7 @@ module Data.Constraint.Extras -- * Bringing instances into scope , Has , has + , hasAll , Has' , has' , HasV @@ -56,7 +59,7 @@ import Data.Functor.Sum (Sum(..)) import Data.Kind import GHC.Generics ((:+:)(..)) --- | Morally, this class is for GADTs whose indices can be finitely +-- | Morally, this class is for GADTs whose indices can be recursively -- enumerated. An @'ArgDict' c f@ instance allows us to do two things: -- -- 1. 'ConstraintsFor' requests the set of constraints @c a@ for all @@ -66,30 +69,44 @@ import GHC.Generics ((:+:)(..)) -- -- Use 'Data.Constraint.Extras.TH.deriveArgDict' to derive instances -- of this class. -class ArgDict (c :: k -> Constraint) (f :: k -> Type) where +-- +-- One law on this class is: +-- +-- > (forall c. (forall a. c a) => ConstraintsForC f c) +-- +-- This provides and upper bound for what '@ConstraintsFor@ f c' requires. in +-- the most general case, all types are possible GADT indices, so we should +-- always be able to '@ConstraintsFor@ f c' from 'forall a. c a'. This law +-- is implemented as a super class. +class + (forall c. (forall a. c a) => ConstraintsForC f c) + => ArgDict (f :: k -> Type) where -- | Apply @c@ to each possible type @a@ that could appear in a @f a@. -- -- > ConstraintsFor Show Tag = (Show Int, Show Bool) - type ConstraintsFor f c :: Constraint + type ConstraintsFor f (c :: k -> Constraint) :: Constraint - -- | Use an @f a@ to select a specific dictionary from @ConstraintsFor f c@. + -- | Use an @f a@ to select a "function dictionary" demonstrating + -- @ConstraintsFor f c@ contains @c a@. -- - -- > argDict I :: Dict (Show Int) - argDict :: ConstraintsFor f c => f a -> Dict (c a) + -- @argDict@ is sufficient for most tasks, but this is slightly more powerful + -- in that this discharges the quantified constraints which are useful when + -- the GADT indices are not finite. + argDictAll :: f a -> Dict (Extract f a) -- | @since 0.3.2.0 -instance (ArgDict c f, ArgDict c g) => ArgDict c (f :+: g) where +instance (ArgDict f, ArgDict g) => ArgDict (f :+: g) where type ConstraintsFor (f :+: g) c = (ConstraintsFor f c, ConstraintsFor g c) - argDict = \case - L1 f -> argDict f - R1 g -> argDict g + argDictAll = \case + L1 f -> weakenContra (argDictAll f) + R1 g -> weakenContra (argDictAll g) -- | @since 0.3.2.0 -instance (ArgDict c f, ArgDict c g) => ArgDict c (Sum f g) where +instance (ArgDict f, ArgDict g) => ArgDict (Sum f g) where type ConstraintsFor (Sum f g) c = (ConstraintsFor f c, ConstraintsFor g c) - argDict = \case - InL f -> argDict f - InR g -> argDict g + argDictAll = \case + InL f -> weakenContra (argDictAll f) + InR g -> weakenContra (argDictAll g) -- | \"Primed\" variants (@ConstraintsFor'@, 'argDict'', 'Has'', -- 'has'', &c.) use the 'ArgDict' instance on @f@ to apply constraints @@ -100,34 +117,62 @@ instance (ArgDict c f, ArgDict c g) => ArgDict c (Sum f g) where -- > ConstraintsFor' Tag Show Identity = (Show (Identity Int), Show (Identity Bool)) type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g) +-- | Helper class to avoid restrictions on type families +class ConstraintsFor f c => ConstraintsForC f c +instance ConstraintsFor f c => ConstraintsForC f c + +-- | Helper class to avoid impredicative type +class (forall c. ConstraintsForC f c => c a) => Extract f a +instance (forall c. ConstraintsForC f c => c a) => Extract f a + +weakenContra + :: forall f g a + . (forall c. ConstraintsForC g c => ConstraintsForC f c) + => Dict (Extract f a) -> Dict (Extract g a) +weakenContra Dict = Dict + +-- | Use an @f a@ to select a specific dictionary from @ConstraintsFor f c@. +-- +-- > argDict I :: Dict (Show Int) +argDict :: forall f c a. Has c f => f a -> Dict (c a) +argDict tag = case argDictAll tag of + (Dict :: Dict (Extract f a)) -> Dict + -- | Get a dictionary for a specific @g a@, using a value of type @f a@. -- -- > argDict' B :: Dict (Show (Identity Bool)) -argDict' :: forall f c g a. (Has' c f g) => f a -> Dict (c (g a)) +argDict' :: forall f c g a. Has' c f g => f a -> Dict (c (g a)) argDict' tag = case argDict tag of (Dict :: Dict (ComposeC c g a)) -> Dict type ConstraintsForV (f :: (k -> k') -> Type) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g) -argDictV :: forall f c g v. (HasV c f g) => f v -> Dict (c (v g)) +argDictV :: forall f c g v. (ArgDict f, ConstraintsForV f c g) => f v -> Dict (c (v g)) argDictV tag = case argDict tag of (Dict :: Dict (FlipC (ComposeC c) g a)) -> Dict {-# DEPRECATED ArgDictV "Just use 'ArgDict'" #-} -type ArgDictV f c = ArgDict f c +type ArgDictV f = ArgDict f -- | @Has c f@ is a constraint which means that for every type @a@ -- that could be applied to @f@, we have @c a@. -- -- > Has Show Tag = (ArgDict Show Tag, Show Int, Show Bool) -type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c) +type Has (c :: k -> Constraint) f = (ArgDict f, ConstraintsFor f c) -- | @Has' c f g@ is a constraint which means that for every type @a@ -- that could be applied to @f@, we have @c (g a)@. -- -- > Has' Show Tag Identity = (ArgDict (Show . Identity) Tag, Show (Identity Int), Show (Identity Bool)) -type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict (ComposeC c g) f, ConstraintsFor' f c g) -type HasV c f g = (ArgDict (FlipC (ComposeC c) g) f, ConstraintsForV f c g) +type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict f, ConstraintsFor' f c g) +type HasV c f g = (ArgDict f, ConstraintsForV f c g) + +-- | More powerful version of @has@. +-- +-- As @has@ is to @argDict@, so @hasAll@ is to @argDictAll@. See the +-- documentation for @argDictAll@ for why one might need this. +hasAll :: forall f a r. ArgDict f => f a -> ((forall c. Has c f => c a) => r) -> r +hasAll k r | (Dict :: Dict (Extract f a)) <- argDictAll k = r -- | Use the @a@ from @f a@ to select a specific @c a@ constraint, and -- bring it into scope. The order of type variables is chosen to work diff --git a/src/Data/Constraint/Extras/TH.hs b/src/Data/Constraint/Extras/TH.hs index 16aea5e..a9a0574 100644 --- a/src/Data/Constraint/Extras/TH.hs +++ b/src/Data/Constraint/Extras/TH.hs @@ -14,24 +14,24 @@ import Language.Haskell.TH deriveArgDict :: Name -> Q [Dec] deriveArgDict n = do (typeHead, constrs) <- getDeclInfo n + ts <- gadtIndices constrs c <- newName "c" - ts <- gadtIndices c constrs let xs = flip map ts $ \case Left t -> AppT (AppT (ConT ''ConstraintsFor) t) (VarT c) Right t -> (AppT (VarT c) t) l = length xs constraints = foldl AppT (TupleT l) xs - [d| instance ArgDict $(varT c) $(pure typeHead) where + [d| instance ArgDict $(pure typeHead) where type ConstraintsFor $(pure typeHead) $(varT c) = $(pure constraints) - argDict = $(LamCaseE <$> matches c constrs 'argDict) + argDictAll = $(LamCaseE <$> matches constrs 'argDictAll) |] {-# DEPRECATED deriveArgDictV "Just use 'deriveArgDict'" #-} deriveArgDictV :: Name -> Q [Dec] deriveArgDictV = deriveArgDict -matches :: Name -> [Con] -> Name -> Q [Match] -matches c constrs argDictName = do +matches :: [Con] -> Name -> Q [Match] +matches constrs argDictName = do x <- newName "x" fmap concat $ forM constrs $ \case GadtC [name] _ _ -> return $ @@ -39,7 +39,7 @@ matches c constrs argDictName = do ForallC _ _ (GadtC [name] bts (AppT _ (VarT b))) -> do ps <- forM bts $ \case (_, AppT t (VarT b')) | b == b' -> do - hasArgDictInstance <- not . null <$> reifyInstances ''ArgDict [VarT c, t] + hasArgDictInstance <- not . null <$> reifyInstances ''ArgDict [t] return $ if hasArgDictInstance then Just x else Nothing @@ -53,7 +53,9 @@ matches c constrs argDictName = do Nothing -> WildP : rest done Just _ -> VarP v : rest True pat = foldr patf (const []) ps False - in [Match (conPCompat name pat) (NormalB $ AppE (VarE argDictName) (VarE v)) []] + eta = CaseE (AppE (VarE argDictName) (VarE v)) + [Match (RecP 'Dict []) (NormalB $ ConE 'Dict) []] + in [Match (conPCompat name pat) (NormalB eta) []] ForallC _ _ (GadtC [name] _ _) -> return $ [Match (RecP name []) (NormalB $ ConE 'Dict) []] a -> error $ "deriveArgDict matches: Unmatched 'Dec': " ++ show a @@ -105,12 +107,12 @@ getDeclInfo n = reify n >>= \case a -> error $ "getDeclInfo: Unmatched parent of data family instance: " ++ show a a -> error $ "getDeclInfo: Unmatched 'Info': " ++ show a -gadtIndices :: Name -> [Con] -> Q [Either Type Type] -gadtIndices c constrs = fmap concat $ forM constrs $ \case +gadtIndices :: [Con] -> Q [Either Type Type] +gadtIndices constrs = fmap concat $ forM constrs $ \case GadtC _ _ (AppT _ typ) -> return [Right typ] ForallC _ _ (GadtC _ bts (AppT _ (VarT _))) -> fmap concat $ forM bts $ \case (_, AppT t (VarT _)) -> do - hasArgDictInstance <- fmap (not . null) $ reifyInstances ''ArgDict [VarT c, t] + hasArgDictInstance <- fmap (not . null) $ reifyInstances ''ArgDict [t] return $ if hasArgDictInstance then [Left t] else [] _ -> return [] ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]