named-sop (empty) → 0.1.0.0
raw patch · 8 files changed
+635/−0 lines, 8 filesdep +basedep +singletonsdep +text
Dependencies added: base, singletons, text
Files
- CHANGELOG.md +4/−0
- LICENSE +20/−0
- README.md +22/−0
- named-sop.cabal +49/−0
- src/Data/NamedSOP/Generic.hs +167/−0
- src/Data/NamedSOP/Map.hs +128/−0
- src/Data/NamedSOP/Sum.hs +136/−0
- src/Data/NamedSOP/Type.hs +109/−0
+ CHANGELOG.md view
@@ -0,0 +1,4 @@+# 0.1.0.0++Initial release. Expect the public-facing API to change as the+library is reworked.
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2019 Sam Schweigel++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ README.md view
@@ -0,0 +1,22 @@+# named-sop: Dependently-typed sums and products, tagged by field name++[](https://hackage.haskell.org/package/named-sop)+[](http://travis-ci.org/sjsch/named-sop)++Sums and Maps (products) indexed by a typelevel map of their field+(or constructor) names and types. They can be combined and split+again; their typelevel map is sorted to ensure that the end result+is independent of the order you combine it in.++"Data.NamedSOP.Generic" contains functions for automatically+converting between types with a Generic instance and named sums of+products:++```haskell+>>> data A = C { a :: Int, b :: Bool } +>>> | D Int Bool deriving (Generic)+>>> :t genSum (C 3 True)+NSum+ '[ "_C" ':-> NMap '[ "a" ':-> Int, "b" ':-> Bool],+ "_D" ':-> NMap '[ "_1" ':-> Int, "_2" ':-> Bool]]+```
+ named-sop.cabal view
@@ -0,0 +1,49 @@+name: named-sop+version: 0.1.0.0+category: Data++homepage: https://github.com/sjsch/named-sop+synopsis: Dependently-typed sums and products, tagged by field name+description:+ Sums and Maps (products) indexed by a typelevel map of their field+ (or constructor) names and types. They can be combined and split+ again; their typelevel map is sorted to ensure that the end result+ is independent of the order you combine it in.+ .+ "Data.NamedSOP.Generic" contains functions for automatically+ converting between types with a Generic instance and named sums of+ products:+ .+ > >>> data A = C { a :: Int, b :: Bool } + > >>> | D Int Bool deriving (Generic)+ > >>> :t genSum (C 3 True)+ > NSum+ > '[ "_C" ':-> NMap '[ "a" ':-> Int, "b" ':-> Bool],+ > "_D" ':-> NMap '[ "_1" ':-> Int, "_2" ':-> Bool]]++license: MIT+license-file: LICENSE+author: Sam Schweigel+maintainer: Sam Schweigel <s.schweigel@gmail.com>++build-type: Simple+cabal-version: 2.0+tested-with: GHC ==8.6.4++extra-source-files: CHANGELOG.md, README.md++source-repository head+ type: git+ location: https://github.com/sjsch/named-sop++library+ exposed-modules: Data.NamedSOP.Type+ , Data.NamedSOP.Map+ , Data.NamedSOP.Sum+ , Data.NamedSOP.Generic+ build-depends: base ^>= 4.12.0.0+ , singletons ^>= 2.5.1+ , text ^>= 1.2.3.1+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall -Werror=incomplete-patterns
+ src/Data/NamedSOP/Generic.hs view
@@ -0,0 +1,167 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{-|+module : Data.NamedSOP.Generic+description : Convert to/from Generic instances and named sums of products+-}+module Data.NamedSOP.Generic+ ( genProduct+ , specProduct+ , genSum+ , specSum+ , GenProduct(GProduct)+ , GenSum(GSum)+ ) where++import Data.Kind+import Data.Singletons+import Data.Singletons.Prelude.Monoid+import Data.Singletons.Prelude.Num+import Data.Singletons.Prelude.Show+import Data.Singletons.TypeLits+import GHC.Generics++import Data.NamedSOP.Map+import Data.NamedSOP.Sum++class GenProduct (f :: * -> *) where+ type GProduct f :: [Mapping Symbol Type]+ genProduct' :: f a -> NMap (GProduct f)+ specProduct' :: NMap (GProduct f) -> f a++instance GenProduct f => GenProduct (D1 _a f) where+ type GProduct (D1 _a f) = GProduct f+ genProduct' = genProduct' . unM1+ specProduct' = M1 . specProduct'++instance GenProduct f => GenProduct (C1 ('MetaCons _a _b 'True) f) where+ type GProduct (C1 ( 'MetaCons _a _b 'True) f) = GProduct f+ genProduct' = genProduct' . unM1+ specProduct' = M1 . specProduct'++instance GenProduct (S1 ('MetaSel ('Just n) _a _b _c) (Rec0 t)) where+ type GProduct (S1 ( 'MetaSel ( 'Just n) _a _b _c) (Rec0 t)) = '[n ':-> t]+ genProduct' (M1 (K1 c)) = NMapExt c NMapEmpty+ specProduct' (NMapExt c NMapEmpty) = M1 (K1 c)++instance (SingI (GProduct f), SingI (GProduct g),+ GenProduct f, GenProduct g) => GenProduct (f :*: g) where+ type GProduct (f :*: g) = Union (GProduct f) (GProduct g)+ genProduct' (x :*: y) = unionMap (genProduct' x, genProduct' y)+ specProduct' m =+ let (m1, m2) = ununionMap m in specProduct' m1 :*: specProduct' m2++instance GenProductN f => GenProduct (C1 ('MetaCons _a _b 'False) f) where+ type GProduct (C1 ( 'MetaCons _a _b 'False) f) = GProductN 1 f+ genProduct' (M1 x) = genProductN' (SNat @1) x+ specProduct' x = M1 (specProductN' (SNat @1) x)++class GenProductN (f :: * -> *) where+ type GProductN (n :: Nat) f :: [Mapping Symbol Type]+ type GProductS f :: Nat+ sGProductS :: SNat (GProductS f)+ sGProductN :: Sing n -> Sing (GProductN n f)+ genProductN' :: Sing n -> f a -> NMap (GProductN n f)+ specProductN' :: Sing n -> NMap (GProductN n f) -> f a++instance GenProductN (S1 ('MetaSel 'Nothing _a _b _c) (Rec0 t)) where+ type GProductN n (S1 ( 'MetaSel 'Nothing _a _b _c) (Rec0 t)) = '[Mappend "_" (Show_ n) ':-> t]+ type GProductS (S1 ( 'MetaSel 'Nothing _a _b _c) (Rec0 t)) = 1+ sGProductS = SNat+ sGProductN sn = SCons (SMapping (sMappend (SSym @"_") (sShow_ sn))) SNil+ genProductN' _ (M1 (K1 c)) = NMapExt c NMapEmpty+ specProductN' _ (NMapExt c NMapEmpty) = M1 (K1 c)++instance (GenProductN f, GenProductN g) => GenProductN (f :*: g) where+ type GProductN n (f :*: g)+ = Union (GProductN n f) (GProductN (n + GProductS f) g)+ type GProductS (f :*: g) = GProductS f + GProductS g+ sGProductS = sGProductS @f %+ sGProductS @g+ sGProductN sn =+ sUnion (sGProductN @f sn) (sGProductN @g (sn %+ sGProductS @f))+ genProductN' sn (x :*: y) =+ let (m1 , m2 ) = (genProductN' sn x, genProductN' (sn %+ sGProductS @f) y)+ (sm1, sm2) = (sGProductN @f sn, sGProductN @g (sn %+ sGProductS @f))+ in withSingI sm1 $ withSingI sm2 $ unionMap (m1, m2)+ specProductN' (sn :: Sing n) m =+ let (sm1, sm2) = (sGProductN @f sn, sGProductN @g (sn %+ sGProductS @f))+ (x, y) =+ withSingI sm1+ $ withSingI sm2+ $ ununionMap @(GProductN n f) @(GProductN (n + GProductS f) g) m+ in specProductN' sn x :*: specProductN' (sn %+ sGProductS @f) y++class GenSum (f :: * -> *) where+ type GSum f :: [Mapping Symbol Type]+ genSum' :: f a -> NSum (GSum f)+ specSum' :: NSum (GSum f) -> f a++instance GenSum f => GenSum (D1 _a f) where+ type GSum (D1 _a f) = GSum f+ genSum' = genSum' . unM1+ specSum' = M1 . specSum'++instance GenProduct f => GenSum (C1 ('MetaCons n _a 'True) f) where+ type GSum (C1 ( 'MetaCons n _a 'True) f) = '[Mappend "_" n ':-> NMap (GProduct f)]+ genSum' (M1 x) = NSumThis (genProduct' x)+ specSum' (NSumThis x) = M1 (specProduct' x)+ specSum' (NSumThat _) = error "unreachable"++instance GenProductN f => GenSum (C1 ('MetaCons n _a 'False) f) where+ type GSum (C1 ( 'MetaCons n _a 'False) f) = '[Mappend "_" n ':-> NMap (GProductN 1 f)]+ genSum' (M1 x) = NSumThis (genProductN' (SNat @1) x)+ specSum' (NSumThis x) = M1 (specProductN' (SNat @1) x)+ specSum' (NSumThat _) = error "unreachable"++instance ( SingI (GSum f), SingI (GSum g)+ , GenSum f, GenSum g) => GenSum (f :+: g) where+ type GSum (f :+: g) = Union (GSum f) (GSum g)+ genSum' (L1 x) = unionSum @(GSum f) @(GSum g) (Left (genSum' x))+ genSum' (R1 x) = unionSum @(GSum f) @(GSum g) (Right (genSum' x))+ specSum' m = case ununionSum @(GSum f) @(GSum g) m of+ Left x -> L1 (specSum' x)+ Right y -> R1 (specSum' y)++-- | Convert a single-constructor type with a 'Generic' instance into+-- a sorted 'NMap'. Constructors with record selectors will use their+-- names, and constructors without will use numbers, prefixed with @_@+-- for better compatibility with @-XOverloadedLabels@.+--+-- >>> data A = C { a :: Int, b :: Bool } deriving (Generic)+-- >>> genProduct (C { a = 1, b = True })+-- { a :-> 1, b :-> True }+--+-- >>> data B = D Int Bool deriving (Generic)+-- >>> genProduct (D 1 True)+-- { _1 :-> 1, _2 :-> True }+genProduct :: (Generic a, GenProduct (Rep a)) => a -> NMap (GProduct (Rep a))+genProduct = genProduct' . from++-- | Reverse the operation performed by 'genProduct'.+specProduct :: (Generic a, GenProduct (Rep a)) => NMap (GProduct (Rep a)) -> a+specProduct = to . specProduct'++-- | Convert a type with a generic instance with any number of+-- constructors into an 'NSum' of 'NMap's. All constructor names will+-- be prefixed with @_@ to allow for the use of @-XOverloadedLabels@.+--+-- >>> data A = C { a :: Int, b :: Bool } | D Int Bool deriving (Generic)+-- >>> :t genSum (C 3 True)+-- NSum+-- '[ "_C" ':-> NMap '[ "a" ':-> Int, "b" ':-> Bool],+-- "_D" ':-> NMap '[ "_1" ':-> Int, "_2" ':-> Bool]]+genSum :: (Generic a, GenSum (Rep a)) => a -> NSum (GSum (Rep a))+genSum = genSum' . from++-- | Reverse the operation performed by 'genSum'.+specSum :: (Generic a, GenSum (Rep a)) => NSum (GSum (Rep a)) -> a+specSum = to . specSum'
+ src/Data/NamedSOP/Map.hs view
@@ -0,0 +1,128 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++{-|+module : Data.NamedSOP.Map+description : Dependently-typed products/maps+-}+module Data.NamedSOP.Map+ ( NMap(..)+ , unionMap+ , ununionMap+ , module Data.NamedSOP.Type+ ) where++import GHC.TypeLits++import Data.Kind+import Data.Singletons+import Data.Singletons.Prelude.Ord++import Data.NamedSOP.Type++-- | A depedently-typed product, or map. The following are roughly+-- equivalent:+--+-- > type A = NMap '[ "a" ':-> Int, "b" ':-> Bool ]+-- > data A = A { a :: Int, b :: Bool }+data NMap :: [Mapping Symbol Type] -> Type where+ NMapEmpty :: NMap '[]+ NMapExt :: forall k v xs. v -> NMap xs -> NMap ((k ':-> v) : xs)++-- Helper typeclasses for showing a map++class ShowMap xs where+ showMap :: NMap xs -> String++instance ShowMap '[ ] where+ showMap NMapEmpty = ""++instance {-# OVERLAPPABLE #-} (KnownSymbol k, Show v) =>+ ShowMap '[ k ':-> v ] where+ showMap (NMapExt v NMapEmpty) =+ symbolVal (Proxy :: Proxy k) ++ " :-> " ++ show v++instance {-# OVERLAPS #-} (KnownSymbol k, Show v, ShowMap xs) =>+ ShowMap ((k ':-> v) ': xs) where+ showMap (NMapExt v xs) =+ symbolVal (Proxy :: Proxy k) ++ " :-> " ++ show v ++ ", " ++ showMap xs++instance ShowMap xs => Show (NMap xs) where+ show xs = "{ " ++ showMap xs ++ " }"++appendMap :: NMap xs -> NMap ys -> NMap (xs ++ ys)+appendMap NMapEmpty ys = ys+appendMap (NMapExt x xs) ys = NMapExt x (appendMap xs ys)++insertMap ::+ Sing (k ':-> v) -> Sing xs -> v -> NMap xs -> NMap (Insert (k ':-> v) xs)+insertMap _ _ x NMapEmpty = NMapExt x NMapEmpty+insertMap sxk (SCons syk sys) x ys@(NMapExt y ys') =+ case sCompare sxk syk of+ SLT -> NMapExt x ys+ SEQ -> NMapExt x ys+ SGT -> NMapExt y (insertMap sxk sys x ys')++sortMap :: Sing xs -> NMap xs -> NMap (Sort xs)+sortMap _ NMapEmpty = NMapEmpty+sortMap (SCons sx sxs) (NMapExt x xs) =+ insertMap sx (sSort sxs) x (sortMap sxs xs)++-- | Combine two 'NMap's in a way such that the original ordering of+-- their fields doesn't matter; no matter how you combine smaller maps+-- to create a large one, you are guaranteed to have a sorted 'NMap'+-- when you finish.+--+-- 'NMap's form a commutative monoid under 'unionMap', with+-- 'NMapEmpty' as the identity.+--+-- This function takes a tuple as an argument so that it is symmetric+-- with `ununionMap`.+unionMap ::+ forall xs ys. (SingI xs, SingI ys)+ => (NMap xs, NMap ys)+ -> NMap (Union xs ys)+unionMap (xs, ys) = sortMap (sing @xs %++ sing @ys) (appendMap xs ys)++splitMap :: forall xs ys. Sing xs -> Sing ys -> NMap (xs ++ ys) -> (NMap xs, NMap ys)+splitMap SNil SNil NMapEmpty = (NMapEmpty, NMapEmpty)+splitMap SNil _ x = (NMapEmpty, x)+splitMap (SCons _ sxs) sys (NMapExt x xs) =+ let (a, b) = splitMap sxs sys xs+ in (NMapExt x a, b)++uninsertMap :: forall k v xs. Sing (k ':-> v) -> Sing xs -> NMap (Insert (k ':-> v) xs) -> (v, NMap xs)+uninsertMap _ SNil (NMapExt v NMapEmpty) = (v, NMapEmpty)+uninsertMap sx@(SMapping sk) (SCons (SMapping sk') sxs) (NMapExt v vs) = case sCompare sk sk' of+ SLT -> (v, vs)+ SEQ -> (v, vs)+ SGT -> let (v', vs') = uninsertMap sx sxs vs+ in (v', NMapExt v vs')+uninsertMap _ (SCons _ _) NMapEmpty = error "unreachable"++unsortMap :: forall xs. Sing xs -> NMap (Sort xs) -> NMap xs+unsortMap SNil NMapEmpty = NMapEmpty+unsortMap (SCons sx@(SMapping _) sxs) vs =+ let (v', vs') = uninsertMap sx (sSort sxs) vs+ in NMapExt v' (unsortMap sxs vs')++-- | Split a sorted 'NMap' into two arbitrary (and potentially+-- unsorted) submaps. Conveniently select the submaps to split into+-- using @-XTypeApplications@.+--+-- >>> m :: NMap '[ "a" ':-> Int, "b" ':-> Bool, "c" ':-> String ]+-- >>> m = NMapExt 1 (NMapExt True (NMapExt "hello" NMapEmpty))+-- >>> ununionMap @'[ "b" ':-> Bool, "a" ':-> Int ] @'[ "c" ':-> String ] m+-- ({ b :-> True, a :-> 1 },{ c :-> "hello" })+ununionMap :: forall xs ys. (SingI xs, SingI ys) =>+ NMap (Union xs ys) -> (NMap xs, NMap ys)+ununionMap vs = splitMap sxs sys (unsortMap (sxs %++ sys) vs)+ where+ sxs = sing @xs+ sys = sing @ys
+ src/Data/NamedSOP/Sum.hs view
@@ -0,0 +1,136 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++{-|+module : Data.NamedSOP.Sum+description : Dependently-typed sums+-}+module Data.NamedSOP.Sum+ ( NSum(..)+ , unionSum+ , ununionSum+ , module Data.NamedSOP.Type+ ) where++import GHC.TypeLits++import Data.Kind+import Data.Singletons+import Data.Singletons.Prelude.Ord++import Data.NamedSOP.Type++-- | A dependently-typed sum. The following are roughly equilvalent:+--+-- > type A = NSum '[ "B" ':-> Int, "C" ':-> Bool ]+-- > data A = B Int | C Bool+data NSum :: [Mapping Symbol Type] -> Type where+ NSumThis :: v -> NSum ((k ':-> v) ': xs)+ NSumThat :: forall x xs. NSum xs -> NSum (x ': xs)++instance {-# OVERLAPPABLE #-} Show (NSum '[]) where+ show _ = error "unreachable"++instance {-# OVERLAPS #-} (KnownSymbol k, Show v, Show (NSum xs)) =>+ Show (NSum ((k ':-> v) ': xs)) where+ show (NSumThis v) = symbolVal (Proxy :: Proxy k) ++ " :-> " ++ show v+ show (NSumThat vs) = show vs++appendSum :: Sing xs -> Sing ys -> Either (NSum xs) (NSum ys) -> NSum (xs ++ ys)+appendSum _ _ (Left (NSumThis x)) = NSumThis x+appendSum (SCons _ sxs) sys (Left (NSumThat xs)) = NSumThat (appendSum sxs sys (Left xs))+appendSum SNil _ (Right ys) = ys+appendSum (SCons (_ :: Sing x) sxs) sys (Right ys) = NSumThat @x (appendSum sxs sys (Right ys))++insertSum :: Sing (k ':-> v) -> Sing xs -> Either v (NSum xs) -> NSum (Insert (k ':-> v) xs)+insertSum _ SNil (Left v) = NSumThis v+insertSum sxk (SCons syk sys) (Left v) =+ case sCompare sxk syk of+ SLT -> NSumThis v+ SEQ -> NSumThis v+ SGT -> NSumThat (insertSum sxk sys (Left v))+insertSum sxk (SCons syk sys) (Right v) = case sCompare sxk syk of+ SLT -> NSumThat v+ SEQ -> NSumThat v+ SGT -> case v of+ NSumThis v' -> NSumThis v'+ NSumThat v' -> NSumThat (insertSum sxk sys (Right v'))+insertSum _ SNil (Right _) = error "unreachable"++sortSum :: Sing xs -> NSum xs -> NSum (Sort xs)+sortSum SNil _ = error "unreachable"+sortSum (SCons sx sxs) (NSumThis v) = insertSum sx (sSort sxs) (Left v)+sortSum (SCons sx@(SMapping _) sxs) (NSumThat vs) =+ insertSum sx (sSort sxs) (Right (sortSum sxs vs))++-- | Combine two 'NSum's. This is dual to+-- 'Data.NamedSOP.Map.unionMap', which accepts a product of products+-- and returns a product; 'unionSum' accepts a sum of sums and returns+-- a sum. The order of fields does not matter, because they will be+-- sorted.+--+-- 'NSum's form a commutative monoid under 'unionSum', with @NSum '[]@+-- as the identity.+--+-- Together with 'Data.NamedSOP.Map.NMap',+-- 'Data.NamedSOP.Map.NMapEmpty', and 'Data.NamedSOP.Map.unionMap', it+-- is a semiring.+unionSum ::+ forall xs ys. (SingI xs, SingI ys)+ => Either (NSum xs) (NSum ys)+ -> NSum (Union xs ys)+unionSum xs = sortSum (sing @xs %++ sing @ys) (appendSum (sing @xs) (sing @ys) xs)++splitSum :: forall xs ys. Sing xs -> Sing ys+ -> NSum (xs ++ ys) -> Either (NSum xs) (NSum ys)+splitSum SNil SNil _ = error "unreachable"+splitSum SNil _ s = Right s+splitSum (SCons _ _) _ (NSumThis v) = Left (NSumThis v)+splitSum (SCons _ sxs) sys (NSumThat v) =+ case splitSum sxs sys v of+ Left x -> Left (NSumThat x)+ Right x -> Right x++uninsertSum :: forall k v xs. Sing (k ':-> v) -> Sing xs+ -> NSum (Insert (k ':-> v) xs) -> Either v (NSum xs)+uninsertSum _ SNil (NSumThis v) = Left v+uninsertSum _ SNil (NSumThat v) = Right v+uninsertSum sxk (SCons syk _) (NSumThis v) = case sCompare sxk syk of+ SLT -> Left v+ SEQ -> Left v+ SGT -> error "unsorted list"+uninsertSum sxk (SCons syk sys) (NSumThat vs) = case sCompare sxk syk of+ SLT -> Right vs+ SEQ -> Right vs+ SGT -> case uninsertSum sxk sys vs of+ Left x -> Left x+ Right x -> Right (NSumThat x)++unsortSum :: forall xs. Sing xs -> NSum (Sort xs) -> NSum xs+unsortSum SNil _ = error "unreachable"+unsortSum (SCons sx@(SMapping _) sxs) v =+ case uninsertSum sx (sSort sxs) v of+ Left x -> NSumThis x+ Right x -> NSumThat (unsortSum sxs x)++-- | Split a sorted 'NSum' into either of two (potentially unsorted)+-- subsums. Select the subsums with @-XTypeApplications@.+--+-- >>> s :: NSum '[ "A" ':-> Int, "B" ':-> Bool, "C" ':-> String ]+-- >>> s = NSumThat (NSumThis True) -- Select the "B" field.+-- >>> ununionSum @'[ "B" ':-> Bool, "A" ':-> Int ] @'[ "C" ':-> String ] s+-- Left (B :-> True)+ununionSum :: forall xs ys. (SingI xs, SingI ys) =>+ NSum (Union xs ys) -> Either (NSum xs) (NSum ys)+ununionSum vs = splitSum sxs sys (unsortSum (sxs %++ sys) vs)+ where+ sxs = sing @xs+ sys = sing @ys
+ src/Data/NamedSOP/Type.hs view
@@ -0,0 +1,109 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{-|+module : Data.NamedSOP.Type+description : Symbol-type mappings, convenience re-exports++End users should not have to manually import this module, since it is+re-exported by "Data.NamedSOP.Map" and "Data.NamedSOP.Sum".++In addition to 'Mapping' and its related singletons, various type+families related to lists are redefined here, since the ones in+"Data.Singletons.Prelude.List" use local definitions. [As of+2019-07](https://github.com/goldfirere/singletons/issues/339), it is+not possible to prove around local definitions that are promoted with+'singletons', so we are stuck redefining them.+-}+module Data.NamedSOP.Type+ ( -- * Symbol-value mappings+ Mapping(..)+ , SMapping+ -- * List operation singletons+ -- | Unlike the usual definition, this 'union' does /not/ remove+ -- duplicates, since that would make it impossible to define a+ -- union operation for sums.+ , Union+ , sUnion+ , union+ , type (++)+ , (%++)+ , Insert+ , sInsert+ , insert+ , Sort+ , sSort+ , sort+ -- * Convenience re-exports+ , SingI+ , Sing(SNil, SCons, SMapping)+ ) where++import Data.Kind+import Data.Singletons+import Data.Singletons.Prelude.List (Sing (SCons, SNil))+import Data.Singletons.TH++singletons [d|+ (++) :: [a] -> [a] -> [a]+ [] ++ ys = ys+ (x:xs) ++ ys = x : (xs ++ ys)++ insert :: Ord a => a -> [a] -> [a]+ insert x [] = [x]+ insert x (y:ys) = case compare x y of+ LT -> x : y : ys+ EQ -> x : y : ys+ GT -> y : insert x ys++ sort :: Ord a => [a] -> [a]+ sort [] = []+ sort (x:xs) = insert x (sort xs)++ union :: Ord a => [a] -> [a] -> [a]+ union xs ys = sort (xs ++ ys)+ |]++-- | A type @v@ with an associated tag @k@. Importantly, its+-- singleton data instance only takes a singleton for the tag @k@ as+-- its argmuent, and not one for the value @v@.+infixr 4 :->++data Mapping k v =+ k :-> v+ deriving (Show)++instance Eq a => Eq (Mapping a b) where+ (x :-> _) == (y :-> _) = x == y++instance Ord a => Ord (Mapping a b) where+ compare (x :-> _) (y :-> _) = compare x y++type SMapping = (Sing :: Mapping k v -> Type)++data instance Sing (a :: Mapping k v) where+ SMapping :: Sing k -> Sing (k ':-> v)++instance SingI k => SingI (k ':-> v) where+ sing = SMapping sing++-- | Equality and ordering on mappings uses only the key.+instance PEq (Mapping k v) where+ type (k1 ':-> _) == (k2 ':-> _) = k1 == k2++instance SEq k => SEq (Mapping k v) where+ (SMapping k1) %== (SMapping k2) = k1 %== k2++instance POrd k => POrd (Mapping k v) where+ type Compare (k1 ':-> _) (k2 ':-> _) = Compare k1 k2++instance SOrd k => SOrd (Mapping k v) where+ sCompare (SMapping k1) (SMapping k2) = sCompare k1 k2