constraints-extras 0.2.0.0 → 0.2.1.0

raw patch · 4 files changed

+65/−32 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• ChangeLog.md +0/−5
• constraints-extras.cabal +1/−2
• src/Data/Constraint/Extras.hs +19/−1
• src/Data/Constraint/Extras/TH.hs +45/−24

@@ -1,5 +0,0 @@-# Revision history for argdict--## 0.1.0.0  -- YYYY-mm-dd--* First version. Released on an unsuspecting world.

@@ -1,5 +1,5 @@ name: constraints-extras-version: 0.2.0.0+version: 0.2.1.0 synopsis: Utility package for constraints license: BSD3 license-file: LICENSE@@ -7,7 +7,6 @@ maintainer: maintainer@obsidian.systems copyright: Obsidian Systems LLC build-type: Simple-extra-source-files: ChangeLog.md cabal-version: >=1.10  library

@@ -13,15 +13,29 @@ import Data.Constraint import Data.Constraint.Forall --- | Provides proof of the existence of a constraint on a GADT+-- | Morally, this class is for GADTs whose indices can be finitely enumerated. It provides operations which will+-- select the appropriate type class dictionary from among a list of contenders based on a value of the type.+-- There are a few different variations of this which we'd like to be able to support, and they're all implemented+-- in the same fashion at the term level, by pattern matching on the constructors of the GADT, and producing Dict+-- as the result.+-- It would be nice to have some way to stop the proliferation of these variants and unify the existing ones, but+-- at the moment, it appears to require honest type level functions. (Closed type families which must be fully+-- applied didn't quite cut it when I tried). Some symbolic type-level application could do the trick, but I didn't+-- want to go quite that far at the time of writing. class ArgDict f where   type ConstraintsFor f (c :: k -> Constraint) :: Constraint   type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) :: Constraint   argDict :: ConstraintsFor f c => f a -> Dict (c a)   argDict' :: ConstraintsFor' f c g => f a -> Dict (c (g a)) +-- | This places a tighter restriction on the kind of f, and so needs to be a separate class.+class ArgDictV f where+  type ConstraintsForV (f :: (k -> k') -> *) (c :: k' -> Constraint) (g :: k) :: Constraint+  argDictV :: ConstraintsForV f c g => f v -> Dict (c (v g))+ type Has (c :: k -> Constraint) f = (ArgDict f, ConstraintsFor f c) type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict f, ConstraintsFor' f c g)+type HasV c f g = (ArgDictV f, ConstraintsForV f c g)  has :: forall c f a r. (Has c f) => f a -> (c a => r) -> r has k r | (Dict :: Dict (c a)) <- argDict k = r@@ -29,9 +43,13 @@ has' :: forall c g f a r. (Has' c f g) => f a -> (c (g a) => r) -> r has' k r | (Dict :: Dict (c (g a))) <- argDict' k = r +hasV :: forall c g f v r. (HasV c f g) => f v -> (c (v g) => r) -> r+hasV k r | (Dict :: Dict (c (v g))) <- argDictV k = r+ whichever :: forall c t a r. (ForallF c t) => (c (t a) => r) -> r whichever r = r \\ (instF :: ForallF c t :- c (t a))  -- | Allows explicit specification of constraint implication class Implies1 c d where   implies1 :: c a :- d a+

@@ -1,7 +1,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE TemplateHaskell #-}-module Data.Constraint.Extras.TH where+module Data.Constraint.Extras.TH (deriveArgDict, deriveArgDictV, gadtIndices) where  import Data.Constraint.Extras import Control.Monad@@ -11,7 +11,7 @@  deriveArgDict :: Name -> Q [Dec] deriveArgDict n = do-  ts <- gadtResults n+  ts <- gadtIndices n   c <- newName "c"   g <- newName "g"   let xs = map (AppT (VarT c)) ts@@ -19,35 +19,56 @@       l = length xs       constraints = foldl AppT (TupleT l) xs       constraints' = foldl AppT (TupleT l) xs'+  {-   runIO $ putStrLn "Constraints:"   runIO . putStrLn . pprint $ constraints'+  -}   [d| instance ArgDict $(pure $ ConT n) where         type ConstraintsFor  $(conT n) $(varT c) = $(pure constraints)         type ConstraintsFor' $(conT n) $(varT c) $(varT g) = $(pure constraints')-        argDict = $(LamCaseE <$> matches 'argDict)-        argDict' = $(LamCaseE <$> matches 'argDict')+        argDict = $(LamCaseE <$> matches n 'argDict)+        argDict' = $(LamCaseE <$> matches n 'argDict')     |]-  where-    matches :: Name -> Q [Match]-    matches argDictName = do-      x <- newName "x"-      reify n >>= \case-        TyConI (DataD _ _ _ _ cons _) -> pure $ concat $ flip map cons $ \case-          GadtC [name] _ (AppT (ConT _) (VarT _)) ->-            [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]-          GadtC [name] _ _ ->-            [Match (RecP name []) (NormalB $ ConE 'Dict) []]-          ForallC _ _ (GadtC [name] _ (AppT (ConT _) (VarT _))) ->-            [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]-          ForallC _ _ (GadtC [name] _ _) ->-            [Match (RecP name []) (NormalB $ ConE 'Dict) []]-          NormalC name [(_, AppT (ConT _) (VarT _))] ->-            [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]-          a -> error $ "deriveArgDict matches: Unmatched 'Dec': " <> show a-        a -> error $ "deriveArgDict matches: Unmatched 'Info': " <> show a -gadtResults :: Name -> Q [Type]-gadtResults n = do+deriveArgDictV :: Name -> Q [Dec]+deriveArgDictV n = do+  vs <- gadtIndices n+  c <- newName "c"+  g <- newName "g"+  let xs = map (\v -> AppT (VarT c) $ AppT v (VarT g)) vs+      l = length xs+      constraints = foldl AppT (TupleT l) xs+  {-+  runIO $ putStrLn "Constraints:"+  runIO . putStrLn . pprint $ constraints'+  -}+  ds <- deriveArgDict n+  d <- [d| instance ArgDictV $(pure $ ConT n) where+             type ConstraintsForV $(conT n) $(varT c) $(varT g) = $(pure constraints)+             argDictV = $(LamCaseE <$> matches n 'argDictV)+       |]+  return (d ++ ds)++matches :: Name -> Name -> Q [Match]+matches n argDictName = do+  x <- newName "x"+  reify n >>= \case+    TyConI (DataD _ _ _ _ cons _) -> pure $ concat $ flip map cons $ \case+      GadtC [name] _ (AppT (ConT _) (VarT _)) ->+        [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]+      GadtC [name] _ _ ->+        [Match (RecP name []) (NormalB $ ConE 'Dict) []]+      ForallC _ _ (GadtC [name] _ (AppT (ConT _) (VarT _))) ->+        [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]+      ForallC _ _ (GadtC [name] _ _) ->+        [Match (RecP name []) (NormalB $ ConE 'Dict) []]+      NormalC name [(_, AppT (ConT _) (VarT _))] ->+        [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]+      a -> error $ "deriveArgDict matches: Unmatched 'Dec': " <> show a+    a -> error $ "deriveArgDict matches: Unmatched 'Info': " <> show a++gadtIndices :: Name -> Q [Type]+gadtIndices n = do   reify n >>= \case     TyConI (DataD _ _ _ _ cons _) -> fmap concat $ forM cons $ \case       GadtC _ _ (AppT (ConT _) (VarT _)) -> return []