quantification 0.5.2 → 0.6.0
raw patch · 3 files changed
+6/−429 lines, 3 filesdep −ghc-primdep ~aesondep ~binary
Dependencies removed: ghc-prim
Dependency ranges changed: aeson, binary
Files
- quantification.cabal +6/−9
- src/Topaz/Rec.hs +0/−144
- src/Topaz/Types.hs +0/−276
quantification.cabal view
@@ -1,10 +1,10 @@-cabal-version: 2.0+cabal-version: 2.4 name: quantification-version: 0.5.2+version: 0.6.0 synopsis: Rage against the quantification description: Data types and typeclasses to deal with universally and existentially quantified types homepage: https://github.com/andrewthad/quantification#readme-license: BSD3+license: BSD-3-Clause license-file: LICENSE author: Andrew Martin maintainer: andrew.thaddeus@gmail.com@@ -18,14 +18,11 @@ Data.Binary.Lifted Data.Exists Data.Monoid.Lifted- Topaz.Rec- Topaz.Types build-depends:- base >= 4.11.1 && < 5- , binary >= 0.8 && < 0.10- , ghc-prim >= 0.5 && < 0.7+ , base >= 4.11.1 && < 5+ , binary >= 0.8 && < 0.11 , hashable >= 1.2 && < 1.4- , aeson >= 1.0 && < 1.5+ , aeson >= 1.0 && < 1.6 , text >= 1.0 && < 2.0 , path-pieces >= 0.2 && < 0.3 , vector >= 0.11 && < 0.13
− src/Topaz/Rec.hs
@@ -1,144 +0,0 @@-{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeFamilyDependencies #-}-{-# LANGUAGE TypeOperators #-}--{-# OPTIONS_GHC -Wall #-}--module Topaz.Rec- ( Rec(..)- , (<:)- , map- , append- , traverse- , traverse_- , zipWith- , foldMap- , foldMap1- , foldl'- -- * Access- , get- , put- , gets- , puts- -- * Conversion- , fromSingList- , toSingList- , fromList- ) where--import Prelude hiding (map,zipWith,foldMap,traverse)-import Topaz.Types (Elem(..),type (++),Rec(..))-import Data.Exists-import qualified Data.Semigroup as SG---- | infix RecCons with proper fixity-infixr 7 <:-(<:) :: forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs)-(<:) = RecCons--map :: (forall x. f x -> g x) -> Rec f as -> Rec g as-map _ RecNil = RecNil-map f (RecCons x xs) = RecCons (f x) (map f xs)--zipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs-zipWith _ RecNil RecNil = RecNil-zipWith f (RecCons a as) (RecCons b bs) =- RecCons (f a b) (zipWith f as bs)---- | Strict left fold over the elements of a record.-foldl' :: forall f a rs.- (forall x. a -> f x -> a) -- ^ Reduction- -> a -- ^ Initial accumulator- -> Rec f rs -- ^ Record- -> a-foldl' g !a0 = go a0 where- go :: forall ss. a -> Rec f ss -> a- go !a RecNil = a- go !a (RecCons r rs) = go (g a r) rs---- | Map each element of a record to a monoid and combine the results.-foldMap :: forall f m rs. Monoid m- => (forall x. f x -> m)- -> Rec f rs- -> m-foldMap f = go mempty- where- go :: forall ss. m -> Rec f ss -> m- go !m record = case record of- RecNil -> m- RecCons r rs -> go (mappend m (f r)) rs- {-# INLINABLE go #-}-{-# INLINE foldMap #-}--foldMap1 :: forall f m r rs. Semigroup m- => (forall x. f x -> m)- -> Rec f (r ': rs)- -> m-foldMap1 f (RecCons b bs) = go (f b) bs- where- go :: forall ss. m -> Rec f ss -> m- go !m record = case record of- RecNil -> m- RecCons r rs -> go (m SG.<> (f r)) rs- {-# INLINABLE go #-}-{-# INLINE foldMap1 #-}--traverse- :: Applicative h- => (forall x. f x -> h (g x))- -> Rec f rs- -> h (Rec g rs)-traverse _ RecNil = pure RecNil-traverse f (RecCons x xs) = RecCons <$> f x <*> traverse f xs-{-# INLINABLE traverse #-}--traverse_- :: Applicative h- => (forall x. f x -> h b)- -> Rec f rs- -> h ()-traverse_ _ RecNil = pure ()-traverse_ f (RecCons x xs) = f x *> traverse_ f xs-{-# INLINABLE traverse_ #-}--get :: Elem rs r -> Rec f rs -> f r-get ElemHere (RecCons r _) = r-get (ElemThere ix) (RecCons _ rs) = get ix rs--put :: Elem rs r -> f r -> Rec f rs -> Rec f rs-put ElemHere r' (RecCons _ rs) = RecCons r' rs-put (ElemThere ix) r' (RecCons r rs) = RecCons r (put ix r' rs)--gets :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss-gets ixs rec = map (\e -> get e rec) ixs--puts :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss -> Rec f rs-puts RecNil rs _ = rs-puts (RecCons ix ixs) rs (RecCons s ss) = put ix s (puts ixs rs ss)--append :: Rec f as -> Rec f bs -> Rec f (as ++ bs)-append RecNil ys = ys-append (RecCons x xs) ys = RecCons x (append xs ys)--fromSingList :: SingList as -> Rec Sing as-fromSingList SingListNil = RecNil-fromSingList (SingListCons r rs) = RecCons r (fromSingList rs)--toSingList :: Rec Sing as -> SingList as-toSingList RecNil = SingListNil-toSingList (RecCons r rs) = SingListCons r (toSingList rs)--fromList :: [Exists f] -> Exists (Rec f)-fromList [] = Exists RecNil-fromList (Exists x : xs) = case fromList xs of- Exists ys -> Exists (RecCons x ys)
− src/Topaz/Types.hs
@@ -1,276 +0,0 @@-{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}--{-# OPTIONS_GHC -Wall -Werror #-}--module Topaz.Types- ( Elem(..)- , Rec(..)- -- , BiRec(..)- , NestRec(..)- , Fix(..)- , HFix(..)- , Nest(..)- , EqHetero(..)- , TestEqualityHetero(..)- , Nat(..)- , SingNat(..)- , Vector(..)- , type (++)- ) where--import Control.Applicative (liftA2)-import Data.Exists-import Data.Foldable (foldrM)-import Data.Hashable (Hashable(..))-import Data.Kind (Type)-import Data.Monoid.Lifted (Semigroup1(..), Monoid1(..), append1)-import Data.Proxy (Proxy(..))-import Data.Type.Coercion-import Data.Type.Equality-import Foreign.Ptr (castPtr,plusPtr)-import Foreign.Storable (Storable(..))--import qualified Data.Aeson as AE-import qualified Data.Aeson.Types as AET-import qualified Data.Semigroup as SG-import qualified Data.Vector as V--data Nat = Succ Nat | Zero--data SingNat :: Nat -> Type where- SingZero :: SingNat 'Zero- SingSucc :: SingNat n -> SingNat ('Succ n)--type instance Sing = SingNat--data Vector :: Nat -> Type -> Type where- VectorNil :: Vector 'Zero a- VectorCons :: a -> Vector n a -> Vector ('Succ n) a--instance Eq a => Eq (Vector n a) where- VectorNil == VectorNil = True- VectorCons a as == VectorCons b bs = a == b && as == bs--data Elem (rs :: [k]) (r :: k) where- ElemHere :: Elem (r ': rs) r- ElemThere :: Elem rs r -> Elem (s ': rs) r--type family (as :: [k]) ++ (bs :: [k]) :: [k] where- '[] ++ bs = bs- (a ': as) ++ bs = a ': (as ++ bs)-infixr 5 ++--data Rec :: (k -> Type) -> [k] -> Type where- RecNil :: Rec f '[]- RecCons :: f r -> Rec f rs -> Rec f (r ': rs)---- data BiRec :: (k -> Type) -> (j -> Type) -> [k] -> [j] -> Type where--- BiRec :: Rec f ks -> Rec g js -> BiRec f g ks js--data NestRec :: (k -> Type) -> Nest k -> Type where- NestRec :: Rec f rs -> Rec (NestRec f) ns -> NestRec f ('Nest ns rs)--data Nest a = Nest [Nest a] [a]-newtype Fix f = Fix (f (Fix f))-newtype HFix h a = HFix (h (HFix h) a)--instance Semigroup1 f => Semigroup (Fix f) where- Fix a <> Fix b = Fix (append1 a b)--instance Monoid1 f => Monoid (Fix f) where- mempty = Fix (liftEmpty mempty)- mappend = (SG.<>)---- Think of a better name for this typeclass-class EqHetero h where- eqHetero :: (forall x. f x -> f x -> Bool) -> h f a -> h f a -> Bool--instance EqHetero h => EqForall (HFix h) where- eqForall (HFix a) (HFix b) = eqHetero eqForall a b --instance EqHetero h => Eq (HFix h a) where- (==) = eqForall--class TestEqualityHetero h where- testEqualityHetero :: (forall x y. f x -> f y -> Maybe (x :~: y)) -> h f a -> h f b -> Maybe (a :~: b)--instance TestEqualityHetero h => TestEquality (HFix h) where- testEquality (HFix a) (HFix b) = testEqualityHetero testEquality a b--instance TestEquality f => TestEquality (Rec f) where- testEquality RecNil RecNil = Just Refl- testEquality (RecCons x xs) (RecCons y ys) = do- Refl <- testEquality x y- Refl <- testEquality xs ys- Just Refl- testEquality _ _ = Nothing--instance TestCoercion f => TestCoercion (Rec f) where- testCoercion RecNil RecNil = Just Coercion- testCoercion (RecCons x xs) (RecCons y ys) = do- Coercion <- testCoercion x y- Coercion <- testCoercion xs ys- Just Coercion- testCoercion _ _ = Nothing--instance HashableForall f => HashableForall (Rec f) where- hashWithSaltForall s0 = go s0 where- go :: Int -> Rec f rs -> Int- go !s x = case x of- RecNil -> s- RecCons b bs -> go (hashWithSaltForall s b) bs--instance HashableForall f => Hashable (Rec f as) where- hashWithSalt = hashWithSaltForall--instance ShowForall f => ShowForall (Rec f) where- showsPrecForall p x = case x of- RecCons v vs -> showParen (p > 10)- $ showString "RecCons "- . showsPrecForall 11 v- . showString " "- . showsPrecForall 11 vs- RecNil -> showString "RecNil"--instance ShowForall f => Show (Rec f as) where- showsPrec = showsPrecForall--instance ShowForeach f => ShowForeach (Rec f) where- showsPrecForeach SingListNil _ RecNil = showString "RecNil"- showsPrecForeach (SingListCons s ss) p (RecCons v vs) = showParen (p > 10)- $ showString "RecCons "- . showsPrecForeach s 11 v- . showString " "- . showsPrecForeach ss 11 vs--instance EqForall f => Eq (Rec f as) where- (==) = eqForall--instance EqForall f => EqForall (Rec f) where- eqForall RecNil RecNil = True- eqForall (RecCons a as) (RecCons b bs) =- eqForall a b && eqForall as bs--instance EqForeach f => EqForeach (Rec f) where- eqForeach SingListNil RecNil RecNil = True- eqForeach (SingListCons s ss) (RecCons a as) (RecCons b bs) =- eqForeach s a b && eqForeach ss as bs--instance EqForallPoly f => EqForallPoly (Rec f) where- eqForallPoly RecNil RecNil = WitnessedEqualityEqual- eqForallPoly RecNil (RecCons _ _) = WitnessedEqualityUnequal- eqForallPoly (RecCons _ _) RecNil = WitnessedEqualityUnequal- eqForallPoly (RecCons x xs) (RecCons y ys) = case eqForallPoly x y of- WitnessedEqualityUnequal -> WitnessedEqualityUnequal- WitnessedEqualityEqual -> case eqForallPoly xs ys of- WitnessedEqualityUnequal -> WitnessedEqualityUnequal- WitnessedEqualityEqual -> WitnessedEqualityEqual--instance OrdForall f => Ord (Rec f as) where- compare = compareForall--instance OrdForall f => OrdForall (Rec f) where- compareForall RecNil RecNil = EQ- compareForall (RecCons a as) (RecCons b bs) =- mappend (compareForall a b) (compareForall as bs)--instance OrdForeach f => OrdForeach (Rec f) where- compareForeach SingListNil RecNil RecNil = EQ- compareForeach (SingListCons s ss) (RecCons a as) (RecCons b bs) =- mappend (compareForeach s a b) (compareForeach ss as bs)---instance SemigroupForall f => Semigroup (Rec f as) where- (<>) = recZipWith appendForall--instance SemigroupForeach f => SemigroupForeach (Rec f) where- appendForeach SingListNil RecNil RecNil = RecNil- appendForeach (SingListCons s ss) (RecCons x xs) (RecCons y ys) =- RecCons (appendForeach s x y) (appendForeach ss xs ys)--instance MonoidForeach f => MonoidForeach (Rec f) where- emptyForeach SingListNil = RecNil- emptyForeach (SingListCons s ss) = RecCons (emptyForeach s) (emptyForeach ss)--instance SemigroupForall f => SemigroupForall (Rec f) where- appendForall = recZipWith appendForall--instance ToJSONForall f => AE.ToJSON (Rec f as) where- toJSON = toJSONForall--instance ToJSONForall f => ToJSONForall (Rec f) where- toJSONForall = AE.toJSON . go- where- go :: forall g xs. ToJSONForall g => Rec g xs -> [AE.Value]- go RecNil = []- go (RecCons x xs) = toJSONForall x : go xs--instance (FromJSONForeach f, Reify as) => AE.FromJSON (Rec f as) where- parseJSON = parseJSONForeach reify--instance FromJSONForeach f => FromJSONForeach (Rec f) where- parseJSONForeach s0 = AE.withArray "Rec" $ \vs -> do- let go :: SingList as -> Int -> AET.Parser (Rec f as)- go SingListNil !ix = if V.length vs == ix- then return RecNil- else fail "too many elements in array"- go (SingListCons s ss) !ix = if ix < V.length vs- then do- r <- parseJSONForeach s (vs V.! ix)- rs <- go ss (ix + 1)- return (RecCons r rs)- else fail "not enough elements in array"- go s0 0--instance StorableForeach f => StorableForeach (Rec f) where- sizeOfForeach _ SingListNil = 0- sizeOfForeach _ (SingListCons s ss) =- sizeOfForeach (Proxy :: Proxy f) s + sizeOfForeach (Proxy :: Proxy (Rec f)) ss- peekForeach SingListNil _ = return RecNil- peekForeach (SingListCons s ss) ptr = do- r <- peekForeach s (castPtr ptr)- rs <- peekForeach ss (plusPtr ptr (sizeOfForeach (Proxy :: Proxy f) s))- return (RecCons r rs)- pokeForeach _ _ RecNil = return ()- pokeForeach (SingListCons s ss) ptr (RecCons r rs) = do- pokeForeach s (castPtr ptr) r- pokeForeach ss (plusPtr ptr (sizeOfForeach (Proxy :: Proxy f) s)) rs--instance (StorableForeach f, Reify as) => Storable (Rec f as) where- sizeOf _ = sizeOfForeach (Proxy :: Proxy (Rec f)) (reify :: SingList as)- alignment _ = sizeOf (undefined :: Rec f as)- poke = pokeForeach (reify :: SingList as)- peek = peekForeach (reify :: SingList as)--instance BinaryForeach f => BinaryForeach (Rec f) where- putForeach SingListNil RecNil = return ()- putForeach (SingListCons s ss) (RecCons r rs) = do- putForeach s r- putForeach ss rs- getForeach SingListNil = return RecNil- getForeach (SingListCons s ss) =- liftA2 RecCons (getForeach s) (getForeach ss)--instance FromJSONExists f => FromJSONExists (Rec f) where- parseJSONExists = AE.withArray "Rec" $ \vs -> - foldrM go (Exists RecNil) vs- where- go :: forall g. FromJSONExists g => AE.Value -> Exists (Rec g) -> AET.Parser (Exists (Rec g))- go v (Exists rs) = do- Exists r <- parseJSONExists v :: AET.Parser (Exists g)- return (Exists (RecCons r rs))--recZipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs-recZipWith _ RecNil RecNil = RecNil-recZipWith f (RecCons a as) (RecCons b bs) =- RecCons (f a b) (recZipWith f as bs)-