diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,4 @@ +# 0.1.0.0 + +Initial release. Expect the public-facing API to change as the +library is reworked. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,22 @@ +# named-sop: Dependently-typed sums and products, tagged by field name + +[![Hackage](https://img.shields.io/hackage/v/named-sop.svg)](https://hackage.haskell.org/package/named-sop) +[![Build Status](https://secure.travis-ci.org/sjsch/named-sop.svg)](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]] +``` diff --git a/named-sop.cabal b/named-sop.cabal new file mode 100644 --- /dev/null +++ b/named-sop.cabal @@ -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 + +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 diff --git a/src/Data/NamedSOP/Generic.hs b/src/Data/NamedSOP/Generic.hs new file mode 100644 --- /dev/null +++ b/src/Data/NamedSOP/Generic.hs @@ -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' diff --git a/src/Data/NamedSOP/Map.hs b/src/Data/NamedSOP/Map.hs new file mode 100644 --- /dev/null +++ b/src/Data/NamedSOP/Map.hs @@ -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 diff --git a/src/Data/NamedSOP/Sum.hs b/src/Data/NamedSOP/Sum.hs new file mode 100644 --- /dev/null +++ b/src/Data/NamedSOP/Sum.hs @@ -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 diff --git a/src/Data/NamedSOP/Type.hs b/src/Data/NamedSOP/Type.hs new file mode 100644 --- /dev/null +++ b/src/Data/NamedSOP/Type.hs @@ -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