quantification 0.5.0 → 0.8
raw patch · 6 files changed
Files
- quantification.cabal +9/−14
- src/Data/Binary/Lifted.hs +0/−1
- src/Data/Exists.hs +7/−228
- src/Data/Monoid/Lifted.hs +1/−2
- src/Topaz/Rec.hs +0/−122
- src/Topaz/Types.hs +0/−277
quantification.cabal view
@@ -1,10 +1,10 @@-cabal-version: 2.0+cabal-version: 2.4 name: quantification-version: 0.5.0+version: 0.8 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,18 +18,13 @@ Data.Binary.Lifted Data.Exists Data.Monoid.Lifted- Topaz.Rec- Topaz.Types- build-depends: - base >= 4.9 && < 5- , binary >= 0.8 && < 0.10- , ghc-prim >= 0.5 && < 0.6- , hashable >= 1.2 && < 1.3- , aeson >= 1.0 && < 1.5- , text >= 1.0 && < 2.0+ build-depends:+ , base >= 4.11.1 && < 5+ , binary >= 0.8 && < 0.11+ , hashable >= 1.4 && < 1.5+ , text >= 1.0 && < 2.2 , path-pieces >= 0.2 && < 0.3- , vector >= 0.11 && < 0.13- , containers >= 0.5 && < 0.6+ , containers >= 0.5 && < 0.7 , unordered-containers >= 0.2 && < 0.3 default-language: Haskell2010 ghc-options: -O2 -Wall
src/Data/Binary/Lifted.hs view
@@ -11,7 +11,6 @@ import Data.Binary (Get,Put,Binary,get,put) import Data.Functor.Compose (Compose(..)) import Data.Word (Word8)-import Data.Semigroup ((<>)) class Binary1 f where liftPut :: (a -> Put) -> f a -> Put
src/Data/Exists.hs view
@@ -2,17 +2,13 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UnboxedTuples #-} @@ -58,16 +54,6 @@ , HashableForall(..) , HashableForeach(..) , PathPieceExists(..)- , FromJSONForeach(..)- , FromJSONExists(..)- , ToJSONForall(..)- , ToJSONForeach(..)- , ToJSONKeyFunctionForall(..)- , FromJSONKeyFunctionForeach(..)- , ToJSONKeyForall(..)- , ToJSONKeyForeach(..)- , FromJSONKeyExists(..)- , FromJSONKeyForeach(..) , StorableForeach(..) , StorableForall(..) , PrimForall(..)@@ -89,8 +75,6 @@ , EqSing(..) , OrdSing(..) , ShowSing(..)- , ToJSONSing(..)- , FromJSONSing(..) , ToSing(..) , SingKind(..) -- * Functions@@ -105,8 +89,6 @@ -- ** Defaulting , defaultEqForallPoly , defaultCompareForallPoly- , parseJSONMapForeachKey- , toJSONMapForeachKey -- ** Weakening , weakenEquality , weakenOrdering@@ -118,38 +100,24 @@ ) where import Control.Applicative (Const(..))-import Data.Aeson (ToJSON(..),FromJSON(..))-import Data.Aeson (ToJSONKey(..),FromJSONKey(..))-import Data.Aeson (ToJSONKeyFunction(..),FromJSONKeyFunction(..))-import Data.Aeson.Internal ((<?>),JSONPathElement(Key,Index)) import Data.Binary (Get,Put,Binary) import Data.Binary.Lifted (Binary1(..))-import Data.Coerce (coerce) import Data.Functor.Classes (Eq1(..),Show1(..),Ord1(..),eq1,compare1) import Data.Functor.Compose (Compose(..)) import Data.Functor.Product (Product(..)) import Data.Functor.Sum (Sum(..)) import Data.Hashable (Hashable(..)) import Data.Kind (Type)-import Data.Map.Strict (Map) import Data.Monoid.Lifted (Semigroup1(..),Monoid1(..),append1,empty1) import Data.Proxy (Proxy(..))-import Data.Semigroup (Semigroup) import Data.Text (Text) import Data.Type.Equality ((:~:)(Refl),TestEquality(..)) import Foreign.Ptr (Ptr) import GHC.Exts (dataToTag#,State#,Int#,Proxy#,Addr#,ByteArray#,MutableByteArray#) import GHC.Int (Int(..)) -import qualified Data.Aeson.Encoding as Aeson-import qualified Data.Aeson.Encoding.Internal as AEI-import qualified Data.Aeson.Types as Aeson import qualified Data.Binary as BN-import qualified Data.HashMap.Strict as HM-import qualified Data.Map.Strict as M import qualified Data.Semigroup as SG-import qualified Data.Traversable as TRV-import qualified Data.Vector as V import qualified Text.Read as R import qualified Web.PathPieces as PP @@ -181,13 +149,6 @@ WitnessedOrderingEQ :: WitnessedOrdering a a WitnessedOrderingGT :: WitnessedOrdering a b -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 FromJSONKeyFunctionForeach f- = FromJSONKeyTextParserForeach !(forall a. Sing a -> Text -> Aeson.Parser (f a))- | FromJSONKeyValueForeach !(forall a. Sing a -> Aeson.Value -> Aeson.Parser (f a))- newtype ApplyForall f a = ApplyForall { getApplyForall :: f a } instance ShowForall f => Show (ApplyForall f a) where@@ -215,7 +176,7 @@ instance (Monoid1 f, Monoid a) => Monoid (ApplyLifted f a) where mempty = empty1 - mappend = liftAppend mappend+ mappend = (<>) instance (Eq1 f, Eq a) => Eq (ApplyLifted f a) where (==) = eq1 @@ -257,12 +218,6 @@ mempty = emptyForeach reify mappend = (SG.<>) -instance (ToJSONForeach f, Reify a) => ToJSON (ApplyForeach f a) where- toJSON = toJSONForeach reify--instance (FromJSONForeach f, Reify a) => FromJSON (ApplyForeach f a) where- parseJSON = parseJSONForeach reify- instance EqForeach f => EqForeach (ApplyForeach f) where eqForeach s (ApplyForeach a) (ApplyForeach b) = eqForeach s a b @@ -275,56 +230,6 @@ instance MonoidForeach f => MonoidForeach (ApplyForeach f) where emptyForeach s = ApplyForeach (emptyForeach s) -instance ToJSONForeach f => ToJSONForeach (ApplyForeach f) where- toJSONForeach s (ApplyForeach x) = toJSONForeach s x--instance FromJSONForeach f => FromJSONForeach (ApplyForeach f) where- parseJSONForeach s = fmap ApplyForeach . parseJSONForeach s--instance ToJSONKeyForeach f => ToJSONKeyForeach (ApplyForeach f) where- toJSONKeyForeach = case toJSONKeyForeach of- ToJSONKeyTextForall f g -> ToJSONKeyTextForall- (\(Pair s (ApplyForeach x)) -> f (Pair s x))- (\(Pair s (ApplyForeach x)) -> g (Pair s x))- ToJSONKeyValueForall f g -> ToJSONKeyValueForall- (\(Pair s (ApplyForeach x)) -> f (Pair s x))- (\(Pair s (ApplyForeach x)) -> g (Pair s x))--instance FromJSONKeyForeach f => FromJSONKeyForeach (ApplyForeach f) where- fromJSONKeyForeach = case fromJSONKeyForeach of- FromJSONKeyTextParserForeach f -> FromJSONKeyTextParserForeach (\s t -> fmap ApplyForeach (f s t))- FromJSONKeyValueForeach f -> FromJSONKeyValueForeach (\s t -> fmap ApplyForeach (f s t))--instance (ToJSONKeyForeach f, Reify a) => ToJSONKey (ApplyForeach f a) where- toJSONKey = case toJSONKeyForeach of- ToJSONKeyTextForall toText toEnc -> ToJSONKeyText- (\(ApplyForeach x) -> toText (Pair reify x))- (\(ApplyForeach x) -> toEnc (Pair reify x))- ToJSONKeyValueForall toValue toEnc -> ToJSONKeyValue- (\(ApplyForeach x) -> toValue (Pair reify x))- (\(ApplyForeach x) -> toEnc (Pair reify x))- toJSONKeyList = case toJSONKeyForeach of- ToJSONKeyTextForall toText toEnc -> ToJSONKeyValue- (\xs -> toJSON $ map (\(ApplyForeach x) -> toText (Pair reify x)) xs)- (\xs -> Aeson.list (textEncodingToValueEncoding . toEnc . Pair reify) (map getApplyForeach xs))- ToJSONKeyValueForall toValue toEnc -> ToJSONKeyValue- (\xs -> toJSON $ map (\(ApplyForeach x) -> toValue (Pair reify x)) xs)- (\xs -> Aeson.list (toEnc . Pair reify) (map getApplyForeach xs))---- this is always safe-textEncodingToValueEncoding :: Aeson.Encoding' Text -> Aeson.Encoding' Aeson.Value-textEncodingToValueEncoding = AEI.retagEncoding--instance (FromJSONKeyForeach f, Reify a) => FromJSONKey (ApplyForeach f a) where- fromJSONKey = case fromJSONKeyForeach of- FromJSONKeyTextParserForeach f -> FromJSONKeyTextParser (fmap ApplyForeach . f reify)- FromJSONKeyValueForeach f -> FromJSONKeyValue (fmap ApplyForeach . f reify)- fromJSONKeyList = case fromJSONKeyForeach of- FromJSONKeyTextParserForeach f -> FromJSONKeyValue $ Aeson.withArray "ApplyForeach" $ \xs -> do- fmap V.toList (mapM (fmap ApplyForeach . Aeson.withText "ApplyForeach" (f reify)) xs)- FromJSONKeyValueForeach f -> FromJSONKeyValue $ Aeson.withArray "ApplyForeach" $ \xs -> do- fmap V.toList (mapM (fmap ApplyForeach . f reify) xs)- class EqForall f where eqForall :: f a -> f a -> Bool @@ -391,30 +296,6 @@ class HashableForeach f where hashWithSaltForeach :: Sing a -> Int -> f a -> Int -class ToJSONKeyForall f where- toJSONKeyForall :: ToJSONKeyFunctionForall f--class ToJSONKeyForeach f where- toJSONKeyForeach :: ToJSONKeyFunctionForall (Product Sing f)--class FromJSONKeyExists f where- fromJSONKeyExists :: FromJSONKeyFunction (Exists f)--class FromJSONKeyForeach f where- fromJSONKeyForeach :: FromJSONKeyFunctionForeach f--class ToJSONForall f where- toJSONForall :: f a -> Aeson.Value--class ToJSONForeach f where- toJSONForeach :: Sing a -> f a -> Aeson.Value--class FromJSONForeach f where- parseJSONForeach :: Sing a -> Aeson.Value -> Aeson.Parser (f a)--class FromJSONExists f where- parseJSONExists :: Aeson.Value -> Aeson.Parser (Exists f)- class EnumForall f where toEnumForall :: Int -> f a fromEnumForall :: f a -> Int@@ -515,20 +396,6 @@ instance Hashable a => HashableForall (Const a) where hashWithSaltForall s (Const a) = hashWithSalt s a -instance FromJSON a => FromJSONForeach (Const a) where- parseJSONForeach _ = fmap Const . parseJSON----- I need to get rid of the ToJSONForall and FromJSONForeach constraints--- on these two instances.-instance (ToJSONKeyForall f, ToJSONForall f) => ToJSONKey (Exists f) where- toJSONKey = case toJSONKeyForall of- ToJSONKeyTextForall t e -> ToJSONKeyText (\(Exists a) -> t a) (\(Exists a) -> e a)- ToJSONKeyValueForall v e -> ToJSONKeyValue (\x -> case x of Exists a -> v a) (\(Exists a) -> e a)--instance (FromJSONKeyExists f, FromJSONExists f) => FromJSONKey (Exists f) where- fromJSONKey = fromJSONKeyExists- instance EqForallPoly f => Eq (Exists f) where Exists a == Exists b = weakenEquality (eqForallPoly a b) @@ -538,15 +405,9 @@ instance OrdForallPoly f => Ord (Exists f) where compare (Exists a) (Exists b) = weakenOrdering (compareForallPoly a b) -instance HashableForall f => Hashable (Exists f) where+instance (EqForallPoly f, HashableForall f) => Hashable (Exists f) where hashWithSalt s (Exists a) = hashWithSaltForall s a -instance ToJSONForall f => ToJSON (Exists f) where- toJSON (Exists a) = toJSONForall a--instance FromJSONExists f => FromJSON (Exists f) where- parseJSON v = parseJSONExists v- instance ShowForall f => Show (Exists f) where showsPrec p (Exists a) = showParen (p >= 11) @@ -604,20 +465,12 @@ (p >= 11) (showString "Pair " . showsPrecForall 11 f . showChar ' ' . showsPrecForall 11 g) +instance (Ord1 f, OrdForeach g) => OrdForeach (Compose f g) where+ compareForeach s (Compose x) (Compose y) = liftCompare (compareForeach s) x y+ instance (Semigroup1 f, SemigroupForall g) => SemigroupForall (Compose f g) where appendForall (Compose x) (Compose y) = Compose (liftAppend appendForall x y) -instance (Aeson.ToJSON1 f, ToJSONForall g) => ToJSONForall (Compose f g) where- toJSONForall (Compose x) = Aeson.liftToJSON toJSONForall (Aeson.toJSON . map toJSONForall) x--instance (Aeson.ToJSON1 f, ToJSONForeach g) => ToJSONForeach (Compose f g) where- toJSONForeach s (Compose x) = Aeson.liftToJSON (toJSONForeach s) (Aeson.toJSON . map (toJSONForeach s)) x--instance (Aeson.FromJSON1 f, FromJSONForeach g) => FromJSONForeach (Compose f g) where- parseJSONForeach s = fmap Compose . Aeson.liftParseJSON- (parseJSONForeach s)- (Aeson.withArray "Compose" (fmap V.toList . V.mapM (parseJSONForeach s)))- instance (Eq1 f, EqForall g) => EqForall (Compose f g) where eqForall (Compose x) (Compose y) = liftEq eqForall x y @@ -729,7 +582,7 @@ instance EqSing a => EqSing [a] where eqSing = eqSingList -eqSingList :: forall (a :: [k]) (b :: [k]). EqSing k => SingList a -> SingList b -> Maybe (a :~: b)+eqSingList :: forall (k :: Type) (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@@ -783,7 +636,7 @@ SingMaybeJust :: Sing a -> SingMaybe ('Just a) SingMaybeNothing :: SingMaybe 'Nothing -unreifyList :: forall (as :: [k]) b. Unreify k+unreifyList :: forall (k :: Type) (as :: [k]) (b :: Type) . Unreify k => SingList as -> (Reify as => b) -> b@@ -810,80 +663,6 @@ class ToSing (f :: k -> Type) where toSing :: f a -> Sing a--class ToJSONSing k where- toJSONSing :: forall (a :: k). Sing a -> Aeson.Value--instance (ToJSONForeach f, ToJSONSing k) => ToJSON (Some (f :: k -> Type)) where- toJSON (Some s v) = toJSON [toJSONSing s, toJSONForeach s v]--class FromJSONSing k where- parseJSONSing :: Aeson.Value -> Aeson.Parser (Exists (Sing :: k -> Type))--instance (FromJSONForeach 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 <- parseJSONForeach s y- return (Some s val)- else fail "array of length 2 expected"---- This name is not great. I need to figure out a better naming--- scheme that allows this area to grow.-toJSONMapForeachKey :: (ToJSONKeyForeach f, ToJSONForeach v)- => Sing a- -> Map (f a) (v a)- -> Aeson.Value-toJSONMapForeachKey s m = case toJSONKeyForeach of- ToJSONKeyTextForall keyToText _ -> toJSON $ M.foldlWithKey'- ( \hm key val -> HM.insert (keyToText (Pair s key)) (toJSONForeach s val) hm- ) HM.empty m- ToJSONKeyValueForall keyToValue _ -> toJSON $ M.foldrWithKey' - ( \key val xs -> (keyToValue (Pair s key), toJSONForeach s val) : xs- ) [] m---- | Parse a 'Map' whose key type is higher-kinded. This only creates a valid 'Map'--- if the 'OrdForeach' instance agrees with the 'Ord' instance.-parseJSONMapForeachKey :: forall k (f :: k -> Type) (a :: k) v. (FromJSONKeyForeach f, OrdForeach f, Unreify k)- => (Aeson.Value -> Aeson.Parser v) - -> Sing a- -> Aeson.Value- -> Aeson.Parser (Map (f a) v)-parseJSONMapForeachKey valueParser s obj = unreify s $ case fromJSONKeyForeach of- FromJSONKeyTextParserForeach f -> Aeson.withObject "Map k v"- ( fmap (M.mapKeysMonotonic getApplyForeach) . HM.foldrWithKey- (\k v m -> M.insert- <$> (coerce (f s k :: Aeson.Parser (f a)) :: Aeson.Parser (ApplyForeach f a)) <?> Key k- <*> valueParser v <?> Key k- <*> m- ) (pure M.empty)- ) obj- FromJSONKeyValueForeach f -> Aeson.withArray "Map k v"- ( fmap (M.mapKeysMonotonic getApplyForeach . M.fromList)- . (coerce :: Aeson.Parser [(f a, v)] -> Aeson.Parser [(ApplyForeach 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 weakenEquality :: WitnessedEquality a b -> Bool weakenEquality = \case
src/Data/Monoid/Lifted.hs view
@@ -13,8 +13,7 @@ import Data.Map.Strict (Map) import Data.Monoid import Data.Proxy (Proxy(..))-import Data.Semigroup (Semigroup)-import Data.Functor.Const (Const(..))+ import qualified Data.Functor.Product as FP import qualified Data.HashMap.Strict as HM import qualified Data.Map.Strict as M
− src/Topaz/Rec.hs
@@ -1,122 +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- -- * Access- , get- , put- , gets- , puts- -- * Conversion- , fromSingList- , toSingList- ) where--import Prelude hiding (map,zipWith,foldMap,traverse)-import Topaz.Types (Elem(..),type (++),Rec(..))-import Data.Exists-import Data.Semigroup (Semigroup)-import qualified Data.Semigroup as SG--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)---- | 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)-
− src/Topaz/Types.hs
@@ -1,277 +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.Semigroup (Semigroup)-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)-