packages feed

universe-some (empty) → 1.2

raw patch · 5 files changed

+451/−0 lines, 5 filesdep +basedep +somedep +template-haskell

Dependencies added: base, some, template-haskell, th-abstraction, transformers, transformers-compat, type-equality, universe-base, universe-some

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2013, Daniel Wagner++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 Daniel Wagner 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.
+ src/Data/Universe/Some.hs view
@@ -0,0 +1,99 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes #-}+module Data.Universe.Some (+  UniverseSome (..),+  FiniteSome (..),+  ) where++import Data.Functor.Sum (Sum (..))+import Data.List (genericLength)+import Data.Some (Some, mapSome, mkSome, foldSome)+import Data.Type.Equality ((:~:) (..))+import Data.Universe.Class (Universe (..), Finite (..))+import Data.Universe.Helpers (Tagged (..), Natural, (+++))++import qualified Data.Some.GADT as G+import qualified Data.Some.Newtype as N+import qualified Data.Some.Church as C++-------------------------------------------------------------------------------+-- Class+-------------------------------------------------------------------------------++-- | Auxiliary class to power @'Universe' ('Some' f)@ instance.+-- (There are no good reasons to use @FlexibleInstances@).+--+-- Laws are induced via @'Universe' ('Some' f)@ instance. For example:+--+-- @+-- 'elem' x 'universe' ==> 'elem' ('Some' f) 'universeSome'+-- @+--+-- As 'Data.GADT.Compare.GEq' cannot be written for phantom 'Functor's, e.g.+-- 'Control.Applicative.Const' or 'Data.Proxy.Proxy', they cannot have+-- 'UniverseSome' instance either.+--+-- /Note:/ The 'Some' type is imported from "Data.Some", i.e. maybe+-- either from "Data.Some.Newtype" (default) or "Data.Some.GADT" modules.+--+class UniverseSome f where+  universeSome :: [Some f]++class UniverseSome f => FiniteSome f where+  universeFSome :: [Some f]+  universeFSome = universeSome++  cardinalitySome :: Tagged (Some f) Natural+  cardinalitySome = Tagged (genericLength (universeFSome :: [Some f]))++-------------------------------------------------------------------------------+-- Instances for Some+-------------------------------------------------------------------------------++instance UniverseSome f => Universe (N.Some f) where+  universe = map (foldSome N.mkSome) universeSome++instance FiniteSome f => Finite (N.Some f) where+  universeF   = map (foldSome N.mkSome) universeFSome+  cardinality = retagSome cardinalitySome++instance UniverseSome f => Universe (G.Some f) where+  universe =  map (foldSome G.mkSome) universeSome++instance FiniteSome f => Finite (G.Some f) where+  universeF   = map (foldSome G.mkSome) universeFSome+  cardinality = retagSome cardinalitySome++instance UniverseSome f => Universe (C.Some f) where+  universe =  map (foldSome C.mkSome) universeSome++instance FiniteSome f => Finite (C.Some f) where+  universeF   = map (foldSome C.mkSome) universeFSome+  cardinality = retagSome cardinalitySome++retagSome :: Tagged (Some f) Natural -> Tagged (some f) Natural+retagSome (Tagged n) = Tagged n++-------------------------------------------------------------------------------+-- Type equality is singleton+-------------------------------------------------------------------------------++instance UniverseSome ((:~:) a) where+  universeSome = [mkSome Refl]++instance FiniteSome ((:~:) a) where+  cardinalitySome = 1++-------------------------------------------------------------------------------+-- Functors+-------------------------------------------------------------------------------++instance (UniverseSome f, UniverseSome g) => UniverseSome (Sum f g) where+  universeSome = map (mapSome InL) universeSome +++ map (mapSome InR) universeSome++instance (FiniteSome f, FiniteSome g) => FiniteSome (Sum f g) where+  universeFSome = map (mapSome InL) universeFSome ++ map (mapSome InR) universeFSome++-- Note: Product instance is tricky, we could for special cases.+-- e.g. '(GEq f, f ~ g) => UnvierseSome (Product f g)', but this is boring+-- instance as we'd 'Pair' equal instances only.
+ src/Data/Universe/Some/TH.hs view
@@ -0,0 +1,172 @@+{-# LANGUAGE CPP #-}+#if __GLASGOW_HASKELL__ >= 800+{-# LANGUAGE TemplateHaskellQuotes #-}+#else+{-# LANGUAGE TemplateHaskell #-}+#endif+module Data.Universe.Some.TH (+  DeriveUniverseSome (..),+  universeSomeQ,+  ) where++import Control.Monad (forM, mapM, unless)+import Data.Some (Some, mkSome)+import Data.Universe.Class (Universe (..))+import Data.Universe.Some (UniverseSome (..))+import Data.Universe.Helpers (interleave, (<+*+>))+import Language.Haskell.TH+import Language.Haskell.TH.Datatype++-- | Derive the @'UniverseSome' n@ instance.+--+-- >>> :set -XGADTs -XTemplateHaskell -XStandaloneDeriving+-- >>> import Data.Universe.Class (universe)+-- >>> import Data.GADT.Show+--+-- >>> data Tag b a where IntTag :: Tag b Int; BoolTag :: b -> Tag b Bool+-- >>> deriving instance Show b => Show (Tag b a)+-- >>> instance Show b => GShow (Tag b) where gshowsPrec = showsPrec+--+-- >>> ; deriveUniverseSome ''Tag+-- >>> universe :: [Some (Tag (Maybe Bool))]+-- [Some IntTag,Some (BoolTag Nothing),Some (BoolTag (Just False)),Some (BoolTag (Just True))]+--+-- 'deriveUniverseSome' variant taking a 'Name' guesses simple class constraints.+-- If you need more specific, you can specify them:+--+-- >>> ; deriveUniverseSome [d| instance Universe b => UniverseSome (Tag b) |]+-- >>> universe :: [Some (Tag (Maybe Bool))]+-- [Some IntTag,Some (BoolTag Nothing),Some (BoolTag (Just False)),Some (BoolTag (Just True))]+--+class DeriveUniverseSome a where+  deriveUniverseSome :: a -> DecsQ++instance DeriveUniverseSome a => DeriveUniverseSome [a] where+  deriveUniverseSome a = fmap concat (mapM deriveUniverseSome a)++instance DeriveUniverseSome a => DeriveUniverseSome (Q a) where+  deriveUniverseSome a = deriveUniverseSome =<< a++instance DeriveUniverseSome Name where+  deriveUniverseSome name = do+    di <- reifyDatatype name+    let DatatypeInfo { datatypeContext = ctxt+                     , datatypeName    = parentName+#if MIN_VERSION_th_abstraction(0,3,0)+                     , datatypeInstTypes = vars0+#else+                     , datatypeVars    = vars0+#endif+                     , datatypeCons    = cons+                     } = di++    case safeUnsnoc vars0 of+      Nothing -> fail "Datatype should have at least one type variable"+      Just (vars, var) -> do+        varNames <- forM vars $ \v -> case v of+#if MIN_VERSION_template_haskell(2,8,0)+          SigT (VarT n) StarT -> newName "x"+#else+          SigT (VarT n) StarK -> newName "x"+#endif+          _                   -> fail "Only arguments of kind Type are supported"++#if MIN_VERSION_template_haskell(2,10,0)+        let constrs :: [TypeQ]+            constrs = map (\n -> conT ''Universe `appT` varT n) varNames+#else+        let constrs :: [PredQ]+            constrs = map (\n -> classP ''Universe [varT n]) varNames+#endif+        let typ     = foldl (\c n -> c `appT` varT n) (conT parentName) varNames++        i <- instanceD (cxt constrs) (conT ''UniverseSome `appT` typ)+            [ instanceDecFor di+            ]++        return [i]++instanceDecFor :: DatatypeInfo -> Q Dec+instanceDecFor di = valD (varP 'universeSome) (normalB $ universeSomeQ' di) []++instance DeriveUniverseSome Dec where+#if MIN_VERSION_template_haskell(2,11,0)+  deriveUniverseSome (InstanceD overlaps c classHead []) = do+    let instanceFor = InstanceD overlaps c classHead+#else+  deriveUniverseSome (InstanceD c classHead []) = do+    let instanceFor = InstanceD c classHead+#endif+    case classHead of+      ConT u `AppT` t | u == ''UniverseSome -> do+        name <- headOfType t+        di <- reifyDatatype name+        i <- fmap instanceFor $ mapM id+            [ instanceDecFor di+            ]+        return [i]+      _ -> fail $ "deriveUniverseSome: expected an instance head like `UniverseSome (C a b ...)`, got " ++ show classHead+  deriveUniverseSome _ = fail "deriveUniverseSome: expected an empty instance declaration"++-- | Derive the method for @:: ['Some' tag]@+--+-- >>> :set -XGADTs -XTemplateHaskell -XStandaloneDeriving+-- >>> import Data.GADT.Show+--+-- >>> data Tag b a where IntTag :: Tag b Int; BoolTag :: b -> Tag b Bool+-- >>> deriving instance Show b => Show (Tag b a)+-- >>> instance Show b => GShow (Tag b) where gshowsPrec = showsPrec+--+-- >>> $(universeSomeQ ''Tag) :: [Some (Tag Bool)]+-- [Some IntTag,Some (BoolTag False),Some (BoolTag True)]+--+universeSomeQ :: Name -> ExpQ+universeSomeQ name = reifyDatatype name >>= universeSomeQ'++universeSomeQ' :: DatatypeInfo -> Q Exp+universeSomeQ' di = do+  let DatatypeInfo { datatypeContext = ctxt+                   , datatypeName    = parentName+#if MIN_VERSION_th_abstraction(0,3,0)+                   , datatypeInstTypes = vars0+#else+                   , datatypeVars    = vars0+#endif+                   , datatypeCons    = cons+                   } = di++  -- check+  unless (null ctxt) $ fail "Datatype context is not empty"++  case safeUnsnoc vars0 of+    Nothing -> fail "Datatype should have at least one type variable"+    Just (vars, var) -> do+      let universe'   = [| universe |]+      let uap         = [| (<+*+>) |]+      let interleave' = [| interleave |]+      let mapSome'    = [| map mkSome |]++      let sums = map (universeForCon mapSome' universe' uap) cons+      interleave' `appE` listE sums+  where+    universeForCon mapSome' universe' uap ci =+      let con     = listE [ conE (constructorName ci) ]+          nargs   = length (constructorFields ci)+          conArgs = foldl (\f x -> infixE (Just f) uap (Just universe')) con (replicate nargs universe')++      in mapSome' `appE` conArgs++-------------------------------------------------------------------------------+-- helpers+-------------------------------------------------------------------------------++headOfType :: Type -> Q Name+headOfType (AppT t _) = headOfType t+headOfType (VarT n)   = return n+headOfType (ConT n)   = return n+headOfType t          = fail $ "headOfType: " ++ show t++safeUnsnoc :: [a] -> Maybe ([a], a)+safeUnsnoc xs = case reverse xs of+  []     -> Nothing+  (y:ys) -> Just (reverse ys, y)
+ test/Test.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+module Main (main) where++import Data.Universe.Class (Universe (..))+import Data.Some (Some (..))+import Data.GADT.Show+import Data.Universe.Some (UniverseSome (..))+import Data.Universe.Some.TH++-------------------------------------------------------------------------------+-- Name+-------------------------------------------------------------------------------++data Tag b a where+  IntTag  :: Tag b Int+  BoolTag :: b -> Tag b Bool++deriving instance Show b => Show (Tag b a)+instance Show b => GShow (Tag b) where gshowsPrec = showsPrec++deriveUniverseSome ''Tag+++-------------------------------------------------------------------------------+-- Dec+-------------------------------------------------------------------------------++data Tag2 b a where+  IntTag2  :: Tag2 b Int+  BoolTag2 :: b -> Tag2 b Bool++deriving instance Show b => Show (Tag2 b a)+instance Show b => GShow (Tag2 b) where gshowsPrec = showsPrec++deriveUniverseSome [d| instance Universe b => UniverseSome (Tag2 b) |]++-------------------------------------------------------------------------------+-- Manual+-------------------------------------------------------------------------------++data Tag3 b a where+  IntTag3  :: Tag3 b Int+  BoolTag3 :: b -> Tag3 b Bool++deriving instance Show b => Show (Tag3 b a)+instance Show b => GShow (Tag3 b) where gshowsPrec = showsPrec++-- to separate splices+$(return [])++instance Universe b => UniverseSome (Tag3 b) where+    universeSome = $(universeSomeQ ''Tag3)++-------------------------------------------------------------------------------+-- Main+-------------------------------------------------------------------------------++main :: IO ()+main = do+  print (universe :: [Some (Tag (Maybe Bool)) ])+  print (universe :: [Some (Tag2 (Maybe Bool)) ])+  print (universe :: [Some (Tag3 (Maybe Bool)) ])
+ universe-some.cabal view
@@ -0,0 +1,86 @@+name:          universe-some+version:       1.2+synopsis:      Universe instances for Some from some+description:+  A class for finite and recursively enumerable types and some helper functions for enumerating them+  defined in @universe-base@ package:+  .+  @+  class Universe a where universe :: [a]+  class Universe a => Finite a where universeF :: [a]; universeF = universe+  @+  .+  This package adds+  .+  @+  class UniverseSome f where universeSome :: [Some f]+  class UniverseSome f => FiniteSome f where universeFSome :: [Some f]; universeFSome = universe+  @+  .+  classes.++homepage:      https://github.com/dmwit/universe+license:       BSD3+license-file:  LICENSE+author:        Daniel Wagner, Oleg Grenrus+maintainer:    me@dmwit.com+copyright:     Daniel Wagner 2014, Oleg Grenrus 2019+category:      Data+build-type:    Simple+cabal-version: >=1.10+tested-with:+  GHC ==7.0.4+   || ==7.4.2+   || ==7.6.3+   || ==7.8.4+   || ==7.10.3+   || ==8.0.2+   || ==8.2.2+   || ==8.4.4+   || ==8.6.5+   || ==8.8.1++source-repository head+  type:     git+  location: https://github.com/dmwit/universe++source-repository this+  type:     git+  location: https://github.com/dmwit/universe+  tag:      instances-dependent-sum-1.1++library+  default-language: Haskell2010+  hs-source-dirs:   src+  exposed-modules:+    Data.Universe.Some+    Data.Universe.Some.TH++  build-depends:+      base              >=4.3      && <4.14+    , some              >=1        && <1.1+    , template-haskell  >=2.5      && <2.16+    , th-abstraction    >=0.2.11.0 && <0.4+    , transformers      >=0.3.0.0  && <0.6+    , universe-base     >=1.1      && <1.1.2++  if !impl(ghc >=7.8)+    build-depends: type-equality >=1 && <1.1++  if impl(ghc >=7.10.3)+    build-depends: transformers >=0.4.2.0++  if !impl(ghc >=7.10.3)+    build-depends: transformers-compat >=0.6.1 && <0.7++test-suite th-test+  type:             exitcode-stdio-1.0+  default-language: Haskell2010+  hs-source-dirs:   test+  main-is:          Test.hs+  build-depends:+      base+    , some+    , template-haskell+    , universe-base+    , universe-some