summer 0.2.0.1 → 0.3.0.0

raw patch · 6 files changed

+235/−49 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +3/−0
• src/Data/ForAll.hs +13/−0
• src/Data/Prodder.hs +113/−12
• src/Data/Summer.hs +20/−0
• summer.cabal +2/−1
• test/Test.hs +84/−36

@@ -24,6 +24,9 @@  a' :: Bool a' = consume y' (\b f -> b && f == 0.2)++q :: Bool+q = select x' $ \b (f :: Float)-> b && f == 0.2 ```  This package is extremely experimental, and is subject to arbitrarily large changes.

@@ -0,0 +1,13 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ExplicitNamespaces #-}+module Data.ForAll (type ForAll) where++import GHC.Exts (Constraint)++type family ForAll c xs :: Constraint where+  ForAll c '[] = ()+  ForAll c (x ': xs) = (c x, ForAll c xs)+

@@ -1,3 +1,6 @@+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE BlockArguments #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE AllowAmbiguousTypes #-}@@ -31,8 +34,18 @@   , tailN   , initN   , dropFirst-  , Consume(consume, produce, extend1, cmap)+  , Consume(consume, extend1, cmap, produceB)+  , produce+  , empty+  , ToList(toList)+  , type ForAll+    -- ** Efficient Iterative Construction+  , buildProd+  , ProdBuilder+  , consB+  , emptyB     -- * Type families+  , Index   , IndexIn   , HasIndexIn   , Consumer@@ -45,20 +58,50 @@   , Strengthen(strengthen)     -- * Transforming extensible products   , remap+    -- * Picking out individual components of a product+  , Selection(select)+  , type FieldsFromSelector+  , type Selector+    -- * Efficiently building 'Prod's   ) where +import Data.ForAll (type ForAll) import Control.Monad (unless) import Control.Exception (catch, SomeException)-import GHC.Exts (Any)+import GHC.Exts (Any, Constraint) import Unsafe.Coerce (unsafeCoerce)+import Data.Functor.Identity (Identity (..)) import Data.Vector (Vector) import qualified Data.Vector as V-import GHC.TypeLits (KnownNat, type (+), type (-), natVal, type (<=))+import qualified Data.Vector.Mutable as MV+import GHC.TypeLits (KnownNat, type (+), type (-), natVal, type (<=), Nat) import Data.Proxy (Proxy(Proxy))+import Control.Monad.ST+import Data.STRef (newSTRef, STRef, writeSTRef, readSTRef)  -- | An extensible product type-data Prod (xs :: [*]) = UnsafeProd { unProd :: Vector Any }+newtype Prod (xs :: [*]) = UnsafeProd { unProd :: Vector Any } +-- | A type for constructing products with linear memory use.+newtype ProdBuilder (xs :: [*]) = UnsafeProdBuilder { unProdBuilder :: forall s. STRef s Int -> V.MVector s Any -> ST s () }++-- | Cons an element onto the head of a 'ProdBuilder'.+consB :: x -> ProdBuilder xs -> ProdBuilder (x ': xs)+consB x (UnsafeProdBuilder b) = UnsafeProdBuilder \ref v -> withIncrement ref \i -> do+  MV.write v i (unsafeCoerce x)++-- | Empty 'ProdBuilder'.+emptyB :: ProdBuilder '[]+emptyB = UnsafeProdBuilder \_ _ -> pure ()++-- | Execute a 'ProdBuilder', pulling out a 'Prod'.+buildProd :: forall xs. (KnownNat (Length xs)) => ProdBuilder xs -> Prod xs+buildProd (UnsafeProdBuilder bs) = UnsafeProd $ V.create do+  ref <- newSTRef 0+  x <- MV.new (fromInteger $ natVal (Proxy @(Length xs)))+  bs ref x+  pure x+ type role Prod representational  -- | A type family for computing the index of a type in a list of types.@@ -66,6 +109,11 @@   IndexIn x (x ': xs) = 0   IndexIn x (y ': xs) = 1 + IndexIn x xs +-- | A type family for indexing into lists of types.+type family Index (n :: Nat) (xs :: [k]) where+  Index 0 (x ': xs) = x+  Index n (_ ': xs) = Index (n - 1) xs+ -- | A type family for computing the length of a type level list type family Length (xs :: [k]) where   Length '[] = 0@@ -147,28 +195,46 @@ -- extensible products. class Consume xs where   consume :: forall r. Prod xs -> Consumer xs r -> r-  produce :: (forall r. Consumer xs r -> r) -> Prod xs-  extend1 :: x -> Consumer xs (Prod (x ': xs))+  produceB :: (forall r. Consumer xs r -> r) -> ProdBuilder xs+  extend1 :: x -> Consumer xs (ProdBuilder (x ': xs))   cmap :: (r -> r') -> Consumer xs r -> Consumer xs r'  +produce :: (KnownNat (Length xs), Consume xs) => (forall r. Consumer xs r -> r) -> Prod xs+produce f = buildProd $ produceB f++empty :: Prod '[]+empty = buildProd $ produceB id+ instance Consume '[] where   consume = flip const   {-# INLINE CONLIKE consume #-}-  produce x = UnsafeProd V.empty-  {-# INLINE CONLIKE produce #-}-  extend1 x = UnsafeProd (V.singleton (unsafeCoerce x))+  produceB x = UnsafeProdBuilder \ref v -> pure ()+  {-# INLINE CONLIKE produceB #-}+  extend1 x = UnsafeProdBuilder \ref v -> withIncrement ref \i -> MV.write v i (unsafeCoerce x)   {-# INLINE CONLIKE extend1 #-}   cmap f x = f x   {-# INLINE CONLIKE cmap #-} +withIncrement :: STRef s Int -> (Int -> ST s x) -> ST s x+withIncrement ref f = do+  i <- readSTRef ref+  x <- f i+  writeSTRef ref (i + 1)+  pure x+ instance Consume xs => Consume (x ': xs) where   consume (UnsafeProd v) g = consume @xs (UnsafeProd (V.tail v)) $ g (unsafeCoerce $ v V.! 0)   {-# INLINE CONLIKE consume #-}-  produce g = g (extend1 @xs)-  {-# INLINE CONLIKE produce #-}+  produceB g = g (extend1 @xs)+  {-# INLINE CONLIKE produceB #-}   cmap f = fmap (cmap @xs f)   {-# INLINE CONLIKE cmap #-}-  extend1 (x1 :: x1) x = cmap @xs @(Prod (x ': xs)) @(Prod (x1 ': x ': xs)) (UnsafeProd . (V.singleton (unsafeCoerce x1) V.++) . unProd) (extend1 @xs x)+  extend1 (x1 :: x1) x = cmap @xs @(ProdBuilder (x ': xs)) @(ProdBuilder (x1 ': x ': xs)) f (extend1 @xs x) where+    f (UnsafeProdBuilder b) = UnsafeProdBuilder \ref v -> (withIncrement ref \i -> MV.write v i (unsafeCoerce x1)) >> b ref v+    +      +     +  -- cmap @xs @(Prod (x ': xs)) @(Prod (x1 ': x ': xs)) (UnsafeProd . (V.singleton (unsafeCoerce x1) V.++) . unProd) (extend1 @xs x)   {-# INLINE CONLIKE extend1 #-}  instance Eq (Prod '[]) where@@ -188,3 +254,38 @@ instance Strengthen xs '[] where   strengthen = const (UnsafeProd V.empty)   {-# INLINE CONLIKE strengthen #-}++-- | A typeclass for creating a selection function which is valid on the given definition.+type family Selector def fields a where+  Selector def (field ': fields) a = Index field def -> Selector def fields a+  Selector def '[] a = a++-- | Extracts the fields intended from the given selector type.+type family FieldsFromSelector def selector where+  FieldsFromSelector def (a -> b) = IndexIn a def ': FieldsFromSelector def b+  FieldsFromSelector def (Identity a) = '[]++-- | A class for constructing the select function inductively.+class Selection def selector a where+  select :: Prod def -> selector -> a++instance Selection def a a where+  select _prod s = s+  {-# INLINE CONLIKE select #-}++instance (HasIndexIn x def, Selection def xs a) => Selection def (x -> xs) a where+  select prod f = select @_ @_ @a prod (f (extract @x prod))+  {-# INLINE CONLIKE select #-}++-- | A class for turning a 'Prod' into a regular list using a+-- function which takes an argument only constrained by a 'Constraint'+-- each element of the product has.+class ForAll c xs => ToList c xs where+  toList :: (forall a. c a => a -> b) -> Prod xs -> [b]++instance ToList c '[] where+  toList _f _p = []++instance (c x, ToList c xs) => ToList c (x ': xs) where+  toList f p = f x : toList @c f (dropFirst p) where+    x = extract @x p

@@ -1,3 +1,5 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE UndecidableSuperClasses #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE UndecidableInstances #-}@@ -33,6 +35,7 @@   , inject   , inspect   , consider+  , considerFirst   , Match(match, override, unmatch)   , Unmatch   -- * Type families@@ -47,6 +50,9 @@   -- * Transforming extensible sums   , inmap   , smap+  -- * Applying Polymorphic Functions+  , ApplyFunction(apply)+  , type ForAll   ) where  import Control.Exception (catch, SomeException)@@ -58,6 +64,7 @@ import Control.Monad (unless) import Generics.SOP (Generic(..)) import qualified Generics.SOP as SOP+import Data.ForAll (type ForAll)  -- | The extensible sum type, allowing inhabitants to be of any of the -- types in the given type list.@@ -234,3 +241,16 @@ instance (Unmatch xs ys, x `HasTagIn` ys) => Unmatch (x ': xs) ys where   unmatchGo f = unmatchGo @xs (f (UnsafeInj (tag @x @ys) . unsafeCoerce @x))   {-# INLINE CONLIKE unmatchGo #-}++-- | Using functions which only require constraints which are satisfied by+-- all members of the sum.+class ForAll c xs => ApplyFunction c xs where+  apply :: (forall a. c a => a -> y) -> Sum xs -> y++instance ApplyFunction c '[] where+  apply _f x = error "Impossible: empty sum"++instance (c x, ApplyFunction c xs) => ApplyFunction c (x ': xs) where+  apply f x = case considerFirst x of+    Right x' -> f x'+    Left xs -> apply @c f xs

@@ -1,6 +1,6 @@ cabal-version:       2.4 name:                summer-version:             0.2.0.1+version:             0.3.0.0 synopsis:            An implementation of extensible products and sums description:         An implementation of extensible products and sums. license:             MIT@@ -20,6 +20,7 @@  library   exposed-modules:     Data.Summer, Data.Prodder+  other-modules:       Data.ForAll   build-depends:       base >=4.12 && <4.16, vector >=0.12, generics-sop >=0.5   hs-source-dirs:      src   default-language:    Haskell2010

@@ -1,3 +1,4 @@+{-# LANGUAGE BlockArguments #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -11,6 +12,12 @@ main :: IO () main = sumTest >> prodTest +require :: Bool -> String -> IO ()+require p s = unless p $ fail s++requires :: [(Bool, String)] -> IO ()+requires = mapM_ (uncurry require)+ prodTest :: IO () prodTest = catchAndDisplay   [ indexTest@@ -27,43 +34,71 @@     indexTest = do       let index' = index @Int @'[Bool, Int]           index'' = index @Bool @'[Bool, Int]-      unless (index' == 1) $ fail ("Index " <> show index' <> " does not equal 1")-      unless (index'' == 0) $ fail ("Index " <> show index'' <> " does not equal 0")+      requires+        [ (index' == 1, "Index " <> show index' <> " does not equal 1")+        , (index'' == 0, "Index " <> show index'' <> " does not equal 0")+        ]     remapTest = do       let x :: Prod '[Int, Bool] = produce (\f -> f 10 True)       let y = remap ((+ 10000000000000000000000000000) . toInteger @Int) x       let z = remap not x-      unless (y == produce (\f -> f 10000000000000000000000000010 True)) $ fail "Remapping does not work 1"-      unless (z == produce (\f -> f 10 False)) $ fail "Remapping does not work 2"+      requires+        [ (y == produce (\f -> f 10000000000000000000000000010 True), "Remapping does not work 1")+        , (z == produce (\f -> f 10 False), "Remapping does not work 2")+        ]     consumeAndProduceTest = do       let x :: Prod '[Int, Bool] = produce (\f -> f 10 True)           y :: Bool = consume x (\n b -> n == 10 && b)-      unless y $ fail "Consuming and producing does not work"+      require y "Consuming and producing does not work"     extractTest = do       let x :: Prod '[Int, Bool] = produce (\f -> f 10 True)           y :: Bool = extract x           z :: Int = extract x-      unless (z == 10 && y) $ fail "Extracting does not work"+      require (z == 10 && y) "Extracting does not work"     strengthenTest = do       let x :: Prod '[Int, Bool, Float] = produce (\f -> f 10 True 0.1)           y :: Prod '[Bool, Int, Float] = strengthen x           z :: Prod '[Bool, Int] = strengthen x-      unless (y == produce (\f -> f True 10 0.1)) $ fail "strengthen doesn't work 1"-      unless (z == produce (\f -> f True 10)) $ fail "strengthen doesn't work 2"+      requires+        [ (y == produce (\f -> f True 10 0.1), "strengthen doesn't work 1")+        , (z == produce (\f -> f True 10), "strengthen doesn't work 2")+        ]     initNTest = do       let x :: Prod '[Int, Bool, Char, Float] = produce (\f -> f 10 True 'a' 0.2)-      unless (initN @0 x == produce id) $ fail "tailN does not work 0"-      unless (initN @1 x == produce (\f -> f 10)) $ fail "tailN does not work 1"-      unless (initN @2 x == produce (\f -> f 10 True)) $ fail "tailN does not work 2"-      unless (initN @3 x == produce (\f -> f 10 True 'a')) $ fail "tailN does not work 3"-      unless (initN @4 x == produce (\f -> f 10 True 'a' 0.2)) $ fail "tailN does not work 4"+      requires+        [ (initN @0 x == produce id, "tailN does not work 0")+        , (initN @1 x == produce (\f -> f 10), "tailN does not work 1")+        , (initN @2 x == produce (\f -> f 10 True), "tailN does not work 2")+        , (initN @3 x == produce (\f -> f 10 True 'a'), "tailN does not work 3")+        , (initN @4 x == produce (\f -> f 10 True 'a' 0.2), "tailN does not work 4")+        ]     tailNTest = do       let x :: Prod '[Int, Bool, Char, Float] = produce (\f -> f 10 True 'a' 0.2)-      unless (tailN @0 x == x) $ fail "tailN does not work 0"-      unless (tailN @1 x == produce (\f -> f True 'a' 0.2)) $ fail "tailN does not work 1"-      unless (tailN @2 x == produce (\f -> f 'a' 0.2)) $ fail "tailN does not work 2"-      unless (tailN @3 x == produce (\f -> f 0.2)) $ fail "tailN does not work 3"-      unless (tailN @4 x == produce id) $ fail "tailN does not work 3"+      requires+        [ (tailN @0 x == x, "tailN does not work 0")+        , (tailN @1 x == produce (\f -> f True 'a' 0.2), "tailN does not work 1")+        , (tailN @2 x == produce (\f -> f 'a' 0.2), "tailN does not work 2")+        , (tailN @3 x == produce (\f -> f 0.2), "tailN does not work 3")+        , (tailN @4 x == produce id, "tailN does not work 3")+        ]+    selectTest = do+      let x :: Prod '[Int, Bool, Char, Float] = produce (\f -> f 10 True 'a' 0.2)+      requires+        [ (select x (\(n :: Int) -> n == 10), "select does not work 0")+        , (select x (\(f :: Float) -> f == 0.2), "select does not work 1")+        , (select x (\(b :: Bool) (f :: Float) -> b && f == 0.2), "select does not work 2")+        ]+    prodBuilderTest = do+      requires+        [ (empty == buildProd emptyB, "prodBuilder does not work 0")+        , (produce (\f -> f "Hello") == buildProd (consB "Hello" emptyB), "prodBuilder does not work 1")+        ]+    toListTest = do+      let x :: Prod '[String, Bool] = produce \f -> f "Hello" True+      requires+        [ (toList @Show show x == [show "Hello", show True], "toList does not work 0")+        , (toList @Eq (\a -> a == a) x == [True, True], "toList does not work 1")+        ]  sumTest :: IO () sumTest = catchAndDisplay@@ -83,7 +118,7 @@     tagTest = do       let tag' = tag @Int @'[Bool, Int]           tag'' = tag @Bool @'[Bool, Int]-      unless (tag' == 1) $ fail ("Tag " <> show tag' <> " does not equal 1")+      require (tag' == 1) ("Tag " <> show tag' <> " does not equal 1")     eqTest = do       let x :: Sum '[Int, Bool] = Inj (10 :: Int)           y :: Sum '[Int, Bool] = Inj True@@ -92,44 +127,57 @@           a :: Sum '[Int, Bool] = Inj (10 :: Int)           b :: Sum '[Int, Bool] = Inj False           c :: Sum '[Int, Bool] = Inj True-      unless (x /= y) $ fail "10 equals True"-      unless (x /= z) $ fail "10 equals 11"-      unless (x == a) $ fail "10 does not equal 10"-      unless (y /= b) $ fail "True equals False"-      unless (y == c) $ fail "True does not equal True"+      requires+        [ (x /= y, "10 equals True")+        , (x /= z, "10 equals 11")+        , (x == a, "10 does not equal 10")+        , (y /= b, "True equals False")+        , (y == c, "True does not equal True")+        ]     noOpWeakenTest = do       let x :: Sum '[Int, Bool]  = Inj (10 :: Int)           y :: Sum '[Int, Bool, Integer] = noOpWeaken x-      unless (y == Inj (10 :: Int)) $ fail "y does not equal Inj 10"+      require (y == Inj (10 :: Int)) "y does not equal Inj 10"       pure ()     weakenTest = do       let x :: Sum '[Int, Bool] = Inj (10 :: Int)           y :: Sum '[Bool, Int] = weaken x           z :: Sum '[Integer, Bool, Float, Int] = weaken y-      unless (y == Inj (10 :: Int)) $ fail "y does not equal Inj 10"-      unless (z == Inj (10 :: Int)) $ fail "y does not equal Inj 10"+      requires+        [ (y == Inj (10 :: Int), "y does not equal Inj 10")+        , (z == Inj (10 :: Int), "y does not equal Inj 10")+        ]     matchTest = do       let x :: Sum '[Int, Bool] = Inj (10 :: Int)-      unless (match x (== 10) id) $ fail "x does not match 10"+      require (match x (== 10) id) "x does not match 10"     considerTest = do       let x :: Sum '[Int, Bool] = Inj (10 :: Int)           y :: Sum '[Int, Bool] = Inj True-      unless (consider @Int x == Right 10) $ fail "x at Int is not considered to be 10"-      unless (consider @Int y == Left (Inj True)) $ fail $ "x is not considered to be Left (Inj True)"-      unless (consider @Bool y == Right True) $ fail "x at Bool is not considered to be Right True"+      requires+        [ (consider @Int x == Right 10, "x at Int is not considered to be 10"),+          (consider @Int y == Left (Inj True), "x is not considered to be Left (Inj True)"),+          (consider @Bool y == Right True, "x at Bool is not considered to be Right True")+        ]     inmapTest = do       let x :: Sum '[Int, Bool] = Inj (10 :: Int)           y :: Sum '[Int, Bool] = inmap (== (10 :: Int)) x           z :: Sum '[Int, Bool] = inmap (== True) x-      unless (y == Inj True) $ fail "x did not get mapped to True"-      unless (z == Inj (10 :: Int)) $ fail "x did not get left alone"+      requires+        [ (y == Inj True, "x did not get mapped to True")+        , (z == Inj (10 :: Int), "x did not get left alone")+        ]     smapTest = do       let x :: Sum '[Int, Bool] = Inj (10 :: Int)           y :: Sum '[Bool, Int] = smap (== (10 :: Int)) x           z :: Sum '[Bool, Int] = smap (== True) x-      unless (y == Inj True) $ fail "x did not get mapped to True"-      unless (z == Inj (10 :: Int)) $ fail "x did not get left alone"+      requires+        [ (y == Inj True, "x did not get mapped to True")+        , (z == Inj (10 :: Int), "x did not get left alone")+        ]     unmatchTest = do       let x :: Sum '[Int, Bool] = Inj True           y = \f g -> f 100-      unless (x == unmatch (match x)) $ fail "match and unmatch are not an inverse pair"+      require (x == unmatch (match x)) "match and unmatch are not an inverse pair"+    applyTest = do+      let x :: Sum '[Int, Bool] = Inj False+      require (apply @Show show x == "False") "apply does not work 0"