topaz (empty) → 0.6.0
raw patch · 5 files changed
+484/−0 lines, 5 filesdep +aesondep +basedep +binarysetup-changed
Dependencies added: aeson, base, binary, hashable, quantification, vector
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- src/Topaz/Rec.hs +144/−0
- src/Topaz/Types.hs +276/−0
- topaz.cabal +32/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Andrew Martin (c) 2016++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 Andrew Martin 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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Topaz/Rec.hs view
@@ -0,0 +1,144 @@+{-# 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 view
@@ -0,0 +1,276 @@+{-# 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 :: forall (k :: Type). (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 :: forall (k :: Type). (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)+
+ topaz.cabal view
@@ -0,0 +1,32 @@+cabal-version: 2.4+name: topaz+version: 0.6.0+synopsis: Extensible records library+description: Provides extensible records types built on top of the quantification library+homepage: https://github.com/andrewthad/quantification#readme+license: BSD-3-Clause+license-file: LICENSE+author: Andrew Martin+maintainer: andrew.thaddeus@gmail.com+copyright: 2018 Andrew Martin+category: Web+build-type: Simple++library+ hs-source-dirs: src+ exposed-modules:+ Topaz.Rec+ Topaz.Types+ build-depends:+ , base >= 4.11.1 && < 5+ , binary >= 0.8 && < 0.11+ , hashable >= 1.2 && < 1.4+ , aeson >= 1.0 && < 1.6+ , vector >= 0.11 && < 0.13+ , quantification >= 0.6.0+ default-language: Haskell2010+ ghc-options: -O2 -Wall++source-repository head+ type: git+ location: https://github.com/andrewthad/quantification