quantification 0.2 → 0.3
raw patch · 5 files changed
+524/−164 lines, 5 filesdep +containersdep +unordered-containersdep ~aeson
Dependencies added: containers, unordered-containers
Dependency ranges changed: aeson
Files
- quantification.cabal +5/−2
- src/Data/Exists.hs +153/−6
- src/Data/Monoid/Lifted.hs +98/−6
- src/Topaz/Rec.hs +40/−150
- src/Topaz/Types.hs +228/−0
quantification.cabal view
@@ -1,5 +1,5 @@ name: quantification-version: 0.2+version: 0.3 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@@ -18,14 +18,17 @@ Data.Exists Data.Monoid.Lifted Topaz.Rec+ Topaz.Types build-depends: base >= 4.9 && < 5 , ghc-prim >= 0.5 && < 0.6 , hashable >= 1.2 && < 1.3- , aeson >= 0.11 && < 1.2+ , aeson >= 0.11 && < 1.3 , text >= 1.0 && < 2.0 , path-pieces >= 0.2 && < 0.3 , vector >= 0.11 && < 0.13+ , containers >= 0.5 && < 0.6+ , unordered-containers >= 0.2 && < 0.3 default-language: Haskell2010 source-repository head
src/Data/Exists.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeInType #-} {-# LANGUAGE CPP #-} {-# OPTIONS_GHC -Wall #-}@@ -27,6 +28,7 @@ Exists(..) , Exists2(..) , Exists3(..)+ , Some(..) -- * Type Classes , EqForall(..) , EqForallPoly(..)@@ -44,8 +46,11 @@ , FromJSONExists(..) , ToJSONForall(..) #if MIN_VERSION_aeson(1,0,0) + , ToJSONKeyFunctionForall(..)+ , FromJSONKeyFunctionForall(..) , ToJSONKeyForall(..) , FromJSONKeyExists(..)+ , FromJSONKeyForall(..) #endif , StorableForall(..) -- * Higher Rank Classes@@ -55,8 +60,14 @@ -- * More Type Classes , Sing , SingList(..)+ , SingMaybe(..) , Reify(..) , Unreify(..)+ -- * Sing Type Classes+ , EqSing(..)+ , ToJSONSing(..)+ , FromJSONSing(..)+ , ToSing(..) -- * Functions -- ** Show , showsForall@@ -66,6 +77,9 @@ -- ** Defaulting , defaultEqForallPoly , defaultCompareForallPoly+#if MIN_VERSION_aeson(1,0,0) + , parseJSONMapForallKey+#endif -- ** Other , unreifyList ) where@@ -83,6 +97,13 @@ import GHC.Int (Int(..)) import GHC.Prim (dataToTag#) import Foreign.Ptr (Ptr)+import Data.Kind (Type)+import Data.Map.Strict (Map)+import Data.Coerce (coerce)+import qualified Data.Traversable as TRV+import qualified Data.Map.Strict as M+import qualified Data.HashMap.Strict as HM+import qualified Data.Vector as V import qualified Data.Aeson.Types as Aeson import qualified Text.Read as R import qualified Web.PathPieces as PP@@ -91,21 +112,25 @@ import qualified Data.Aeson.Encoding as Aeson import Data.Aeson (ToJSONKey(..),FromJSONKey(..), ToJSONKeyFunction(..),FromJSONKeyFunction(..))+import Data.Aeson.Internal ((<?>),JSONPathElement(Key,Index)) #endif -- newtype Exists (f :: k -> *) = Exists { runExists :: forall r. (forall a. f a -> r) -> r } -- | Hide a type parameter.-data Exists (f :: k -> *) = forall a. Exists !(f a)+data Exists (f :: k -> Type) = forall a. Exists !(f a) -data Exists2 (f :: k -> j -> *) = forall a b. Exists2 !(f a b)+data Exists2 (f :: k -> j -> Type) = forall a b. Exists2 !(f a b) -data Exists3 (f :: k -> j -> l -> *) = forall a b c. Exists3 !(f a b c)+data Exists3 (f :: k -> j -> l -> Type) = forall a b c. Exists3 !(f a b c) #if MIN_VERSION_aeson(1,0,0) data ToJSONKeyFunctionForall f = ToJSONKeyTextForall !(forall a. f a -> Text) !(forall a. f a -> Aeson.Encoding' Text) | ToJSONKeyValueForall !(forall a. f a -> Aeson.Value) !(forall a. f a -> Aeson.Encoding)+data FromJSONKeyFunctionForall f+ = FromJSONKeyTextParserForall !(forall a. Sing a -> Text -> Aeson.Parser (f a))+ | FromJSONKeyValueForall !(forall a. Sing a -> Aeson.Value -> Aeson.Parser (f a)) #endif class EqForall f where@@ -162,6 +187,9 @@ class FromJSONKeyExists f where fromJSONKeyExists :: FromJSONKeyFunction (Exists f)++class FromJSONKeyForall f where+ fromJSONKeyForall :: FromJSONKeyFunctionForall f #endif class ToJSONForall f where@@ -188,7 +216,7 @@ class SemigroupForall f where sappendForall :: f a -> f a -> f a -class StorableForall (f :: k -> *) where+class StorableForall (f :: k -> Type) where peekForall :: Sing a -> Ptr (f a) -> IO (f a) pokeForall :: Ptr (f a) -> f a -> IO () sizeOfFunctorForall :: f a -> Int@@ -311,6 +339,14 @@ (p >= 11) (showString "Pair " . showsPrecForall 11 f . showChar ' ' . showsPrecForall 11 g) +instance (Aeson.ToJSON1 f, ToJSONForall g) => ToJSONForall (Compose f g) where+ toJSONForall (Compose x) = Aeson.liftToJSON toJSONForall (Aeson.toJSON . map toJSONForall) x++instance (Aeson.FromJSON1 f, FromJSONForall g) => FromJSONForall (Compose f g) where+ parseJSONForall s = fmap Compose . Aeson.liftParseJSON+ (parseJSONForall s)+ (Aeson.withArray "Compose" (fmap V.toList . V.mapM (parseJSONForall s)))+ instance (Eq1 f, EqForall g) => EqForall (Compose f g) where eqForall (Compose x) (Compose y) = liftEq eqForall x y @@ -358,13 +394,17 @@ getTagBox !x = I# (dataToTag# x) {-# INLINE getTagBox #-} -type family Sing = (r :: k -> *) | r -> k+type family Sing = (r :: k -> Type) | r -> k type instance Sing = SingList+type instance Sing = SingMaybe class Unreify k where unreify :: forall (a :: k) b. Sing a -> (Reify a => b) -> b +instance Unreify k => Unreify [k] where+ unreify = unreifyList+ class Reify a where reify :: Sing a @@ -374,18 +414,125 @@ instance (Reify a, Reify as) => Reify (a ': as) where reify = SingListCons reify reify +instance Reify 'Nothing where+ reify = SingMaybeNothing++instance Reify a => Reify ('Just a) where+ reify = SingMaybeJust reify++class EqSing k where+ eqSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> Maybe (a :~: b)++instance EqSing a => EqSing [a] where+ eqSing = eqSingList++eqSingList :: forall (a :: [k]) (b :: [k]). EqSing k => SingList a -> SingList b -> Maybe (a :~: b)+eqSingList SingListNil SingListNil = Just Refl+eqSingList SingListNil (SingListCons _ _) = Nothing+eqSingList (SingListCons _ _) SingListNil = Nothing+eqSingList (SingListCons a as) (SingListCons b bs) = case eqSing a b of+ Just Refl -> case eqSingList as bs of+ Just Refl -> Just Refl+ Nothing -> Nothing+ Nothing -> Nothing+ class SemigroupForall f => MonoidForall f where memptyForall :: Sing a -> f a -data SingList :: [k] -> * where+data SingList :: [k] -> Type where SingListNil :: SingList '[] SingListCons :: Sing r -> SingList rs -> SingList (r ': rs) +data SingMaybe :: Maybe k -> Type where+ SingMaybeJust :: Sing a -> SingMaybe ('Just a)+ SingMaybeNothing :: SingMaybe 'Nothing+ unreifyList :: forall (as :: [k]) b. Unreify k => SingList as -> (Reify as => b) -> b unreifyList SingListNil b = b unreifyList (SingListCons s ss) b = unreify s (unreifyList ss b)++data Some (f :: k -> Type) = forall a. Some !(Sing a) !(f a)++instance (EqForall f, EqSing k) => Eq (Some (f :: k -> Type)) where + Some s1 v1 == Some s2 v2 = case eqSing s1 s2 of+ Just Refl -> eqForall v1 v2+ Nothing -> False++class ToSing (f :: k -> Type) where+ toSing :: f a -> Sing a++class ToJSONSing k where+ toJSONSing :: forall (a :: k). Sing a -> Aeson.Value++instance (ToJSONForall f, ToJSONSing k) => ToJSON (Some (f :: k -> Type)) where+ toJSON (Some s v) = toJSON [toJSONSing s, toJSONForall v]++class FromJSONSing k where+ parseJSONSing :: Aeson.Value -> Aeson.Parser (Exists (Sing :: k -> Type))++instance (FromJSONForall f, FromJSONSing k) => FromJSON (Some (f :: k -> Type)) where+ parseJSON = Aeson.withArray "Some" $ \v -> if V.length v == 2+ then do+ let x = V.unsafeIndex v 0+ y = V.unsafeIndex v 1+ Exists s <- parseJSONSing x :: Aeson.Parser (Exists (Sing :: k -> Type))+ val <- parseJSONForall s y+ return (Some s val)+ else fail "array of length 2 expected"++-- only used internally for its instances+newtype Apply f a = Apply { getApply :: f a }++instance EqForall f => Eq (Apply f a) where+ Apply a == Apply b = eqForall a b++instance OrdForall f => Ord (Apply f a) where+ compare (Apply a) (Apply b) = compareForall a b++#if MIN_VERSION_aeson(1,0,0) +-- | Parse a 'Map' whose key type is higher-kinded. This only creates a valid 'Map'+-- if the 'OrdForall' instance agrees with the 'Ord' instance.+parseJSONMapForallKey :: forall f a v. (FromJSONKeyForall f, OrdForall f)+ => (Aeson.Value -> Aeson.Parser v) + -> Sing a+ -> Aeson.Value+ -> Aeson.Parser (Map (f a) v)+parseJSONMapForallKey valueParser s obj = case fromJSONKeyForall of+ FromJSONKeyTextParserForall f -> Aeson.withObject "Map k v"+ ( fmap (M.mapKeysMonotonic getApply) . HM.foldrWithKey+ (\k v m -> M.insert+ <$> (coerce (f s k :: Aeson.Parser (f a)) :: Aeson.Parser (Apply f a)) <?> Key k+ <*> valueParser v <?> Key k+ <*> m+ ) (pure M.empty)+ ) obj+ FromJSONKeyValueForall f -> Aeson.withArray "Map k v"+ ( fmap (M.mapKeysMonotonic getApply . M.fromList)+ . (coerce :: Aeson.Parser [(f a, v)] -> Aeson.Parser [(Apply f a, v)])+ . TRV.sequence+ . zipWith (parseIndexedJSONPair (f s) valueParser) [0..]+ . V.toList+ ) obj++-- copied from aeson+parseIndexedJSONPair :: (Aeson.Value -> Aeson.Parser a) -> (Aeson.Value -> Aeson.Parser b) -> Int -> Aeson.Value -> Aeson.Parser (a, b)+parseIndexedJSONPair keyParser valParser idx value = p value <?> Index idx+ where+ p = Aeson.withArray "(k,v)" $ \ab ->+ let n = V.length ab+ in if n == 2+ then (,) <$> parseJSONElemAtIndex keyParser 0 ab+ <*> parseJSONElemAtIndex valParser 1 ab+ else fail $ "cannot unpack array of length " +++ show n ++ " into a pair"+{-# INLINE parseIndexedJSONPair #-}++-- copied from aeson+parseJSONElemAtIndex :: (Aeson.Value -> Aeson.Parser a) -> Int -> V.Vector Aeson.Value -> Aeson.Parser a+parseJSONElemAtIndex p idx ary = p (V.unsafeIndex ary idx) <?> Index idx+#endif
src/Data/Monoid/Lifted.hs view
@@ -1,18 +1,110 @@ module Data.Monoid.Lifted ( Semigroup1(..)+ , Monoid1(..)+ , append1+ , empty1 ) where +import Data.Functor.Identity import Data.Functor.Compose+import qualified Data.Functor.Product as FP+import Data.Map.Strict (Map)+import Data.HashMap.Strict (HashMap)+import Control.Applicative+import Data.Semigroup (Semigroup)+import Data.Hashable (Hashable)+import Data.Monoid+import Data.Proxy (Proxy(..))+import qualified Data.Semigroup as SG+import qualified Data.Map.Strict as M+import qualified Data.HashMap.Strict as HM +-- | Laws for this typeclass:+--+-- * @liftAppend f a (liftAppend f b c) = liftAppend f (liftAppend f a b) c@ class Semigroup1 f where- sappend1 :: (a -> a -> a) -> f a -> f a -> f a+ liftAppend :: (a -> a -> a) -> f a -> f a -> f a +append1 :: (Semigroup1 f, Semigroup a) => f a -> f a -> f a+append1 = liftAppend (SG.<>)++-- | Laws for this typeclass:+--+-- * @liftAppend f a (liftEmpty mempty) = a@+class Semigroup1 f => Monoid1 f where+ liftEmpty :: a -> f a++empty1 :: (Monoid1 f, Monoid a) => f a+empty1 = liftEmpty mempty+ instance Semigroup1 Maybe where- sappend1 _ Nothing Nothing = Nothing- sappend1 _ a@(Just _) Nothing = a- sappend1 _ Nothing a@(Just _) = a- sappend1 f (Just a) (Just b) = Just (f a b)+ liftAppend _ Nothing Nothing = Nothing+ liftAppend _ a@(Just _) Nothing = a+ liftAppend _ Nothing a@(Just _) = a+ liftAppend f (Just a) (Just b) = Just (f a b) instance (Semigroup1 f, Semigroup1 g) => Semigroup1 (Compose f g) where- sappend1 f (Compose a) (Compose b) = Compose ((sappend1 (sappend1 f)) a b)+ liftAppend f (Compose a) (Compose b) = Compose ((liftAppend (liftAppend f)) a b)++instance (Monoid1 f, Monoid1 g) => Monoid1 (Compose f g) where+ liftEmpty a = Compose (liftEmpty (liftEmpty a))++instance Semigroup1 IO where+ liftAppend = liftA2++instance Monoid1 IO where+ liftEmpty = pure++-- | Disagrees with 'Semigroup' instance for 'Map'+instance Ord k => Semigroup1 (Map k) where+ liftAppend = M.unionWith++-- | Disagrees with 'Semigroup' instance for 'HashMap'+instance (Hashable k, Eq k) => Semigroup1 (HashMap k) where+ liftAppend = HM.unionWith++instance (Hashable k, Eq k) => Monoid1 (HashMap k) where+ liftEmpty _ = HM.empty++instance Semigroup1 [] where+ liftAppend _ = (++)++instance Monoid1 [] where+ liftEmpty _ = []++instance Semigroup1 Identity where+ liftAppend f (Identity a) (Identity b) = Identity (f a b)++instance Monoid1 Identity where+ liftEmpty = Identity++instance (Semigroup1 f, Semigroup1 g) => Semigroup1 (FP.Product f g) where+ liftAppend f (FP.Pair a1 b1) (FP.Pair a2 b2) = FP.Pair (liftAppend f a1 a2) (liftAppend f b1 b2)++instance (Monoid1 f, Monoid1 g) => Monoid1 (FP.Product f g) where+ liftEmpty a = FP.Pair (liftEmpty a) (liftEmpty a)++instance Semigroup1 Dual where+ liftAppend f (Dual a) (Dual b) = Dual (f b a)++instance Monoid1 Dual where+ liftEmpty a = Dual a++instance Semigroup a => Semigroup1 ((,) a) where+ liftAppend f (a1,b1) (a2,b2) = (a1 SG.<> a2, f b1 b2)++instance (Semigroup a, Monoid a) => Monoid1 ((,) a) where+ liftEmpty b = (mempty,b)++instance Semigroup1 Proxy where+ liftAppend _ _ _ = Proxy++instance Monoid1 Proxy where+ liftEmpty _ = Proxy++instance Semigroup1 ((->) a) where+ liftAppend combine f g a = combine (f a) (g a)++instance Monoid1 ((->) a) where+ liftEmpty b _ = b
src/Topaz/Rec.hs view
@@ -1,179 +1,46 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE BangPatterns #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -Wall #-} module Topaz.Rec ( Rec(..) , map+ , append , traverse , traverse_ , zipWith , foldMap , foldMap1+ -- * Access+ , get+ , put+ , gets+ , puts+ -- * Conversion+ , fromSingList ) where import Prelude hiding (map,zipWith,foldMap,traverse)+import Topaz.Types (Elem(..),type (++),Rec(..))+import Topaz.Types (Elem(..),Rec(..)) import Data.Exists-import Data.Type.Equality-import Data.Type.Coercion-import Data.Foldable (foldrM) import Data.Proxy (Proxy(..))-import Foreign.Ptr (castPtr,plusPtr)-import Foreign.Storable (Storable(..)) import Data.Semigroup (Semigroup)-import Data.Hashable (Hashable(..)) import qualified Data.Semigroup as SG import qualified Data.Vector as V-import qualified Data.Aeson as AE-import qualified Data.Aeson.Types as AET -data Rec :: (k -> *) -> [k] -> * where- RecNil :: Rec f '[]- RecCons :: f r -> Rec f rs -> Rec f (r ': rs)--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 EqForall f => Eq (Rec f as) where- (==) = eqForall--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 EqForall f => EqForall (Rec f) where- eqForall RecNil RecNil = True- eqForall (RecCons a as) (RecCons b bs) =- eqForall a b && eqForall as bs--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 SemigroupForall f => Semigroup (Rec f as) where- (<>) = zipWith sappendForall--instance (MonoidForall f, Reify as) => Monoid (Rec f as) where- mempty = map memptyForall (singListToRec reify)- mappend = zipWith sappendForall--instance MonoidForall f => MonoidForall (Rec f) where- memptyForall SingListNil = RecNil- memptyForall (SingListCons s ss) = RecCons (memptyForall s) (memptyForall ss)--instance SemigroupForall f => SemigroupForall (Rec f) where- sappendForall = zipWith sappendForall--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 (FromJSONForall f, Reify as) => AE.FromJSON (Rec f as) where- parseJSON = parseJSONForall reify--instance FromJSONForall f => FromJSONForall (Rec f) where- parseJSONForall 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 <- parseJSONForall s (vs V.! ix)- rs <- go ss (ix + 1)- return (RecCons r rs)- else fail "not enough elements in array"- go s0 0--instance StorableForall f => StorableForall (Rec f) where- sizeOfFunctorForall RecNil = 0- sizeOfFunctorForall (RecCons r rs) =- sizeOfFunctorForall r + sizeOfFunctorForall rs- sizeOfForall _ SingListNil = 0- sizeOfForall _ (SingListCons s ss) =- sizeOfForall (Proxy :: Proxy f) s + sizeOfForall (Proxy :: Proxy (Rec f)) ss- peekForall SingListNil _ = return RecNil- peekForall (SingListCons s ss) ptr = do- r <- peekForall s (castPtr ptr)- rs <- peekForall ss (plusPtr ptr (sizeOfForall (Proxy :: Proxy f) s))- return (RecCons r rs)- pokeForall _ RecNil = return ()- pokeForall ptr (RecCons r rs) = do- pokeForall (castPtr ptr) r- pokeForall (plusPtr ptr (sizeOfFunctorForall r)) rs--instance (StorableForall f, Reify as) => Storable (Rec f as) where- sizeOf _ = sizeOfForall (Proxy :: Proxy (Rec f)) (reify :: SingList as)- alignment _ = sizeOf (undefined :: Rec f as)- poke = pokeForall- peek = peekForall (reify :: SingList as)--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))--singListToRec :: SingList as -> Rec Sing as-singListToRec SingListNil = RecNil-singListToRec (SingListCons r rs) = RecCons r (singListToRec rs)- 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)@@ -227,4 +94,27 @@ 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)
+ src/Topaz/Types.hs view
@@ -0,0 +1,228 @@+{-# 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(..)+ , type (++)+ ) where++import Data.Exists+import Data.Hashable (Hashable(..))+import Foreign.Storable (Storable(..))+import Data.Type.Equality+import Data.Type.Coercion+import Data.Semigroup (Semigroup)+import Data.Proxy (Proxy(..))+import Foreign.Ptr (castPtr,plusPtr)+import Data.Foldable (foldrM)+import Data.Kind (Type)+import Data.Monoid.Lifted (Semigroup1(..), Monoid1(..), append1)+import qualified Data.Semigroup as SG+import qualified Data.Aeson as AE+import qualified Data.Aeson.Types as AET+import qualified Data.Vector as V++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 EqForall f => Eq (Rec f as) where+ (==) = eqForall++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 EqForall f => EqForall (Rec f) where+ eqForall RecNil RecNil = True+ eqForall (RecCons a as) (RecCons b bs) =+ eqForall a b && eqForall as bs++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 SemigroupForall f => Semigroup (Rec f as) where+ (<>) = recZipWith sappendForall++instance (MonoidForall f, Reify as) => Monoid (Rec f as) where+ mempty = recMap memptyForall (singListToRec reify)+ mappend = recZipWith sappendForall++instance MonoidForall f => MonoidForall (Rec f) where+ memptyForall SingListNil = RecNil+ memptyForall (SingListCons s ss) = RecCons (memptyForall s) (memptyForall ss)++instance SemigroupForall f => SemigroupForall (Rec f) where+ sappendForall = recZipWith sappendForall++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 (FromJSONForall f, Reify as) => AE.FromJSON (Rec f as) where+ parseJSON = parseJSONForall reify++instance FromJSONForall f => FromJSONForall (Rec f) where+ parseJSONForall 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 <- parseJSONForall s (vs V.! ix)+ rs <- go ss (ix + 1)+ return (RecCons r rs)+ else fail "not enough elements in array"+ go s0 0++instance StorableForall f => StorableForall (Rec f) where+ sizeOfFunctorForall RecNil = 0+ sizeOfFunctorForall (RecCons r rs) =+ sizeOfFunctorForall r + sizeOfFunctorForall rs+ sizeOfForall _ SingListNil = 0+ sizeOfForall _ (SingListCons s ss) =+ sizeOfForall (Proxy :: Proxy f) s + sizeOfForall (Proxy :: Proxy (Rec f)) ss+ peekForall SingListNil _ = return RecNil+ peekForall (SingListCons s ss) ptr = do+ r <- peekForall s (castPtr ptr)+ rs <- peekForall ss (plusPtr ptr (sizeOfForall (Proxy :: Proxy f) s))+ return (RecCons r rs)+ pokeForall _ RecNil = return ()+ pokeForall ptr (RecCons r rs) = do+ pokeForall (castPtr ptr) r+ pokeForall (plusPtr ptr (sizeOfFunctorForall r)) rs++instance (StorableForall f, Reify as) => Storable (Rec f as) where+ sizeOf _ = sizeOfForall (Proxy :: Proxy (Rec f)) (reify :: SingList as)+ alignment _ = sizeOf (undefined :: Rec f as)+ poke = pokeForall+ peek = peekForall (reify :: SingList as)++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))++singListToRec :: SingList as -> Rec Sing as+singListToRec SingListNil = RecNil+singListToRec (SingListCons r rs) = RecCons r (singListToRec 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)++recMap :: (forall x. f x -> g x) -> Rec f as -> Rec g as+recMap _ RecNil = RecNil+recMap f (RecCons x xs) = RecCons (f x) (recMap f xs)+