diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,51 +1,62 @@ -# Revision history for red-black-record - -## 2.1.0.0 - -- Made the type-level map poly-kinded in the values, as there wasn't a real - reason to force them to the Type kind. -- Removed deprecated EmptyMap (use Empty instead). - -## 2.0.4.0 - -- Compatibility with sop-core 0.5.0.0. -- Contravariant intance for Case newtype. - -## 2.0.3.0 - -- Issue #7: FromVariant & ToVariant instances for sum types with branches with - no arguments. - -## 2.0.2.2 - -- Improved compilation times for type-level deletion. - -## 2.0.0.0 - -- BREAKING CHANGES - - The constructors for the type-level map are now hidden. - - The name of the type-level map has changed from RBT to Map, to - de-emphasize implementation details. - -- Added the "Deletable" typeclass with de "delete" and "winnow" methods. - -- Solved bugs with coloring/balancing, added new tests. - -- Data.RBR.Internal is still exported, but it doesn't appear in the Haddocks. - It appears that Haddock doesn't play well with reexported-modules sections in - Cabal. - -## 1.1.0.0 - -- Field and Branch type families to help speed up type-level computations. - - Apparently, having identical invocations of a "costly to compute" type family - in a signature slowed things down. - -## 1.0.0.2 - -- Improved compilation times for getters by refactoring `KeyHelper`. - -## 1.0.0.0 - -- First version. Released on an unsuspecting world. +# Revision history for red-black-record + +## 2.1.1.0 +- Added NP-like functions for working on Records, like sequence_Record. + They are memebers of the Maplike typeclass. +- Deprecated the -Subset functions from Data.RBR and created a new module + Data.RBR.Subset with new versions. To avoid collisions, Data.RBR.Subset + should be imported qualified. +- Deprecated a number of other functions that had Productlike / Sumlike + constraints, added new functions with Maplike constraints. +- Added IsRecordType, IsVariantType. +- Added KeyValueConstraints, ValueConstraint. + +## 2.1.0.0 + +- Made the type-level map poly-kinded in the values, as there wasn't a real + reason to force them to the Type kind. +- Removed deprecated EmptyMap (use Empty instead). + +## 2.0.4.0 + +- Compatibility with sop-core 0.5.0.0. +- Contravariant intance for Case newtype. + +## 2.0.3.0 + +- Issue #7: FromVariant & ToVariant instances for sum types with branches with + no arguments. + +## 2.0.2.2 + +- Improved compilation times for type-level deletion. + +## 2.0.0.0 + +- BREAKING CHANGES + - The constructors for the type-level map are now hidden. + - The name of the type-level map has changed from RBT to Map, to + de-emphasize implementation details. + +- Added the "Deletable" typeclass with de "delete" and "winnow" methods. + +- Solved bugs with coloring/balancing, added new tests. + +- Data.RBR.Internal is still exported, but it doesn't appear in the Haddocks. + It appears that Haddock doesn't play well with reexported-modules sections in + Cabal. + +## 1.1.0.0 + +- Field and Branch type families to help speed up type-level computations. + + Apparently, having identical invocations of a "costly to compute" type family + in a signature slowed things down. + +## 1.0.0.2 + +- Improved compilation times for getters by refactoring `KeyHelper`. + +## 1.0.0.0 + +- First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,30 +1,30 @@ -Copyright (c) 2018, Daniel Diaz - -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 Daniel Diaz 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. +Copyright (c) 2018, Daniel Diaz + +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 Daniel Diaz 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. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -21,10 +21,9 @@ and variants are isomorphic to [n-ary unlabeled sums](http://hackage.haskell.org/package/sop-core-0.4.0.0/docs/Data-SOP.html#t:NS). The [sop-core](http://hackage.haskell.org/package/sop-core) library provides -such unlabeled types, along with a rich API for manipulating them. Instead of -reinventing the wheel, red-black-record defines conversion functions to -facilitate working in the "unlabeled" world and then coming back to records and -variants. +such unlabeled types, along with a rich API for manipulating them. +red-black-record defines conversion functions to facilitate working in the +"unlabeled" world, if needed, and then coming back to records and variants. There is another world towards which bridges must be built: the everyday Haskell world of conventional records and sums. In fact, one of the motivations diff --git a/lib-demoted/Data/RBR/Demoted.hs b/lib-demoted/Data/RBR/Demoted.hs --- a/lib-demoted/Data/RBR/Demoted.hs +++ b/lib-demoted/Data/RBR/Demoted.hs @@ -1,215 +1,215 @@ -{-# LANGUAGE DataKinds, - TypeOperators, - ConstraintKinds, - PolyKinds, - TypeFamilies, - GADTs, - MultiParamTypeClasses, - FunctionalDependencies, - FlexibleInstances, - FlexibleContexts, - UndecidableInstances, - UndecidableSuperClasses, - TypeApplications, - ScopedTypeVariables, - AllowAmbiguousTypes, - ExplicitForAll, - RankNTypes, - DefaultSignatures, - PartialTypeSignatures, - LambdaCase, - EmptyCase -#-} -{-# OPTIONS_GHC -Wno-partial-type-signatures #-} - -module Data.RBR.Demoted where - -import Data.RBR.Internal - -import Data.Proxy -import Data.Kind -import Data.Typeable -import GHC.TypeLits - -emptyMap :: Map String TypeRep -emptyMap = E - -class DemotableColor (c :: Color) where - demoteColor :: Proxy c -> Color - -instance DemotableColor R where - demoteColor _ = R - -instance DemotableColor B where - demoteColor _ = B - -class DemotableMap (t :: Map Symbol Type) where - demoteMap :: Proxy t -> Map String TypeRep - -instance DemotableMap E where - demoteMap _ = E - -instance (DemotableColor c, - KnownSymbol s, - Typeable ty, - DemotableMap l, - DemotableMap r) - => DemotableMap (N c l s ty r) where - demoteMap _ = N (demoteColor (Proxy @c)) - (demoteMap (Proxy @l)) - (symbolVal (Proxy @s)) - (typeRep (Proxy @ty)) - (demoteMap (Proxy @r)) - -t_insert :: Ord a => a -> v -> Map a v -> Map a v -t_insert x val s = - N B a v z b - where - N _ a v z b = ins s - ins E = N R E x val E - ins s@(N B a y val' b) - | xy = t_balance a y val' (ins b) - | otherwise = s - ins s@(N R a y val' b) - | xy = N R a y val' (ins b) - | otherwise = s - -t_balance :: Map a v -> a -> v -> Map a v -> Map a v -t_balance (N R a x xv b) y yv (N R c z zv d) = N R (N B a x xv b) y yv (N B c z zv d) -t_balance (N R (N R a x xv b) y yv c) z zv d = N R (N B a x xv b) y yv (N B c z zv d) -t_balance (N R a x xv (N R b y yv c)) z zv d = N R (N B a x xv b) y yv (N B c z zv d) -t_balance a x xv (N R b y yv (N R c z zv d)) = N R (N B a x xv b) y yv (N B c z zv d) -t_balance a x xv (N R (N R b y yv c) z zv d) = N R (N B a x xv b) y yv (N B c z zv d) -t_balance a x xv b = N B a x xv b - - -t_delete :: Ord a => a -> Map a v -> Map a v -t_delete x t = - case del t of {N _ a y yv b -> N B a y yv b; _ -> E} - where - del E = E - del (N _ a y yv b) - | xy = delformRight a y yv b - | otherwise = t_app a b - delformLeft a@(N B _ _ _ _) y yv b = t_balleft (del a) y yv b - delformLeft a y yv b = N R (del a) y yv b - - delformRight a y yv b@(N B _ _ _ _) = t_balright a y yv (del b) - delformRight a y yv b = N R a y yv (del b) - -t_balleft :: Map a v -> a -> v -> Map a v -> Map a v -t_balleft (N R a x xv b) y yv c = N R (N B a x xv b) y yv c -t_balleft bl x xv (N B a y yv b) = t_balance bl x xv (N R a y yv b) -t_balleft bl x xv (N R (N B a y yv b) z zv c) = N R (N B bl x xv a) y yv (t_balance b z zv (t_sub1 c)) - -t_balright :: Map a v -> a -> v -> Map a v -> Map a v -t_balright a x xv (N R b y yv c) = N R a x xv (N B b y yv c) -t_balright (N B a x xv b) y yv bl = t_balance (N R a x xv b) y yv bl -t_balright (N R a x xv (N B b y yv c)) z zv bl = N R (t_balance (t_sub1 a) x xv b) y yv (N B c z zv bl) - -t_sub1 :: Map a v -> Map a v -t_sub1 (N B a x xv b) = N R a x xv b -t_sub1 _ = error "invariance violation" - -t_app :: Map a v -> Map a v -> Map a v -t_app E x = x -t_app x E = x -t_app (N R a x xv b) (N R c y yv d) = - case t_app b c of - N R b' z zv c' -> N R (N R a x xv b') z zv (N R c' y yv d) - bc -> N R a x xv (N R bc y yv d) -t_app (N B a x xv b) (N B c y yv d) = - case t_app b c of - N R b' z zv c' -> N R (N B a x xv b') z zv (N B c' y yv d) - bc -> t_balleft a x xv (N B bc y yv d) -t_app a (N R b x xv c) = N R (t_app a b) x xv c -t_app (N R a x xv b) c = N R a x xv (t_app b c) - --- The original term-level code, taken from: --- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html --- --- {- Version 1, 'untyped' -} --- data Color = R | B deriving Show --- data RB a = E | T Color (RB a) a (RB a) deriving Show --- --- {- Insertion and membership test as by Okasaki -} --- insert :: Ord a => a -> RB a -> RB a --- insert x s = --- T B a z b --- where --- T _ a z b = ins s --- ins E = T R E x E --- ins s@(T B a y b) --- | xy = balance a y (ins b) --- | otherwise = s --- ins s@(T R a y b) --- | xy = T R a y (ins b) --- | otherwise = s --- --- --- {- balance: first equation is new, --- to make it work with a weaker invariant -} --- balance :: RB a -> a -> RB a -> RB a --- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d) --- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) --- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) --- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) --- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) --- balance a x b = T B a x b --- --- member :: Ord a => a -> RB a -> Bool --- member x E = False --- member x (T _ a y b) --- | xy = member x b --- | otherwise = True --- --- {- deletion a la SMK -} --- delete :: Ord a => a -> RB a -> RB a --- delete x t = --- case del t of {T _ a y b -> T B a y b; _ -> E} --- where --- del E = E --- del (T _ a y b) --- | xy = delformRight a y b --- | otherwise = app a b --- delformLeft a@(T B _ _ _) y b = balleft (del a) y b --- delformLeft a y b = T R (del a) y b --- --- delformRight a y b@(T B _ _ _) = balright a y (del b) --- delformRight a y b = T R a y (del b) --- --- balleft :: RB a -> a -> RB a -> RB a --- balleft (T R a x b) y c = T R (T B a x b) y c --- balleft bl x (T B a y b) = balance bl x (T R a y b) --- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c)) --- --- balright :: RB a -> a -> RB a -> RB a --- balright a x (T R b y c) = T R a x (T B b y c) --- balright (T B a x b) y bl = balance (T R a x b) y bl --- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) --- --- sub1 :: RB a -> RB a --- sub1 (T B a x b) = T R a x b --- sub1 _ = error "invariance violation" --- --- app :: RB a -> RB a -> RB a --- app E x = x --- app x E = x --- app (T R a x b) (T R c y d) = --- case app b c of --- T R b' z c' -> T R(T R a x b') z (T R c' y d) --- bc -> T R a x (T R bc y d) --- app (T B a x b) (T B c y d) = --- case app b c of --- T R b' z c' -> T R(T B a x b') z (T B c' y d) --- bc -> balleft a x (T B bc y d) --- app a (T R b x c) = T R (app a b) x c --- app (T R a x b) c = T R a x (app b c) - +{-# LANGUAGE DataKinds, + TypeOperators, + ConstraintKinds, + PolyKinds, + TypeFamilies, + GADTs, + MultiParamTypeClasses, + FunctionalDependencies, + FlexibleInstances, + FlexibleContexts, + UndecidableInstances, + UndecidableSuperClasses, + TypeApplications, + ScopedTypeVariables, + AllowAmbiguousTypes, + ExplicitForAll, + RankNTypes, + DefaultSignatures, + PartialTypeSignatures, + LambdaCase, + EmptyCase +#-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} + +module Data.RBR.Demoted where + +import Data.RBR.Internal + +import Data.Proxy +import Data.Kind +import Data.Typeable +import GHC.TypeLits + +emptyMap :: Map String TypeRep +emptyMap = E + +class DemotableColor (c :: Color) where + demoteColor :: Proxy c -> Color + +instance DemotableColor R where + demoteColor _ = R + +instance DemotableColor B where + demoteColor _ = B + +class DemotableMap (t :: Map Symbol Type) where + demoteMap :: Proxy t -> Map String TypeRep + +instance DemotableMap E where + demoteMap _ = E + +instance (DemotableColor c, + KnownSymbol s, + Typeable ty, + DemotableMap l, + DemotableMap r) + => DemotableMap (N c l s ty r) where + demoteMap _ = N (demoteColor (Proxy @c)) + (demoteMap (Proxy @l)) + (symbolVal (Proxy @s)) + (typeRep (Proxy @ty)) + (demoteMap (Proxy @r)) + +t_insert :: Ord a => a -> v -> Map a v -> Map a v +t_insert x val s = + N B a v z b + where + N _ a v z b = ins s + ins E = N R E x val E + ins s@(N B a y val' b) + | xy = t_balance a y val' (ins b) + | otherwise = s + ins s@(N R a y val' b) + | xy = N R a y val' (ins b) + | otherwise = s + +t_balance :: Map a v -> a -> v -> Map a v -> Map a v +t_balance (N R a x xv b) y yv (N R c z zv d) = N R (N B a x xv b) y yv (N B c z zv d) +t_balance (N R (N R a x xv b) y yv c) z zv d = N R (N B a x xv b) y yv (N B c z zv d) +t_balance (N R a x xv (N R b y yv c)) z zv d = N R (N B a x xv b) y yv (N B c z zv d) +t_balance a x xv (N R b y yv (N R c z zv d)) = N R (N B a x xv b) y yv (N B c z zv d) +t_balance a x xv (N R (N R b y yv c) z zv d) = N R (N B a x xv b) y yv (N B c z zv d) +t_balance a x xv b = N B a x xv b + + +t_delete :: Ord a => a -> Map a v -> Map a v +t_delete x t = + case del t of {N _ a y yv b -> N B a y yv b; _ -> E} + where + del E = E + del (N _ a y yv b) + | xy = delformRight a y yv b + | otherwise = t_app a b + delformLeft a@(N B _ _ _ _) y yv b = t_balleft (del a) y yv b + delformLeft a y yv b = N R (del a) y yv b + + delformRight a y yv b@(N B _ _ _ _) = t_balright a y yv (del b) + delformRight a y yv b = N R a y yv (del b) + +t_balleft :: Map a v -> a -> v -> Map a v -> Map a v +t_balleft (N R a x xv b) y yv c = N R (N B a x xv b) y yv c +t_balleft bl x xv (N B a y yv b) = t_balance bl x xv (N R a y yv b) +t_balleft bl x xv (N R (N B a y yv b) z zv c) = N R (N B bl x xv a) y yv (t_balance b z zv (t_sub1 c)) + +t_balright :: Map a v -> a -> v -> Map a v -> Map a v +t_balright a x xv (N R b y yv c) = N R a x xv (N B b y yv c) +t_balright (N B a x xv b) y yv bl = t_balance (N R a x xv b) y yv bl +t_balright (N R a x xv (N B b y yv c)) z zv bl = N R (t_balance (t_sub1 a) x xv b) y yv (N B c z zv bl) + +t_sub1 :: Map a v -> Map a v +t_sub1 (N B a x xv b) = N R a x xv b +t_sub1 _ = error "invariance violation" + +t_app :: Map a v -> Map a v -> Map a v +t_app E x = x +t_app x E = x +t_app (N R a x xv b) (N R c y yv d) = + case t_app b c of + N R b' z zv c' -> N R (N R a x xv b') z zv (N R c' y yv d) + bc -> N R a x xv (N R bc y yv d) +t_app (N B a x xv b) (N B c y yv d) = + case t_app b c of + N R b' z zv c' -> N R (N B a x xv b') z zv (N B c' y yv d) + bc -> t_balleft a x xv (N B bc y yv d) +t_app a (N R b x xv c) = N R (t_app a b) x xv c +t_app (N R a x xv b) c = N R a x xv (t_app b c) + +-- The original term-level code, taken from: +-- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html +-- +-- {- Version 1, 'untyped' -} +-- data Color = R | B deriving Show +-- data RB a = E | T Color (RB a) a (RB a) deriving Show +-- +-- {- Insertion and membership test as by Okasaki -} +-- insert :: Ord a => a -> RB a -> RB a +-- insert x s = +-- T B a z b +-- where +-- T _ a z b = ins s +-- ins E = T R E x E +-- ins s@(T B a y b) +-- | xy = balance a y (ins b) +-- | otherwise = s +-- ins s@(T R a y b) +-- | xy = T R a y (ins b) +-- | otherwise = s +-- +-- +-- {- balance: first equation is new, +-- to make it work with a weaker invariant -} +-- balance :: RB a -> a -> RB a -> RB a +-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d) +-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) +-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) +-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) +-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) +-- balance a x b = T B a x b +-- +-- member :: Ord a => a -> RB a -> Bool +-- member x E = False +-- member x (T _ a y b) +-- | xy = member x b +-- | otherwise = True +-- +-- {- deletion a la SMK -} +-- delete :: Ord a => a -> RB a -> RB a +-- delete x t = +-- case del t of {T _ a y b -> T B a y b; _ -> E} +-- where +-- del E = E +-- del (T _ a y b) +-- | xy = delformRight a y b +-- | otherwise = app a b +-- delformLeft a@(T B _ _ _) y b = balleft (del a) y b +-- delformLeft a y b = T R (del a) y b +-- +-- delformRight a y b@(T B _ _ _) = balright a y (del b) +-- delformRight a y b = T R a y (del b) +-- +-- balleft :: RB a -> a -> RB a -> RB a +-- balleft (T R a x b) y c = T R (T B a x b) y c +-- balleft bl x (T B a y b) = balance bl x (T R a y b) +-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c)) +-- +-- balright :: RB a -> a -> RB a -> RB a +-- balright a x (T R b y c) = T R a x (T B b y c) +-- balright (T B a x b) y bl = balance (T R a x b) y bl +-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) +-- +-- sub1 :: RB a -> RB a +-- sub1 (T B a x b) = T R a x b +-- sub1 _ = error "invariance violation" +-- +-- app :: RB a -> RB a -> RB a +-- app E x = x +-- app x E = x +-- app (T R a x b) (T R c y d) = +-- case app b c of +-- T R b' z c' -> T R(T R a x b') z (T R c' y d) +-- bc -> T R a x (T R bc y d) +-- app (T B a x b) (T B c y d) = +-- case app b c of +-- T R b' z c' -> T R(T B a x b') z (T B c' y d) +-- bc -> balleft a x (T B bc y d) +-- app a (T R b x c) = T R (app a b) x c +-- app (T R a x b) c = T R a x (app b c) + diff --git a/lib/Data/RBR.hs b/lib/Data/RBR.hs --- a/lib/Data/RBR.hs +++ b/lib/Data/RBR.hs @@ -1,158 +1,172 @@ -{-| - This module provides extensible 'Record' and 'Variant' types, which are - indexed by a type-level 'Map'. - - Many functions in this module require the use of @TypeApplications@ to - avoid ambiguity. The order of the applications is the order of the type - variables in the function signature's @forall@. The first type variable is - usually the field/branch name and it's always required. The other type - variables can often be inferred. - - Meaning of commonly used type and kind variables: - - - @t@: A type-level 'Map', usually of kind @Map Symbol q@. - - @k@: A key of kind 'Symbol' in a type-level 'Map'. - - @v@: A type value of kind @q@ in a type-level 'Map'. - - @q@: The kind of the type value @v@. - - @f@: A type constructor of kind @q -> Type@ that wraps the type @v@. - - @flat@: A type-level list of kind @[q]@ whose elements correspond to values in a type-level 'Map'. - --} -module Data.RBR ( - -- * Type-level map - -- $typelevel - Map, - Empty, - KeysValuesAll(), - KnownKey(), - demoteKeys, - KnownKeyTypeableValue(), - demoteEntries, - -- * Records and Variants - Record, - unit, - cpure_Record, - collapse_Record, - prettyShowRecord, - prettyShowRecordI, - Variant, - impossible, - prettyShowVariant, - prettyShowVariantI, - -- ** Inserting and widening - Insertable (Insert), - InsertAll, - FromList, - insert, - addField, - insertI, - addFieldI, - widen, - -- ** Deleting and winnowing - Deletable (Delete), - delete, - winnow, - winnowI, - -- ** Projecting and injecting - Key (Value), - Field, - field, - Branch, - branch, - project, - projectI, - getField, - getFieldI, - setField, - setFieldI, - modifyField, - modifyFieldI, - inject, - injectI, - match, - matchI, - -- ** Eliminating variants - eliminate, - Case (..), - addCase, - addCaseI, - -- ** Subsets of fields and branches - PresentIn, - ProductlikeSubset, - fieldSubset, - projectSubset, - getFieldSubset, - setFieldSubset, - modifyFieldSubset, - SumlikeSubset, - branchSubset, - injectSubset, - matchSubset, - eliminateSubset, - -- * Interfacing with normal records - -- $nominal - ToRecord (..), - FromRecord (..), - VariantCode, - ToVariant (..), - FromVariant(..), - -- * Interfacing with Data.SOP - Productlike (..), - prefixNP, - breakNP, - toNP, - fromNP, - Sumlike (..), - prefixNS, - breakNS, - toNS, - fromNS, - -- * Data.SOP re-exports - I(..), - K(..), - NP(..), - NS(..), - ) where - -import Data.RBR.Internal -import Data.SOP (I(..),K(..),NP(..),NS(..)) - -{- $setup - ->>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric ->>> :set -Wno-partial-type-signatures ->>> import Data.RBR ->>> import Data.SOP ->>> import GHC.Generics - --} - -{- $typelevel - - A type-level map that keeps track of which keys are present, and to which - types they correspond. - - Implemented as a red-black tree, and used as a kind by means of @DataKinds@. --} - -{- $nominal - - Typeclasses for converting to and from normal Haskell records and sum types. - - They have default implementations based in "GHC.Generics": - ->>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) ->>> instance ToRecord Person ->>> instance FromRecord Person - ->>> data Summy = Lefty Int | Righty Bool deriving (Generic,Show) ->>> instance ToVariant Summy ->>> instance FromVariant Summy - - Only single-constructor records with named fields can have 'ToRecord' and - 'FromRecord' instances. - - Only sum types with exactly one anonymous argument on each branch can have - 'ToVariant' and 'FromVariant' instances. - --} +{-| + This module provides extensible 'Record' and 'Variant' types, which are + indexed by a type-level 'Map'. + + Many functions in this module require the use of @TypeApplications@ to + avoid ambiguity. The order of the applications is the order of the type + variables in the function signature's @forall@. The first type variable is + usually the field/branch name and it's always required. The other type + variables can often be inferred. + + Meaning of commonly used type and kind variables: + + - @t@: A type-level 'Map', usually of kind @Map Symbol q@. + - @k@: A key of kind 'Symbol' in a type-level 'Map'. + - @v@: A type value of kind @q@ in a type-level 'Map'. + - @q@: The kind of the type value @v@. + - @f@: A type constructor of kind @q -> Type@ that wraps the type @v@. + - @flat@: A type-level list of kind @[q]@ whose elements correspond to values in a type-level 'Map'. + +-} +module Data.RBR ( + -- * Type-level map + -- $typelevel + Map, + Empty, + KeysValuesAll(), + KnownKey(), + demoteKeys, + KnownKeyTypeableValue(), + demoteEntries, + KeyValueConstraints(), + ValueConstraint(), + PresentIn(), + -- * Records and Variants + Record, + unit, + Variant, + impossible, + -- ** Inserting and widening + Insertable (Insert), + InsertAll, + FromList, + insert, + addField, + insertI, + addFieldI, + widen, + -- ** Deleting and winnowing + Deletable (Delete), + delete, + winnow, + winnowI, + -- ** Projecting and injecting + Key (Value), + Field, + field, + Branch, + branch, + project, + projectI, + getField, + getFieldI, + setField, + setFieldI, + modifyField, + modifyFieldI, + inject, + injectI, + match, + matchI, + -- ** Transformations + Maplike(..), + cpure_Record, + cpure'_Record, + VariantInjection(..), + prettyShow_Record, + prettyShow_RecordI, + prettyShow_Variant, + prettyShow_VariantI, + -- ** Eliminating variants + eliminate_Variant, + Case (..), + addCase, + addCaseI, + -- * Interfacing with normal records + -- $nominal + ToRecord (..), + FromRecord (..), + IsRecordType, + VariantCode, + ToVariant (..), + FromVariant(..), + IsVariantType, + -- * Interfacing with Data.SOP + Productlike (..), + prefixNP, + breakNP, + toNP, + fromNP, + Sumlike (..), + prefixNS, + breakNS, + toNS, + fromNS, + -- * Data.SOP re-exports + I(..), + K(..), + NP(..), + NS(..), + (:.:)(..), + -- * Deprecated + collapse_Record, + eliminate, + prettyShowRecord, + prettyShowRecordI, + prettyShowVariant, + prettyShowVariantI, + ProductlikeSubset, + fieldSubset, + projectSubset, + getFieldSubset, + setFieldSubset, + modifyFieldSubset, + SumlikeSubset, + branchSubset, + injectSubset, + matchSubset, + eliminateSubset + ) where + +import Data.RBR.Internal +import Data.SOP (I(..),K(..),NP(..),NS(..),(:.:)(..),Top) + +{- $setup + +>>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric +>>> :set -Wno-partial-type-signatures +>>> import Data.RBR +>>> import Data.SOP +>>> import GHC.Generics + +-} + +{- $typelevel + + A type-level map that keeps track of which keys are present, and to which + types they correspond. + + Implemented as a red-black tree, and used as a kind by means of @DataKinds@. +-} + +{- $nominal + + Typeclasses for converting to and from normal Haskell records and sum types. + + They have default implementations based in "GHC.Generics": + +>>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) +>>> instance ToRecord Person +>>> instance FromRecord Person + +>>> data Summy = Lefty Int | Righty Bool deriving (Generic,Show) +>>> instance ToVariant Summy +>>> instance FromVariant Summy + + Only single-constructor records with named fields can have 'ToRecord' and + 'FromRecord' instances. + + Only sum types with exactly one anonymous argument on each branch can have + 'ToVariant' and 'FromVariant' instances. + +-} diff --git a/lib/Data/RBR/Examples.hs b/lib/Data/RBR/Examples.hs --- a/lib/Data/RBR/Examples.hs +++ b/lib/Data/RBR/Examples.hs @@ -1,349 +1,346 @@ -module Data.RBR.Examples ( - -- * Setup code - -- $setup - - -- * Constructing a record and viewing its fields. - -- $record1 - - -- * Getting a subset of fields out of a record - -- $record2 - - -- * Creating a Record out of a conventional Haskell record - -- $record3 - - -- * Injecting into a Variant and eliminating it - -- $variant1 - - -- * Working with a bigger error type inside a function - -- $variant1bError - - -- * Creating a Variant out of a sum type and matching on it - -- $variant2 - - -- * Changing the way a specific record field is parsed from JSON - -- $json1 - - -- * Parsing a record from JSON using aliased fields - -- $json2 - - -- * Parsing a subset of a record's fields from JSON and inserting them in an existing record value - -- $json3 - - -- * Ensuring all branches of a sum type are parsed from JSON - -- $json4sum - - -- * External examples - -- $externalexamples - ) where - -import Data.RBR -import Data.SOP - -{- $setup - ->>> :set -XDataKinds -XTypeApplications ->>> :set -XFlexibleContexts -XTypeFamilies -XAllowAmbiguousTypes -XScopedTypeVariables ->>> :set -XDeriveGeneric ->>> :set -XPartialTypeSignatures ->>> :set -Wno-partial-type-signatures ->>> import Data.RBR ->>> import Data.SOP ->>> import Data.SOP.NP (cpure_NP,sequence_NP,liftA2_NP,collapse_NP) ->>> import Data.String ->>> import Data.Proxy ->>> import Data.Foldable ->>> import Data.Profunctor (Star(..)) ->>> import GHC.Generics ->>> import qualified Data.Text ->>> import Data.Aeson ->>> import Data.Aeson.Types (explicitParseField,Parser,parseMaybe) - --} - -{- $record1 - -We use 'addFieldI' instead of 'addField' because we are dealing with pure -records. - ->>> :{ - let r = addFieldI @"name" "Foo" - . addFieldI @"age" 5 - $ unit - in print (getFieldI @"name" r) -:} -"Foo" - --} - -{- $record2 - -Notice that the subset is specified as a type-level tree using 'FromList', a -type family that takes a list of type-level tuples. - -Because here the types of each field can be inferred, we can use a wildcard -(enabled by the @PartialTypeSignatures@ extension). - ->>> :{ - let r = addFieldI @"name" "Foo" - . addFieldI @"age" 5 - . addFieldI @"whatever" 'x' - $ unit - s = getFieldSubset @(FromList [ '("age",_), '("whatever",_) ]) r - in putStrLn (prettyShowRecordI s) -:} -{age = 5, whatever = 'x'} - --} - -{- $record3 - ->>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) ->>> instance ToRecord Person ->>> :{ - let r = addFieldI @"whatever" 'x' (toRecord (Person "Foo" 50)) - in putStrLn (prettyShowRecordI r) -:} -{age = 50, name = "Foo", whatever = 'x'} - --} - -{- $variant1 - - Here the full type of the 'Variant' is inferred from the type of its - 'Record' of eliminators. - ->>> :{ - let b = injectI @"left" 'c' - e = addCaseI @"left" putChar - . addCaseI @"right" @Bool print - $ unit - in eliminate e b -:} -c - --} - -{- $variant1bError - - A function can use internally an error 'Variant' bigger than the one it - eventually returns. The internal branches of the 'Variant' can be removed with - 'winnow'. - - This library makes it more involved than it should be, because inserting an - entry and then deleting it can result in structurally dissimilar type-level - maps. So we need extra type annotations in 'winnow', and also a call to - 'injectSubset' to perform the conversion. - ->>> type Smaller = FromList '[ '("foo",Char), '("bar",Int) ] ->>> :{ - let func :: Int -> Variant I Smaller - func i = - let v = if (i == 0) then injectI @"baz" "internal" - else injectI @"foo" 'c' - r = case winnowI @"baz" @String @(Insert "baz" String Smaller) v of - Right e -> error "this is the baz internal error" - Left smaller -> smaller - in injectSubset r - in putStrLn $ prettyShowVariantI (func 1) -:} -foo ('c') - --} - - -{- $variant2 - ->>> data Summy = Lefty Int | Righty Bool deriving (Generic,Show) ->>> instance ToVariant Summy ->>> :{ - let v = toVariant (Lefty 5) - in matchI @"Lefty" v -:} -Just 5 - --} - -{- $json1 - - We start in the @sop-core@ world, creating a product of parsing functions - (one for each field) using 'cpure_NP'. - - Then we convert that product to a 'Record', apply to it a transformation - that uses field selectors, and convert it back to a product. - - Then we demote the field names and combine them with the product of - 'Data.Aeson.Value' parsers using 'liftA2_NP', getting a product of - 'Data.Aeson.Object' parsers. - - Then we use 'sequence_NP' to convert the product of parsers into a parser - of 'Record'. - ->>> :{ - let parseSpecial - :: forall r c flat. (Generic r, - FromRecord r, - RecordCode r ~ c, - KeysValuesAll KnownKey c, - Productlike '[] c flat, - All FromJSON flat) - => (Record (Star Parser Data.Aeson.Value) c -> Record (Star Parser Data.Aeson.Value) c) - -> Data.Aeson.Value - -> Parser r - parseSpecial transform = - let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) - fieldParsers = transform $ fromNP @c (cpure_NP (Proxy @FromJSON) (Star parseJSON)) - Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c demoteKeys) (toNP fieldParsers)) - in withObject "someobj" $ \o -> fromRecord <$> parser o - :} - ->>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) ->>> instance ToRecord Person ->>> instance FromRecord Person ->>> :{ - instance FromJSON Person where - parseJSON = parseSpecial (setField @"name" (Star (\_ -> pure "foo"))) - :} - ->>> Data.Aeson.eitherDecode @Person (fromString "{ \"name\" : null, \"age\" : 50 }") -Right (Person {name = "foo", age = 50}) - --} - - -{- $json2 - - The aliases are passed as a 'Record' with values wrapped in the 'K' - functor. This means that there aren't really any values of the type that - corresponds to each field, only the `String` annotations. - ->>> :{ - let parseWithAliases - :: forall r c flat. (Generic r, - FromRecord r, - RecordCode r ~ c, - KeysValuesAll KnownKey c, - Productlike '[] c flat, - All FromJSON flat) - => Record (K String) c - -> Data.Aeson.Value - -> Parser r - parseWithAliases aliases = - let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) - fieldParsers = cpure_NP (Proxy @FromJSON) (Star parseJSON) - Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c aliases) fieldParsers) - in withObject "someobj" $ \o -> fromRecord <$> parser o - :} - - We have to use 'getFieldSubset' because the aliases are listed in a - different order than the record fields, and that might result in different - type-level trees. If the orders were the same, we wouldn't need it. - ->>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) ->>> instance ToRecord Person ->>> instance FromRecord Person ->>> :{ - instance FromJSON Person where - parseJSON = let aliases = addField @"age" (K "bar") - . addField @"name" (K "foo") - $ unit - in parseWithAliases (getFieldSubset @(RecordCode Person) aliases) - :} - ->>> Data.Aeson.eitherDecode @Person (fromString "{ \"foo\" : \"John\", \"bar\" : 50 }") -Right (Person {name = "John", age = 50}) - --} - - - -{- $json3 - ->>> :{ - let parseFieldSubset - :: forall subset subflat c flat r. (Generic r, - FromRecord r, - RecordCode r ~ c, - ProductlikeSubset subset c subflat, - KeysValuesAll KnownKey subset, - All FromJSON subflat) - => r - -> Data.Aeson.Value - -> Parser r - parseFieldSubset r = - let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) - objNP = liftA2_NP mapKSS (toNP @subset demoteKeys) (cpure_NP (Proxy @FromJSON) (Star parseJSON)) - intoOriginal subr = fromRecord (setFieldSubset @subset subr (toRecord r)) - Star subparser = intoOriginal . fromNP @subset <$> sequence_NP objNP - in withObject "someobj" subparser - :} - ->>> data Person = Person { name :: String, age :: Int, whatever :: Bool } deriving (Generic, Show) ->>> instance ToRecord Person ->>> instance FromRecord Person ->>> :{ - let original = Person "John" 50 True - Just v = Data.Aeson.decode @Data.Aeson.Value (fromString "{ \"name\" : \"Mark\", \"age\" : 70 }") - subsetParser = parseFieldSubset @(FromList [ '("name",_), '("age",_) ]) original - Just s = parseMaybe subsetParser v - in s - :} -Person {name = "Mark", age = 70, whatever = True} - --} - - -{- $json4sum - - To ensure that we don't forget any branch when parsing a sum type from JSON, - we can create a n-ary product of parsers, one for each branch. - - Then we create a n-ary product of injections. Each component of the - product creates a n-ary sum out of the value of the corresponding branch. - - We combine the n-ary product of parsers with the n-ary product of - injections, and collapse all the resulting parsers with - 'Control.Applicative.asum'. - - Then we convert the n-ary sum value that "wins" into a 'Variant' and - finally back into the original type. - ->>> :{ - let parseAll - :: forall r c flat. (Generic r, - FromVariant r, - VariantCode r ~ c, - KeysValuesAll KnownKey c, - Productlike '[] c flat, - Sumlike '[] c flat, - All FromJSON flat) - => Data.Aeson.Value - -> Parser r - parseAll = - let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) - branchParsers = liftA2_NP mapKSS (toNP @c demoteKeys) (cpure_NP (Proxy @FromJSON) (Star parseJSON)) - injected = liftA2_NP (\f star -> K (unK . apFn f . I <$> star)) (injections @flat) branchParsers - Star parser = asum $ collapse_NP injected - in withObject "someobj" (\o -> fromVariant @r . fromNS <$> parser o) - :} - ->>> data ThisOrThat = This String | That Int deriving (Generic, Show) ->>> instance FromVariant ThisOrThat ->>> :{ - let Just v = Data.Aeson.decode @Data.Aeson.Value (fromString "{ \"That\" : 70 }") - Just s = parseMaybe (parseAll @ThisOrThat) v - in s - :} -That 70 - --} - -{- $externalexamples - - * [Is there a canonical way of comparing/changing one/two records in haskell? (SO)](https://stackoverflow.com/a/57574731/1364288) - * [Given a record of functions, and a record of data of the types acted on by the functions, how to generically apply the function record? (SO)](https://stackoverflow.com/a/58890226/1364288) - * [Help with Generics. (Reddit)](https://www.reddit.com/r/haskell/comments/cteemj/help_with_generics/expyjfk) - * [Adventures assembling records of capabilities. (Discourse)](https://discourse.haskell.org/t/adventures-assembling-records-of-capabilities/623) - * [Resources on sop-core and generics-sop. (GitHub)](https://github.com/well-typed/generics-sop/issues/47) - --} - +module Data.RBR.Examples ( + -- * Setup code + -- $setup + + -- * Constructing a record and viewing its fields. + -- $record1 + + -- * Getting a subset of fields out of a record + -- $record2 + + -- * Creating a Record out of a conventional Haskell record + -- $record3 + + -- * Injecting into a Variant and eliminating it + -- $variant1 + + -- * Working with a bigger error type inside a function + -- $variant1bError + + -- * Creating a Variant out of a sum type and matching on it + -- $variant2 + + -- * Changing the way a specific record field is parsed from JSON + -- $json1 + + -- * Parsing a record from JSON using aliased fields + -- $json2 + + -- * Parsing a subset of a record's fields from JSON and inserting them in an existing record value + -- $json3 + + -- * Ensuring all branches of a sum type are parsed from JSON + -- $json4sum + + -- * External examples + -- $externalexamples + ) where + +import Data.RBR +import Data.SOP + +{- $setup + +>>> :set -XDataKinds -XTypeApplications +>>> :set -XFlexibleContexts -XTypeFamilies -XAllowAmbiguousTypes -XScopedTypeVariables +>>> :set -XDeriveGeneric +>>> :set -XPartialTypeSignatures +>>> :set -XTypeOperators +>>> :set -Wno-partial-type-signatures +>>> import Data.RBR +>>> import qualified Data.RBR.Subset as S +>>> import Data.SOP +>>> import Data.SOP.NP (cpure_NP,sequence_NP,liftA2_NP,collapse_NP) +>>> import Data.String +>>> import Data.Proxy +>>> import Data.Foldable +>>> import Data.Profunctor (Star(..)) +>>> import GHC.Generics (Generic) +>>> import GHC.TypeLits +>>> import qualified Data.Text +>>> import Data.Aeson +>>> import Data.Aeson.Types (explicitParseField,Parser,parseMaybe) + +-} + +{- $record1 + +We use 'addFieldI' instead of 'addField' because we are dealing with pure +records. + +>>> :{ + let r = addFieldI @"name" "Foo" + . addFieldI @"age" 5 + $ unit + in print (getFieldI @"name" r) +:} +"Foo" + +-} + +{- $record2 + +Notice that the subset is specified as a type-level tree using 'FromList', a +type family that takes a list of type-level tuples. + +Because here the types of each field can be inferred, we can use a wildcard +(enabled by the @PartialTypeSignatures@ extension). + +>>> :{ + let r = addFieldI @"name" "Foo" + . addFieldI @"age" 5 + . addFieldI @"whatever" 'x' + $ unit + s = S.getFieldSubset @(FromList [ '("age",_), '("whatever",_) ]) r + in putStrLn (prettyShow_RecordI s) +:} +{age = 5, whatever = 'x'} + +-} + +{- $record3 + +>>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) +>>> instance ToRecord Person +>>> :{ + let r = addFieldI @"whatever" 'x' (toRecord (Person "Foo" 50)) + in putStrLn (prettyShow_RecordI r) +:} +{age = 50, name = "Foo", whatever = 'x'} + +-} + +{- $variant1 + + Here the full type of the 'Variant' is inferred from the type of its + 'Record' of eliminators. + +>>> :{ + let b = injectI @"left" 'c' + e = addCaseI @"left" putChar + . addCaseI @"right" @Bool print + $ unit + in eliminate_Variant e b +:} +c + +-} + +{- $variant1bError + + A function can use internally an error 'Variant' bigger than the one it + eventually returns. The internal branches of the 'Variant' can be removed with + 'winnow'. + + This library makes it more involved than it should be, because inserting an + entry and then deleting it can result in structurally dissimilar type-level + maps. So we need extra type annotations in 'winnow', and also a call to + 'injectSubset' to perform the conversion. + +>>> type Smaller = FromList '[ '("foo",Char), '("bar",Int) ] +>>> :{ + let func :: Int -> Variant I Smaller + func i = + let v = if (i == 0) then injectI @"baz" "internal" + else injectI @"foo" 'c' + r = case winnowI @"baz" @String @(Insert "baz" String Smaller) v of + Right e -> error "this is the baz internal error" + Left smaller -> smaller + in S.injectSubset r + in putStrLn $ prettyShow_VariantI (func 1) +:} +foo ('c') + +-} + + +{- $variant2 + +>>> data Summy = Lefty Int | Righty Bool deriving (Generic,Show) +>>> instance ToVariant Summy +>>> :{ + let v = toVariant (Lefty 5) + in matchI @"Lefty" v +:} +Just 5 + +-} + +{- $json1 + + We start in the @sop-core@ world, creating a product of parsing functions + (one for each field) using 'cpure_NP'. + + Then we convert that product to a 'Record', apply to it a transformation + that uses field selectors, and convert it back to a product. + + Then we demote the field names and combine them with the product of + 'Data.Aeson.Value' parsers using 'liftA2_NP', getting a product of + 'Data.Aeson.Object' parsers. + + Then we use 'sequence_NP' to convert the product of parsers into a parser + of 'Record'. + +>>> :{ + let parseSpecial + :: forall r c flat. (IsRecordType r c, + Maplike c, + KeysValuesAll (KeyValueConstraints KnownSymbol FromJSON) c) + => (Record ((,) String :.: Star Parser Data.Aeson.Value) c -> Record ((,) String :.: Star Parser Data.Aeson.Value) c) + -> Data.Aeson.Value + -> Parser r + parseSpecial transform = + let fieldParsers = transform $ + cpure'_Record (Proxy @FromJSON) $ \fieldName -> Comp (fieldName,Star parseJSON) + applyName (Comp (fieldName,Star f)) = Star (\o -> explicitParseField f o (Data.Text.pack fieldName)) + Star objectParser = sequence_Record $ liftA_Record applyName fieldParsers + in withObject "someobj" $ \o -> fromRecord <$> objectParser o + :} + +>>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) +>>> instance ToRecord Person +>>> instance FromRecord Person +>>> :{ + instance FromJSON Person where + parseJSON = parseSpecial (setField @"name" (Comp ("anothername",Star (\_ -> pure "foo")))) + :} + +>>> Data.Aeson.eitherDecode @Person (fromString "{ \"anothername\" : null, \"age\" : 50 }") +Right (Person {name = "foo", age = 50}) + +-} + + +{- $json2 + + The aliases are passed as a 'Record' with values wrapped in the 'K' + functor. This means that there aren't really any values of the type that + corresponds to each field, only the `String` annotations. + +>>> :{ + let parseWithAliases + :: forall r c flat. (IsRecordType r c, + Maplike c, + KeysValuesAll (ValueConstraint FromJSON) c) + => Record (K String) c + -> Data.Aeson.Value + -> Parser r + parseWithAliases aliases = + let fieldParsers = cpure_Record (Proxy @(ValueConstraint FromJSON)) (Star parseJSON) + mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) + Star objectParser = sequence_Record $ liftA2_Record mapKSS aliases fieldParsers + in withObject "someobj" $ \o -> fromRecord <$> objectParser o + :} + + We have to use 'getFieldSubset' because the aliases are listed in a + different order than the record fields, and that might result in different + type-level trees. If the orders were the same, we wouldn't need it. + +>>> data Person = Person { name :: String, age :: Int } deriving (Generic, Show) +>>> instance ToRecord Person +>>> instance FromRecord Person +>>> :{ + instance FromJSON Person where + parseJSON = let aliases = addField @"age" (K "bar") + . addField @"name" (K "foo") + $ unit + in parseWithAliases (S.getFieldSubset @(RecordCode Person) aliases) + :} + +>>> Data.Aeson.eitherDecode @Person (fromString "{ \"foo\" : \"John\", \"bar\" : 50 }") +Right (Person {name = "John", age = 50}) + +-} + + + +{- $json3 + +>>> :{ + let parseFieldSubset + :: forall subset c r. (IsRecordType r c, + S.Subset subset c, + Maplike subset, + KeysValuesAll (KeyValueConstraints KnownSymbol FromJSON) subset) + => r + -> Data.Aeson.Value + -> Parser r + parseFieldSubset r = + let subparser = + sequence_Record $ + cpure'_Record (Proxy @FromJSON) $ \fieldName -> + Star (\o -> explicitParseField parseJSON o (Data.Text.pack fieldName)) + intoOriginal subrecord = fromRecord (S.setFieldSubset @subset subrecord (toRecord r)) + Star parser = intoOriginal <$> subparser + in withObject "someobj" parser + :} + +>>> data Person = Person { name :: String, age :: Int, whatever :: Bool } deriving (Generic, Show) +>>> instance ToRecord Person +>>> instance FromRecord Person +>>> :{ + let original = Person "John" 50 True + Just v = Data.Aeson.decode @Data.Aeson.Value (fromString "{ \"name\" : \"Mark\", \"age\" : 70 }") + subsetParser = parseFieldSubset @(FromList [ '("name",_), '("age",_) ]) original + Just s = parseMaybe subsetParser v + in s + :} +Person {name = "Mark", age = 70, whatever = True} + +-} + + +{- $json4sum + + To ensure that we don't forget any branch when parsing a sum type from JSON, + we can create a n-ary product of parsers, one for each branch. + + Then we create a n-ary product of injections. Each component of the + product creates a n-ary sum out of the value of the corresponding branch. + + We combine the n-ary product of parsers with the n-ary product of + injections, and collapse all the resulting parsers with + 'Control.Applicative.asum'. + + Then we convert the n-ary sum value that "wins" into a 'Variant' and + finally back into the original type. + +>>> :{ + let parseAll + :: forall r c flat. (IsVariantType r c, + Maplike c, + KeysValuesAll (KeyValueConstraints KnownSymbol FromJSON) c) + => Data.Aeson.Value + -> Parser r + parseAll = + let fieldParsers = cpure'_Record (Proxy @FromJSON) $ \fieldName -> + Star (\o -> explicitParseField parseJSON o (Data.Text.pack fieldName)) + injected = liftA2_Record (\f star -> K [ runVariantInjection f . I <$> star ]) injections_Variant fieldParsers + Star parser = asum $ collapse'_Record injected + in withObject "someobj" (\o -> fromVariant <$> parser o) + :} + +>>> data ThisOrThat = This String | That Int deriving (Generic, Show) +>>> instance FromVariant ThisOrThat +>>> instance ToVariant ThisOrThat +>>> :{ + let Just v = Data.Aeson.decode @Data.Aeson.Value (fromString "{ \"That\" : 70 }") + Just s = parseMaybe (parseAll @ThisOrThat) v + in s + :} +That 70 + +-} + +{- $externalexamples + + * [Is there a canonical way of comparing/changing one/two records in haskell? (SO)](https://stackoverflow.com/a/57574731/1364288) + * [Given a record of functions, and a record of data of the types acted on by the functions, how to generically apply the function record? (SO)](https://stackoverflow.com/a/58890226/1364288) + * [Help with Generics. (Reddit)](https://www.reddit.com/r/haskell/comments/cteemj/help_with_generics/expyjfk) + * [Adventures assembling records of capabilities. (Discourse)](https://discourse.haskell.org/t/adventures-assembling-records-of-capabilities/623) + * [Creating a result piecewise from stateful computation. (SO)](https://stackoverflow.com/a/60067270/1364288) + * [Extracting sections of function pipelines. (GitHub)](https://gist.github.com/danidiaz/2157e68f5d4967e468a9d062d4476adf#file-pipelines3-hs) + * [Resources on sop-core and generics-sop. (GitHub)](https://github.com/well-typed/generics-sop/issues/47) + +-} + diff --git a/lib/Data/RBR/Internal.hs b/lib/Data/RBR/Internal.hs --- a/lib/Data/RBR/Internal.hs +++ b/lib/Data/RBR/Internal.hs @@ -1,1897 +1,2065 @@ --- | See for --- the original term-level code by Stefan Kahrs. It is also copied at the end --- of this file. Some parts of the type-level code include the correspondign --- term-level parts in their comments. -{-# LANGUAGE DataKinds, - TypeOperators, - ConstraintKinds, - PolyKinds, - TypeFamilies, - GADTs, - MultiParamTypeClasses, - FunctionalDependencies, - FlexibleInstances, - FlexibleContexts, - UndecidableInstances, - UndecidableSuperClasses, - TypeApplications, - ScopedTypeVariables, - AllowAmbiguousTypes, - ExplicitForAll, - RankNTypes, - DefaultSignatures, - PartialTypeSignatures, - LambdaCase, - EmptyCase -#-} -{-# OPTIONS_GHC -Wno-partial-type-signatures #-} - -module Data.RBR.Internal where - -import Data.Proxy -import Data.Kind -import Data.Typeable -import Data.Coerce -import Data.Functor.Contravariant (Contravariant(contramap)) -import Data.Bifunctor (first) -import Data.Monoid (Endo(..)) -import Data.List (intersperse) -import Data.Foldable (asum) -import GHC.TypeLits -import GHC.Generics (D1,C1,S1(..),M1(..),K1(..),Rec0(..)) -import qualified GHC.Generics as G - -import Data.SOP (I(..),K(..),unI,unK,NP(..),NS(..),All,SListI,type (-.->)(Fn,apFn),mapKIK) -import Data.SOP.NP (collapse_NP,liftA_NP,liftA2_NP,cliftA_NP,cliftA2_NP,pure_NP) -import Data.SOP.NS (collapse_NS,ap_NS,injections,Injection) - - -{- $setup - ->>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric ->>> :set -Wno-partial-type-signatures ->>> import Data.RBR ->>> import Data.SOP ->>> import GHC.Generics - --} - - --- | The color of a node. -data Color = R - | B - deriving (Show,Eq) - --- | A Red-Black tree. It will be used as a kind, to index the 'Record' and 'Variant' types. -data Map symbol q = E - | N Color (Map symbol q) symbol q (Map symbol q) - deriving (Show,Eq) - --- | A map without entries. See also 'unit' and 'impossible'. -type Empty = E - --- --- --- This code has been copied and adapted from the corresponding Data.SOP code (the All constraint). --- - --- Why is this KeysValuesAllF type family needed at all? Why is not KeysValuesAll sufficient by itself? --- In fact, if I delete KeysValuesAllF and use eclusively KeysValuesAll, functions like demoteKeys seem to still work fine. --- --- UndecidableSuperClasses and RankNTypes seem to be required by KeysValuesAllF. -type family - KeysValuesAllF (c :: symbol -> q -> Constraint) (t :: Map symbol q) :: Constraint where - KeysValuesAllF _ E = () - KeysValuesAllF c (N color left k v right) = (c k v, KeysValuesAll c left, KeysValuesAll c right) - -{- | Require a constraint for every key-value pair in a tree. This is a generalization of 'Data.SOP.All' from "Data.SOP". --} -class KeysValuesAllF c t => KeysValuesAll (c :: symbol -> q -> Constraint) (t :: Map symbol q) where - - -- 'cpara_Map' constructs a 'Record' by means of a constraint for producing - -- the nodes of the tree. The constraint is passed as a 'Data.Proxy.Proxy'. - cpara_Map :: - proxy c - -> r E - -> (forall left k v right color . (c k v, KeysValuesAll c left, KeysValuesAll c right) - => r left -> r right -> r (N color left k v right)) - -> r t - -instance KeysValuesAll c E where - cpara_Map _p nil _step = nil - -instance (c k v, KeysValuesAll c left, KeysValuesAll c right) => KeysValuesAll c (N color left k v right) where - cpara_Map p nil cons = - cons (cpara_Map p nil cons) (cpara_Map p nil cons) - -{- | - Create a 'Record', knowing that both keys and values satisfy a 2-place constraint. The constraint is passed as a 'Data.Proxy.Proxy'. - - The naming scheme follows that of 'Data.SOP.NP.cpure_NP'. - -} -cpure_Record :: forall c t f. KeysValuesAll c t => (Proxy c) -> (forall k v. c k v => f v) -> Record f t -cpure_Record _ fpure = cpara_Map (Proxy @c) unit go - where - go :: forall left k' v' right color. (c k' v', KeysValuesAll c left, KeysValuesAll c right) - => Record f left - -> Record f right - -> Record f (N color left k' v' right) - go left right = Node left (fpure @k' @v') right - -{- | Create a 'Record' containing the names of each field. - - The names are represented by a constant functor 'K' carrying an annotation - of type 'String'. This means that there aren't actually any values of the - type that corresponds to each field, only the 'String' annotations. - ->>> putStrLn $ prettyShowRecord show $ demoteKeys @(Insert "foo" Char (Insert "bar" Bool Empty)) -{bar = K "bar", foo = K "foo"} - --} -demoteKeys :: forall t. KeysValuesAll KnownKey t => Record (K String) t -demoteKeys = cpara_Map (Proxy @KnownKey) unit go - where - go :: forall left k v right color. (KnownKey k v, KeysValuesAll KnownKey left, KeysValuesAll KnownKey right) - => Record (K String) left - -> Record (K String) right - -> Record (K String) (N color left k v right) - go left right = Node left (K (symbolVal (Proxy @k))) right - -{- | - Two-place constraint saying that a 'Symbol' key can be demoted to 'String'. Nothing is required from the corresponding value. - - Defined using the "class synonym" . --} -class KnownSymbol k => KnownKey (k :: Symbol) (v :: q) -instance KnownSymbol k => KnownKey k v - -{- | - Create a record containing the names of each field along with a term-level - representation of each type. - ->>> putStrLn $ prettyShowRecord show $ demoteEntries @(Insert "foo" Char (Insert "bar" Bool Empty)) -{bar = K ("bar",Bool), foo = K ("foo",Char)} - - See also 'collapse_Record' for getting the entries as a list. --} -demoteEntries :: forall t. KeysValuesAll KnownKeyTypeableValue t => Record (K (String,TypeRep)) t -demoteEntries = cpara_Map (Proxy @KnownKeyTypeableValue) unit go - where - go :: forall left k v right color. (KnownKeyTypeableValue k v, KeysValuesAll KnownKeyTypeableValue left, KeysValuesAll KnownKeyTypeableValue right) - => Record (K (String,TypeRep)) left - -> Record (K (String,TypeRep)) right - -> Record (K (String,TypeRep)) (N color left k v right) - go left right = Node left (K (symbolVal (Proxy @k),typeRep (Proxy @v))) right - -{- | - Two-place constraint saying that a 'Symbol' key can be demoted to 'String', and that the corresponding value 'Type' has a term-level representation. - - Defined using the "class synonym" . --} -class (KnownSymbol k, Typeable v) => KnownKeyTypeableValue (k :: Symbol) (v :: q) -instance (KnownSymbol k, Typeable v) => KnownKeyTypeableValue k v - --- class KeyValueTop (k :: Symbol) (v :: z) --- instance KeyValueTop k v - --- --- - -{- | An extensible product-like type with named fields. - - The values in the 'Record' come wrapped in a type constructor @f@, which - por pure records will be the identity functor 'I'. - - See also 'insert', 'delete' and 'project'. --} -data Record (f :: q -> Type) (t :: Map Symbol q) where - Empty :: Record f E - Node :: Record f left -> f v -> Record f right -> Record f (N color left k v right) - -instance (Productlike '[] t result, Show (NP f result)) => Show (Record f t) where - show x = "fromNP (" ++ show (toNP x) ++ ")" - - -{- | Collapse a 'Record' composed of 'K' annotations. - ->>> collapse_Record unit -[] - ->>> collapse_Record (insert @"bar" (K False) unit) -[False] - - The naming scheme follows that of 'Data.SOP.NP.collapse_NP'. - --} -collapse_Record :: forall t result a. (Productlike '[] t result) => Record (K a) t -> [a] -collapse_Record = collapse_NP . toNP - -{- | Show a 'Record' in a friendlier way than the default 'Show' instance. The - function argument will usually be 'show', but it can be used to unwrap the - value of each field before showing it. --} -prettyShowRecord :: forall t flat f. (KeysValuesAll KnownKey t,Productlike '[] t flat, All Show flat, SListI flat) - => (forall x. Show x => f x -> String) - -> Record f t - -> String -prettyShowRecord showf r = - let keysflat = toNP @t (demoteKeys @t) - valuesflat = toNP @t r - entries = cliftA2_NP (Proxy @Show) (\(K key) fv -> K (key ++ " = " ++ showf fv)) - keysflat - valuesflat - in "{" ++ mconcat (intersperse ", " (collapse_NP entries)) ++ "}" - - -{- | Like 'prettyShowRecord' but specialized to pure records. --} -prettyShowRecordI :: forall t flat. (KeysValuesAll KnownKey t,Productlike '[] t flat, All Show flat, SListI flat) => Record I t -> String -prettyShowRecordI r = prettyShowRecord (show . unI) r - -{-| A Record without components is a boring, uninformative type whose single value can be conjured out of thin air. --} -unit :: Record f Empty -unit = Empty - -{- | An extensible sum-like type with named branches. - - The values in the 'Variant' come wrapped in a type constructor @f@, which - por pure variants will be the identity functor 'I'. - - See also 'widen', 'winnow' and 'inject'. --} -data Variant (f :: q -> Type) (t :: Map Symbol q) where - Here :: f v -> Variant f (N color left k v right) - LookRight :: Variant f t -> Variant f (N color' left' k' v' t) - LookLeft :: Variant f t -> Variant f (N color' t k' v' right') - -instance (Sumlike '[] t result, Show (NS f result)) => Show (Variant f t) where - show x = "fromNS (" ++ show (toNS x) ++ ")" - -{-| A Variant without branches doesn't have any values. From an impossible thing, anything can come out. --} -impossible :: Variant f Empty -> b -impossible v = case v of - -{- | Show a 'Variant' in a friendlier way than the default 'Show' instance. The - function argument will usually be 'show', but it can be used to unwrap the - value of the branch before showing it. --} -prettyShowVariant :: forall t flat f. (KeysValuesAll KnownKey t,Productlike '[] t flat, Sumlike '[] t flat, All Show flat, SListI flat) - => (forall x. Show x => f x -> String) - -> Variant f t - -> String -prettyShowVariant showf v = - let keysflat = toNP @t (demoteKeys @t) - eliminators = cliftA_NP (Proxy @Show) (\(K k) -> Fn (\fv -> (K (k ++ " (" ++ showf fv ++ ")")))) keysflat - valuesflat = toNS @t v - in collapse_NS (ap_NS eliminators valuesflat) - -{- | Like 'prettyShowVariant' but specialized to pure variants. --} -prettyShowVariantI :: forall t flat. (KeysValuesAll KnownKey t,Productlike '[] t flat, Sumlike '[] t flat, All Show flat, SListI flat) - => Variant I t -> String -prettyShowVariantI v = prettyShowVariant (show . unI) v - --- --- --- Insertion - -{- | Insert a list of type level key / value pairs into a type-level map. --} -type family InsertAll (es :: [(Symbol,q)]) (t :: Map Symbol q) :: Map Symbol q where - InsertAll '[] t = t - InsertAll ( '(name,fieldType) ': es ) t = Insert name fieldType (InsertAll es t) - -{- | Build a type-level map out of a list of type level key / value pairs. --} -type FromList (es :: [(Symbol,q)]) = InsertAll es Empty - - -{- | - Adds a new field to a 'Record'. - ->>> project @"foo" (insert @"foo" (I 'a') unit) -I 'a' - ->>> project @"foo" (insert @"foo" @Char Nothing unit) -Nothing - - -} -insert :: forall k v t f. Insertable k v t => f v -> Record f t -> Record f (Insert k v t) -insert = _insert @_ @k @v @t @f - -{- | - Lets you use a 'Variant' in a bigger context - than the one in which is was defined. - -} -widen :: forall k v t f. Insertable k v t => Variant f t -> Variant f (Insert k v t) -widen = _widen @_ @k @v @t @f - -{- | Alias for 'insert'. --} -addField :: forall k v t f. Insertable k v t => f v -> Record f t -> Record f (Insert k v t) -addField = insert @k @v @t @f - -{- | Like 'insert' but specialized to pure 'Record's. - ->>> projectI @"foo" (insertI @"foo" 'a' unit) -'a' - --} -insertI :: forall k v t . Insertable k v t => v -> Record I t -> Record I (Insert k v t) -insertI = insert @k @v @t . I - -{- | Like 'addField' but specialized to pure 'Record's. --} -addFieldI :: forall k v t . Insertable k v t => v -> Record I t -> Record I (Insert k v t) -addFieldI = insertI @k @v @t - -{- | Class that determines if the pair of a 'Symbol' key and a type can - be inserted into a type-level map. - - The associated type family 'Insert' produces the resulting map. - - At the term level, this manifests in 'insert', which adds a new field to a - record, and in 'widen', which lets you use a 'Variant' in a bigger context - than the one in which is was defined. 'insert' tends to be more useful in - practice. - - If the map already has the key but with a /different/ type, the - insertion fails to compile. - -} -class Insertable (k :: Symbol) (v :: q) (t :: Map Symbol q) where - type Insert k v t :: Map Symbol q - _insert :: f v -> Record f t -> Record f (Insert k v t) - _widen :: Variant f t -> Variant f (Insert k v t) - --- insert x s = --- T B a z b --- where --- T _ a z b = ins s -instance (InsertableHelper1 k v t, Insert1 k v t ~ inserted, CanMakeBlack inserted) => Insertable k v t where - type Insert k v t = MakeBlack (Insert1 k v t) - _insert fv r = makeBlackR @_ (insert1 @_ @k @v fv r) - _widen v = makeBlackV @_ (widen1 @_ @k @v v) - -class CanMakeBlack (t :: Map Symbol k) where - type MakeBlack t :: Map Symbol k - makeBlackR :: Record f t -> Record f (MakeBlack t) - makeBlackV :: Variant f t -> Variant f (MakeBlack t) - -instance CanMakeBlack (N color left k v right) where - type MakeBlack (N color left k v right) = N B left k v right - makeBlackR (Node left fv right) = Node left fv right - makeBlackV v = case v of - LookLeft l -> LookLeft l - Here v -> Here v - LookRight r -> LookRight r - -instance CanMakeBlack E where - type MakeBlack E = E - makeBlackR Empty = Empty - makeBlackV = impossible - -class InsertableHelper1 (k :: Symbol) - (v :: q) - (t :: Map Symbol q) where - type Insert1 k v t :: Map Symbol q - insert1 :: f v -> Record f t -> Record f (Insert1 k v t) - widen1 :: Variant f t -> Variant f (Insert1 k v t) - -instance InsertableHelper1 k v E where - type Insert1 k v E = N R E k v E - insert1 fv Empty = Node Empty fv Empty - widen1 = impossible - -instance (CmpSymbol k k' ~ ordering, - InsertableHelper2 ordering k v color left k' v' right - ) - => InsertableHelper1 k v (N color left k' v' right) where - -- FIXME possible duplicate work with CmpSymbol: both in constraint and in associated type family. - -- Is that bad? How to avoid it? - type Insert1 k v (N color left k' v' right) = Insert2 (CmpSymbol k k') k v color left k' v' right - insert1 = insert2 @_ @ordering @k @v @color @left @k' @v' @right - widen1 = widen2 @_ @ordering @k @v @color @left @k' @v' @right - -class InsertableHelper2 (ordering :: Ordering) - (k :: Symbol) - (v :: q) - (color :: Color) - (left :: Map Symbol q) - (k' :: Symbol) - (v' :: q) - (right :: Map Symbol q) where - type Insert2 ordering k v color left k' v' right :: Map Symbol q - insert2 :: f v -> Record f (N color left k' v' right) -> Record f (Insert2 ordering k v color left k' v' right) - widen2 :: Variant f (N color left k' v' right) -> Variant f (Insert2 ordering k v color left k' v' right) - --- ins s@(T B a y b) --- | x InsertableHelper2 LT k v B left k' v' right where - type Insert2 LT k v B left k' v' right = Balance (Insert1 k v left) k' v' right - insert2 fv (Node left fv' right) = balanceR @_ @_ @k' @v' @right (Node (insert1 @_ @k @v fv left) fv' right) - widen2 v = balanceV @_ @(Insert1 k v left) @k' @v' @right $ case v of - Here x -> Here x - LookLeft x -> LookLeft (widen1 @_ @k @v x) - LookRight x -> LookRight x - --- ins s@(T B a y b) --- | x InsertableHelper2 LT k v R left k' v' right where - type Insert2 LT k v R left k' v' right = N R (Insert1 k v left) k' v' right - insert2 fv (Node left fv' right) = Node (insert1 @_ @k @v fv left) fv' right - widen2 v = case v of - Here x -> Here x - LookLeft x -> LookLeft (widen1 @_ @k @v x) - LookRight x -> LookRight x - - --- This instance implies that we can't change the type associated to an --- existing key. If we did that, we wouldn't be able to widen Variants that --- happen to match that key! -instance InsertableHelper2 EQ k v color left k v right where - type Insert2 EQ k v color left k v right = N color left k v right - insert2 fv (Node left _ right) = Node left fv right - widen2 = id - --- ins s@(T B a y b) --- | ... --- | x>y = balance a y (ins b) -instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted, - Balanceable left k' v' inserted - ) - => InsertableHelper2 GT k v B left k' v' right where - type Insert2 GT k v B left k' v' right = Balance left k' v' (Insert1 k v right) - insert2 fv (Node left fv' right) = balanceR @_ @left @k' @v' @_ (Node left fv' (insert1 @_ @k @v fv right)) - widen2 v = balanceV @_ @left @k' @v' @(Insert1 k v right) $ case v of - Here x -> Here x - LookLeft x -> LookLeft x - LookRight x -> LookRight (widen1 @_ @k @v x) - --- ins s@(T R a y b) --- | ... --- | x>y = T R a y (ins b) -instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted, - Balanceable left k' v' inserted - ) - => InsertableHelper2 GT k v R left k' v' right where - type Insert2 GT k v R left k' v' right = N R left k' v' (Insert1 k v right) - insert2 fv (Node left fv' right) = Node left fv' (insert1 @_ @k @v fv right) - widen2 v = case v of - Here x -> Here x - LookLeft x -> LookLeft x - LookRight x -> LookRight (widen1 @_ @k @v x) - -data BalanceAction = BalanceSpecial - | BalanceLL - | BalanceLR - | BalanceRL - | BalanceRR - | DoNotBalance - deriving Show - -type family ShouldBalance (left :: Map k' v') (right :: Map k' v') :: BalanceAction where - ShouldBalance (N R _ _ _ _) (N R _ _ _ _) = BalanceSpecial - ShouldBalance (N R (N R _ _ _ _) _ _ _) _ = BalanceLL - ShouldBalance (N R _ _ _ (N R _ _ _ _)) _ = BalanceLR - ShouldBalance _ (N R (N R _ _ _ _) _ _ _) = BalanceRL - ShouldBalance _ (N R _ _ _ (N R _ _ _ _)) = BalanceRR - ShouldBalance _ _ = DoNotBalance - -class Balanceable (left :: Map Symbol q) (k :: Symbol) (v :: q) (right :: Map Symbol q) where - type Balance left k v right :: Map Symbol q - balanceR :: Record f (N color left k v right) -> Record f (Balance left k v right) - balanceV :: Variant f (N color left k v right) -> Variant f (Balance left k v right) - -instance (ShouldBalance left right ~ action, - BalanceableHelper action left k v right - ) - => Balanceable left k v right where - -- FIXME possible duplicate work with ShouldBalance: both in constraint and in associated type family. - -- Is that bad? How to avoid it? - type Balance left k v right = Balance' (ShouldBalance left right) left k v right - balanceR = balanceR' @_ @action @left @k @v @right - balanceV = balanceV' @_ @action @left @k @v @right - -class BalanceableHelper (action :: BalanceAction) - (left :: Map Symbol q) - (k :: Symbol) - (v :: q) - (right :: Map Symbol q) where - type Balance' action left k v right :: Map Symbol q - balanceR' :: Record f (N color left k v right) -> Record f (Balance' action left k v right) - balanceV' :: Variant f (N color left k v right) -> Variant f (Balance' action left k v right) - --- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d) -instance BalanceableHelper BalanceSpecial (N R left1 k1 v1 right1) kx vx (N R left2 k2 v2 right2) where - type Balance' BalanceSpecial (N R left1 k1 v1 right1) kx vx (N R left2 k2 v2 right2) = - N R (N B left1 k1 v1 right1) kx vx (N B left2 k2 v2 right2) - balanceR' (Node (Node left1 v1 right1) vx (Node left2 v2 right2)) = - (Node (Node left1 v1 right1) vx (Node left2 v2 right2)) - balanceV' v = case v of - LookLeft (LookLeft x) -> LookLeft (LookLeft x) - LookLeft (Here x) -> LookLeft (Here x) - LookLeft (LookRight x) -> LookLeft (LookRight x) - Here x -> Here x - LookRight (LookLeft x) -> LookRight (LookLeft x) - LookRight (Here x) -> LookRight (Here x) - LookRight (LookRight x) -> LookRight (LookRight x) - --- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) -instance BalanceableHelper BalanceLL (N R (N R a k1 v1 b) k2 v2 c) k3 v3 d where - type Balance' BalanceLL (N R (N R a k1 v1 b) k2 v2 c) k3 v3 d = - N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d) - balanceR' (Node (Node (Node a fv1 b) fv2 c) fv3 d) = - Node (Node a fv1 b) fv2 (Node c fv3 d) - balanceV' v = case v of - LookLeft (LookLeft x) -> LookLeft (case x of LookLeft y -> LookLeft y - Here y -> Here y - LookRight y -> LookRight y) - LookLeft (Here x) -> Here x - LookLeft (LookRight x) -> LookRight (LookLeft x) - Here x -> LookRight (Here x) - LookRight x -> LookRight (LookRight x) - --- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) -instance BalanceableHelper BalanceLR (N R a k1 v1 (N R b k2 v2 c)) k3 v3 d where - type Balance' BalanceLR (N R a k1 v1 (N R b k2 v2 c)) k3 v3 d = - N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d) - balanceR' (Node (Node a fv1 (Node b fv2 c)) fv3 d) = - Node (Node a fv1 b) fv2 (Node c fv3 d) - balanceV' v = case v of - LookLeft (LookLeft x) -> LookLeft (LookLeft x) - LookLeft (Here x) -> LookLeft (Here x) - LookLeft (LookRight x) -> case x of LookLeft y -> LookLeft (LookRight y) - Here y -> Here y - LookRight y -> LookRight (LookLeft y) - Here x -> LookRight (Here x) - LookRight x -> LookRight (LookRight x) - --- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) -instance BalanceableHelper BalanceRL a k1 v1 (N R (N R b k2 v2 c) k3 v3 d) where - type Balance' BalanceRL a k1 v1 (N R (N R b k2 v2 c) k3 v3 d) = - N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d) - balanceR' (Node a fv1 (Node (Node b fv2 c) fv3 d)) = - Node (Node a fv1 b) fv2 (Node c fv3 d) - balanceV' v = case v of - LookLeft x -> LookLeft (LookLeft x) - Here x -> LookLeft (Here x) - LookRight (LookLeft x) -> case x of LookLeft y -> LookLeft (LookRight y) - Here y -> Here y - LookRight y -> LookRight (LookLeft y) - LookRight (Here x) -> LookRight (Here x) - LookRight (LookRight x) -> LookRight (LookRight x) - - --- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) -instance BalanceableHelper BalanceRR a k1 v1 (N R b k2 v2 (N R c k3 v3 d)) where - type Balance' BalanceRR a k1 v1 (N R b k2 v2 (N R c k3 v3 d)) = - N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d) - balanceR' (Node a fv1 (Node b fv2 (Node c fv3 d))) = - Node (Node a fv1 b) fv2 (Node c fv3 d) - balanceV' v = case v of - LookLeft x -> LookLeft (LookLeft x) - Here x -> LookLeft (Here x) - LookRight (LookLeft x) -> LookLeft (LookRight x) - LookRight (Here x) -> Here x - LookRight (LookRight x) -> LookRight (case x of LookLeft y -> LookLeft y - Here y -> Here y - LookRight y -> LookRight y) - --- balance a x b = T B a x b -instance BalanceableHelper DoNotBalance a k v b where - type Balance' DoNotBalance a k v b = N B a k v b - balanceR' (Node left v right) = (Node left v right) - balanceV' v = case v of - LookLeft l -> LookLeft l - Here v -> Here v - LookRight r -> LookRight r - - --- --- --- Accessing fields - --- --- These two type families exist to avoid duplicating expensive type-level --- computations, in particular the Value' computations. --- --- Record accessors are compiled WAY slower without them! --- -{- | Auxiliary type family to avoid repetition and help improve compilation times. - -} -type family Field (f :: q -> Type) (t :: Map Symbol q) (v :: q) where - Field f t v = Record f t -> (f v -> Record f t, f v) - -{- | Auxiliary type family to avoid repetition and help improve compilation times. - -} -type family Branch (f :: q -> Type) (t :: Map Symbol q) (v :: q) where - Branch f t v = (Variant f t -> Maybe (f v), f v -> Variant f t) - --- -{- | - Class that determines if a given 'Symbol' key is present in a type-level - map. - - The 'Value' type family gives the 'Type' corresponding to the key. --} -class Key (k :: Symbol) (t :: Map Symbol q) where - type Value k t :: q - _field :: Field f t (Value k t) - _branch :: Branch f t (Value k t) - -{- | - Takes a field name (given through @TypeApplications@) and a - 'Record', and returns a pair of a setter for the field and the original - value of the field. --} -field :: forall k t f. Key k t => Field f t (Value k t) -field = _field @_ @k @t - -{- | - Takes a branch name (given through @TypeApplications@) and - returns a pair of a match function and a constructor. --} -branch :: forall k t f. Key k t => Branch f t (Value k t) -branch = _branch @_ @k @t - --- member :: Ord a => a -> RB a -> Bool -class KeyHelper (ordering :: Ordering) (k :: Symbol) (left :: Map Symbol q) (v :: q) (right :: Map Symbol q) where - type Value' ordering k left v right :: q - field' :: Field f (N colorx left kx v right) (Value' ordering k left v right) - branch' :: Branch f (N colorx left kx v right) (Value' ordering k left v right) - -instance (CmpSymbol k' k ~ ordering, KeyHelper ordering k left v' right) => Key k (N color left k' v' right) where - type Value k (N color left k' v' right) = Value' (CmpSymbol k' k) k left v' right - _field = field' @_ @ordering @k @left @v' @right - _branch = branch' @_ @ordering @k @left @v' @right - --- | x KeyHelper LT k left v (N color2 left2 k2 v2 right2) where - type Value' LT k left v (N color2 left2 k2 v2 right2) = Value' (CmpSymbol k2 k) k left2 v2 right2 - field' (Node left fv right) = - let (setter,x) = field' @_ @ordering @k @left2 @v2 @right2 right - in (\z -> Node left fv (setter z),x) - branch' = - let (match,inj) = branch' @_ @ordering @k @left2 @v2 @right2 - in (\case LookRight x -> match x - _ -> Nothing, - \fv -> LookRight (inj fv)) - --- | x>y = member x b -instance (CmpSymbol k2 k ~ ordering, KeyHelper ordering k left2 v2 right2) - => KeyHelper GT k (N color2 left2 k2 v2 right2) v' right where - type Value' GT k (N color2 left2 k2 v2 right2) v' right = Value' (CmpSymbol k2 k) k left2 v2 right2 - field' (Node left fv right) = - let (setter,x) = field' @_ @ordering @k @left2 @v2 @right2 left - in (\z -> Node (setter z) fv right,x) - branch' = - let (match,inj) = branch' @_ @ordering @k @left2 @v2 @right2 - in (\case LookLeft x -> match x - _ -> Nothing, - \fv -> LookLeft (inj fv)) - --- | otherwise = True -instance KeyHelper EQ k left v right where - type Value' EQ k left v right = v - field' (Node left fv right) = (\x -> Node left x right, fv) - branch' = (\case Here x -> Just x - _ -> Nothing, - Here) - -{- | Get the value of a field for a 'Record'. - - --} -project :: forall k t f . Key k t => Record f t -> f (Value k t) -project = snd . field @k @t - -{- | Alias for 'project'. --} -getField :: forall k t f . Key k t => Record f t -> f (Value k t) -getField = project @k @t @f - -{- | Set the value of a field for a 'Record'. --} -setField :: forall k t f . Key k t => f (Value k t) -> Record f t -> Record f t -setField fv r = fst (field @k @t @f r) fv - -{- | Modify the value of a field for a 'Record'. --} -modifyField :: forall k t f . Key k t => (f (Value k t) -> f (Value k t)) -> Record f t -> Record f t -modifyField f r = uncurry ($) (fmap f (field @k @t @f r)) - -{- | Put a value into the branch of a 'Variant'. - ->>> match @"foo" (inject @"foo" (I 'a') :: Variant I (Insert "foo" Char Empty)) -Just (I 'a') - --} -inject :: forall k t f. Key k t => f (Value k t) -> Variant f t -inject = snd (branch @k @t) - -{- | Check if a 'Variant' value is the given branch. --} -match :: forall k t f. Key k t => Variant f t -> Maybe (f (Value k t)) -match = fst (branch @k @t) - -{- | Like 'project' but specialized to pure 'Record's. - ->>> projectI @"foo" (insertI @"foo" 'a' (insertI @"bar" False unit)) -'a' - --} -projectI :: forall k t . Key k t => Record I t -> Value k t -projectI = unI . snd . field @k @t - -{- | Like 'getField' but specialized to pure 'Record's. --} -getFieldI :: forall k t . Key k t => Record I t -> Value k t -getFieldI = projectI @k @t - -{- | Like 'setField' but specialized to pure 'Record's. --} -setFieldI :: forall k t . Key k t => Value k t -> Record I t -> Record I t -setFieldI v r = fst (field @k @t r) (I v) - -{- | Like 'modifyField' but specialized to pure 'Record's. --} -modifyFieldI :: forall k t . Key k t => (Value k t -> Value k t) -> Record I t -> Record I t -modifyFieldI f = modifyField @k @t (I . f . unI) - -{- | Like 'inject' but specialized to pure 'Variant's. - ->>> matchI @"foo" (injectI @"foo" 'a' :: Variant I (Insert "foo" Char Empty)) -Just 'a' - --} -injectI :: forall k t. Key k t => Value k t -> Variant I t -injectI = snd (branch @k @t) . I - -{- | Like 'match' but specialized to pure 'Variants's. --} -matchI :: forall k t . Key k t => Variant I t -> Maybe (Value k t) -matchI v = unI <$> fst (branch @k @t) v - -{- | Process a 'Variant' using a eliminator 'Record' that carries - handlers for each possible branch of the 'Variant'. - ->>> eliminate (addCaseI @"foo" @Int succ (addCaseI @"bar" pred unit)) (injectI @"bar" 33) -32 - --} -eliminate :: (Productlike '[] t result, Sumlike '[] t result, SListI result) => Record (Case f r) t -> Variant f t -> r -eliminate cases variant = - let adapt (Case e) = Fn (\fv -> K (e fv)) - in collapse_NS (ap_NS (liftA_NP adapt (toNP cases)) (toNS variant)) - -{- | Represents a handler for a branch of a 'Variant'. --} -newtype Case f a b = Case (f b -> a) - -instance Functor f => Contravariant (Case f a) where - contramap g (Case c) = Case (c . fmap g) - -{- | A form of 'addField' for creating eliminators for 'Variant's. --} -addCase :: forall k v t f a. Insertable k v t => (f v -> a) -> Record (Case f a) t -> Record (Case f a) (Insert k v t) -addCase f = addField @k @v @t (Case f) - -{- | A pure version of 'addCase'. --} -addCaseI :: forall k v t a. Insertable k v t => (v -> a) -> Record (Case I a) t -> Record (Case I a) (Insert k v t) -addCaseI f = addField @k @v @t (Case (f . unI)) - --- --- --- Subsetting - -newtype SetField f a b = SetField { getSetField :: f b -> a -> a } - --- this odd trick again... -class (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q) -instance (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q) - -{- | Constraint for maps that represent subsets of fields of 'Record'-like types. --} -type ProductlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (flat :: [q]) = - (KeysValuesAll (PresentIn whole) subset, - Productlike '[] subset flat, - SListI flat) - -{- | Like 'field', but targets multiple fields at the same time - --} -fieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) - => Record f whole -> (Record f subset -> Record f whole, Record f subset) -fieldSubset r = - (,) - (let goset :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left, - KeysValuesAll (PresentIn whole) right) - => Record (SetField f (Record f whole)) left - -> Record (SetField f (Record f whole)) right - -> Record (SetField f (Record f whole)) (N color left k v right) - goset left right = Node left (SetField (\v w -> fst (field @k @whole w) v)) right - setters = toNP @subset @_ @(SetField f (Record f whole)) (cpara_Map (Proxy @(PresentIn whole)) unit goset) - appz (SetField func) fv = K (Endo (func fv)) - in \toset -> appEndo (mconcat (collapse_NP (liftA2_NP appz setters (toNP toset)))) r) - (let goget :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left, - KeysValuesAll (PresentIn whole) right) - => Record f left - -> Record f right - -> Record f (N color left k v right) - goget left right = Node left (project @k @whole r) right - in cpara_Map (Proxy @(PresentIn whole)) unit goget) - -{- | Like 'project', but extracts multiple fields at the same time. - - The types in the subset tree can often be inferred and left as wildcards in type signature. - ->>> prettyShowRecordI $ projectSubset @(Insert "foo" _ (Insert "bar" _ Empty)) (insertI @"foo" 'a' (insertI @"bar" True (insertI @"baz" (Just ()) unit))) -"{bar = True, foo = 'a'}" - - Can also be used to convert between 'Record's with structurally dissimilar - type-level maps that nevertheless hold the same entries. --} -projectSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) - => Record f whole - -> Record f subset -projectSubset = snd . fieldSubset - -{- | Alias for 'projectSubset'. --} -getFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) - => Record f whole - -> Record f subset -getFieldSubset = projectSubset - -{- | Like 'setField', but sets multiple fields at the same time. - --} -setFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) - => Record f subset - -> Record f whole - -> Record f whole -setFieldSubset subset whole = fst (fieldSubset whole) subset - -{- | Like 'modifyField', but modifies multiple fields at the same time. - --} -modifyFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) - => (Record f subset -> Record f subset) - -> Record f whole - -> Record f whole -modifyFieldSubset f r = uncurry ($) (fmap f (fieldSubset @subset @whole r)) - - -{- | Constraint for maps that represent subsets of branches of 'Variant'-like types. --} -type SumlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (subflat :: [q]) (wholeflat :: [q]) = - (KeysValuesAll (PresentIn whole) subset, - Productlike '[] whole wholeflat, - Sumlike '[] whole wholeflat, - SListI wholeflat, - Productlike '[] subset subflat, - Sumlike '[] subset subflat, - SListI subflat) - -{- | Like 'branch', but targets multiple branches at the same time. --} -branchSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat) - => (Variant f whole -> Maybe (Variant f subset), Variant f subset -> Variant f whole) -branchSubset = - let inj2case :: forall t flat f v. Sumlike '[] t flat => (_ -> _) -> Injection _ flat v -> Case _ _ v - inj2case = \adapt -> \fn -> Case (\fv -> adapt (fromNS @t (unK (apFn fn fv)))) - -- The intuition is that getting the setter and the getter together might be faster at compile-time. - -- The intuition might be wrong. - subs :: forall f. Record f whole -> (Record f subset -> Record f whole, Record f subset) - subs = fieldSubset @subset @whole - in - (,) - (let injs :: Record (Case f (Maybe (Variant f subset))) subset - injs = fromNP @subset (liftA_NP (inj2case Just) (injections @subflat)) - wholeinjs :: Record (Case f (Maybe (Variant f subset))) whole - wholeinjs = fromNP @whole (pure_NP (Case (\_ -> Nothing))) - mixedinjs = fst (subs wholeinjs) injs - in eliminate mixedinjs) - (let wholeinjs :: Record (Case f (Variant f whole)) whole - wholeinjs = fromNP @whole (liftA_NP (inj2case id) (injections @wholeflat)) - injs = snd (subs wholeinjs) - in eliminate injs) - -{- | Like 'inject', but injects one of several possible branches. - - Can also be used to convert between 'Variant's with structurally - dissimilar type-level maps that nevertheless hold the same entries. --} -injectSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat) - => Variant f subset -> Variant f whole -injectSubset = snd (branchSubset @subset @whole @subflat @wholeflat) - -{- | Like 'match', but matches more than one branch. --} -matchSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat) - => Variant f whole -> Maybe (Variant f subset) -matchSubset = fst (branchSubset @subset @whole @subflat @wholeflat) - -{- | - Like 'eliminate', but allows the eliminator 'Record' to have more fields - than there are branches in the 'Variant'. --} -eliminateSubset :: forall subset whole subflat wholeflat f r. (SumlikeSubset subset whole subflat wholeflat) - => Record (Case f r) whole -> Variant f subset -> r -eliminateSubset cases = - let reducedCases = getFieldSubset @subset @whole cases - in eliminate reducedCases - --- - --- Interaction with Data.SOP - -{- | Class from converting 'Record's to and from the n-ary product type 'NP' from "Data.SOP". - - 'prefixNP' flattens a 'Record' and adds it to the initial part of the product. - - 'breakNP' reconstructs a 'Record' from the initial part of the product and returns the unconsumed part. - - The functions 'toNP' and 'fromNP' are usually easier to use. --} -class Productlike (start :: [k]) - (t :: Map Symbol k) - (result :: [k]) | start t -> result, result t -> start where - _prefixNP:: Record f t -> NP f start -> NP f result - _breakNP :: NP f result -> (Record f t, NP f start) - -instance Productlike start E start where - _prefixNP _ start = start - _breakNP start = (Empty, start) - -instance (Productlike start right middle, - Productlike (v ': middle) left result) - => Productlike start (N color left k v right) result where - _prefixNP (Node left fv right) start = - _prefixNP @_ @_ @left @result left (fv :* prefixNP @start @right @middle right start) - _breakNP result = - let (left, fv :* middle) = _breakNP @_ @_ @left @result result - (right, start) = _breakNP @_ @start @right middle - in (Node left fv right, start) - -{- | - Flattens a 'Record' and adds it to the initial part of the product. --} -prefixNP:: forall start t result f. Productlike start t result => Record f t -> NP f start -> NP f result -prefixNP = _prefixNP @_ @start @t @result - -{- | - Reconstructs a 'Record' from the initial part of the product and returns the unconsumed part. --} -breakNP :: forall start t result f. Productlike start t result => NP f result -> (Record f t, NP f start) -breakNP = _breakNP @_ @start @t @result - -{- | Convert a 'Record' into a n-ary product. The order of the elements in the - product is not the order of insertion in the record. - ->>> toNP (insertI @"foo" 'a' (insertI @"bar" True unit)) -I True :* I 'a' :* Nil - --} -toNP :: forall t result f. Productlike '[] t result => Record f t -> NP f result -toNP r = prefixNP r Nil - -{- | Convert a n-ary product into a compatible 'Record'. Usually follows an invocation of 'toNP'. - ->>> prettyShowRecordI . fromNP @(Insert "foo" _ (Insert "bar" _ Empty)) . toNP $ insertI @"foo" 'a' (insertI @"bar" True unit) -"{bar = True, foo = 'a'}" - --} -fromNP :: forall t result f. Productlike '[] t result => NP f result -> Record f t -fromNP np = let (r,Nil) = breakNP np in r - -{- | Class from converting 'Variant's to and from the n-ary sum type 'NS' from "Data.SOP". - - 'prefixNS' flattens a 'Variant' and adds it to the initial part of the sum. - - 'breakNS' reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part. - - The functions 'toNS' and 'fromNS' are usually easier to use. --} -class Sumlike (start :: [k]) - (t :: Map Symbol k) - (result :: [k]) | start t -> result, result t -> start where - _prefixNS :: Either (NS f start) (Variant f t) -> NS f result - _breakNS :: NS f result -> Either (NS f start) (Variant f t) - -instance Sumlike start - (N color E k v E) - (v ': start) where - _prefixNS = \case - Left l -> S l - Right x -> case x of Here fv -> Z @_ @v @start fv - _breakNS = \case - Z x -> Right (Here x) - S x -> Left x - -instance (Sumlike start (N colorR leftR kR vR rightR) middle, - Sumlike (v ': middle) (N colorL leftL kL vL rightL) result) - => Sumlike start - (N color (N colorL leftL kL vL rightL) k v (N colorR leftR kR vR rightR)) - result where - _prefixNS = \case - Left x -> - _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (S (_prefixNS @_ @_ @(N colorR leftR kR vR rightR) (Left x)))) - Right x -> - case x of LookLeft x -> _prefixNS @_ @(v ': middle) @(N colorL leftL kL vL rightL) @result (Right x) - Here x -> _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (Z x)) - LookRight x -> _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (S (_prefixNS @_ (Right x)))) - _breakNS ns = case _breakNS @_ @(v ': middle) @(N colorL leftL kL vL rightL) ns of - Left x -> case x of - Z x -> Right (Here x) - S x -> case _breakNS @_ @start @(N colorR leftR kR vR rightR) x of - Left ns -> Left ns - Right v -> Right (LookRight v) - Right v -> Right (LookLeft v) - -instance Sumlike (v ': start) (N colorL leftL kL vL rightL) result - => Sumlike start (N color (N colorL leftL kL vL rightL) k v E) result where - _prefixNS = \case - Left x -> - _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (S x)) - Right x -> - case x of LookLeft x -> _prefixNS @_ @(v ': start) @(N colorL leftL kL vL rightL) @result (Right x) - Here x -> _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (Z x)) - _breakNS ns = case _breakNS @_ @(v ': start) @(N colorL leftL kL vL rightL) ns of - Left x -> case x of - Z x -> Right (Here x) - S x -> Left x - Right v -> Right (LookLeft v) - -instance Sumlike start (N colorR leftR kR vR rightR) middle - => Sumlike start (N color E k v (N colorR leftR kR vR rightR)) (v ': middle) where - _prefixNS = \case - Left x -> S (_prefixNS @_ @_ @(N colorR leftR kR vR rightR) (Left x)) - Right x -> - case x of Here x -> Z x - LookRight x -> S (_prefixNS @_ @_ @(N colorR leftR kR vR rightR) (Right x)) - _breakNS = \case - Z x -> Right (Here x) - S x -> case _breakNS @_ @_ @(N colorR leftR kR vR rightR) x of - Left ns -> Left ns - Right v -> Right (LookRight v) - -{- | - - Flattens a 'Variant' and adds it to the initial part of the sum. --} -prefixNS :: forall start t result f. Sumlike start t result => Either (NS f start) (Variant f t) -> NS f result -prefixNS = _prefixNS @_ @start @t @result - -{- | - Reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part. --} -breakNS :: forall start t result f. Sumlike start t result => NS f result -> Either (NS f start) (Variant f t) -breakNS = _breakNS @_ @start @t @result - -{- | Convert a 'Variant' into a n-ary sum. - ->>> toNS (injectI @"foo" 'a' :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) -S (Z (I 'a')) - --} -toNS :: forall t result f. Sumlike '[] t result => Variant f t -> NS f result -toNS = prefixNS . Right - -{- | Convert a n-ary sum into a compatible 'Variant'. - ->>> prettyShowVariantI $ fromNS @(Insert "foo" _ (Insert "bar" _ Empty)) . toNS $ (injectI @"foo" 'a' :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) -"foo ('a')" - --} -fromNS :: forall t result f. Sumlike '[] t result => NS f result -> Variant f t -fromNS ns = case breakNS ns of - Left _ -> error "this never happens" - Right x -> x - --- --- --- Interfacing with normal records - -class ToRecord (r :: Type) where - type RecordCode r :: Map Symbol Type - -- https://stackoverflow.com/questions/22087549/defaultsignatures-and-associated-type-families/22088808 - type RecordCode r = RecordCode' E (G.Rep r) - toRecord :: r -> Record I (RecordCode r) - default toRecord :: (G.Generic r,ToRecordHelper E (G.Rep r),RecordCode r ~ RecordCode' E (G.Rep r)) => r -> Record I (RecordCode r) - toRecord r = toRecord' unit (G.from r) - -class ToRecordHelper (start :: Map Symbol Type) (g :: Type -> Type) where - type RecordCode' start g :: Map Symbol Type - toRecord' :: Record I start -> g x -> Record I (RecordCode' start g) - -instance ToRecordHelper E fields => ToRecordHelper E (D1 meta (C1 metacons fields)) where - type RecordCode' E (D1 meta (C1 metacons fields)) = RecordCode' E fields - toRecord' r (M1 (M1 g)) = toRecord' @E @fields r g - -instance (Insertable k v start) => - ToRecordHelper start - (S1 ('G.MetaSel ('Just k) - unpackedness - strictness - laziness) - (Rec0 v)) - where - type RecordCode' start - (S1 ('G.MetaSel ('Just k) - unpackedness - strictness - laziness) - (Rec0 v)) = Insert k v start - toRecord' start (M1 (K1 v)) = insertI @k v start - -instance ( ToRecordHelper start t2, - RecordCode' start t2 ~ middle, - ToRecordHelper middle t1 - ) => - ToRecordHelper start (t1 G.:*: t2) - where - type RecordCode' start (t1 G.:*: t2) = RecordCode' (RecordCode' start t2) t1 - toRecord' start (t1 G.:*: t2) = toRecord' @middle (toRecord' @start start t2) t1 - --- --- -class ToRecord r => FromRecord (r :: Type) where - fromRecord :: Record I (RecordCode r) -> r - default fromRecord :: (G.Generic r, FromRecordHelper (RecordCode r) (G.Rep r)) => Record I (RecordCode r) -> r - fromRecord r = G.to (fromRecord' @(RecordCode r) @(G.Rep r) r) - -class FromRecordHelper (t :: Map Symbol Type) (g :: Type -> Type) where - fromRecord' :: Record I t -> g x - -instance FromRecordHelper t fields => FromRecordHelper t (D1 meta (C1 metacons fields)) where - fromRecord' r = M1 (M1 (fromRecord' @t @fields r)) - -instance (Key k t, Value k t ~ v) => - FromRecordHelper t - (S1 ('G.MetaSel ('Just k) - unpackedness - strictness - laziness) - (Rec0 v)) - where - fromRecord' r = let v = projectI @k r in M1 (K1 v) - -instance ( FromRecordHelper t t1, - FromRecordHelper t t2 - ) => - FromRecordHelper t (t1 G.:*: t2) - where - fromRecord' r = - let v1 = fromRecord' @_ @t1 r - v2 = fromRecord' @_ @t2 r - in v1 G.:*: v2 - --- --- --- -type family VariantCode (s :: Type) :: Map Symbol Type where - VariantCode s = VariantCode' E (G.Rep s) - -type family VariantCode' (acc :: Map Symbol Type) (g :: Type -> Type) :: Map Symbol Type where - VariantCode' acc (D1 meta fields) = VariantCode' acc fields - VariantCode' acc (t1 G.:+: t2) = VariantCode' (VariantCode' acc t2) t1 - VariantCode' acc (C1 (G.MetaCons k _ _) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v))) = Insert k v acc - VariantCode' acc (C1 (G.MetaCons k _ _) G.U1) = Insert k () acc - -class FromVariant (s :: Type) where - fromVariant :: Variant I (VariantCode s) -> s - default fromVariant :: (G.Generic s, FromVariantHelper (VariantCode s) (G.Rep s)) => Variant I (VariantCode s) -> s - fromVariant v = case fromVariant' @(VariantCode s) v of - Just x -> G.to x - Nothing -> error "fromVariant match fail. Should not happen." - -class FromVariantHelper (t :: Map Symbol Type) (g :: Type -> Type) where - fromVariant' :: Variant I t -> Maybe (g x) - -instance FromVariantHelper t fields => FromVariantHelper t (D1 meta fields) where - fromVariant' v = M1 <$> fromVariant' @t v - -instance (Key k t, Value k t ~ v) - => FromVariantHelper t (C1 (G.MetaCons k x y) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v))) - where - fromVariant' v = case matchI @k @t v of - Just x -> Just (M1 (M1 (K1 x)) ) - Nothing -> Nothing - -instance (Key k t, Value k t ~ ()) - => FromVariantHelper t (C1 (G.MetaCons k x y) G.U1) - where - fromVariant' v = case matchI @k @t v of - Just x -> Just (M1 G.U1) - Nothing -> Nothing - -instance ( FromVariantHelper t t1, - FromVariantHelper t t2 - ) => - FromVariantHelper t (t1 G.:+: t2) - where - fromVariant' v = case fromVariant' @t @t1 v of - Just x1 -> Just (G.L1 x1) - Nothing -> case fromVariant' @t @t2 v of - Just x2 -> Just (G.R1 x2) - Nothing -> Nothing - --- --- -class ToVariant (s :: Type) where - toVariant :: s -> Variant I (VariantCode s) - default toVariant :: (G.Generic s, ToVariantHelper (VariantCode s) (G.Rep s)) => s -> Variant I (VariantCode s) - toVariant s = toVariant' @(VariantCode s) @(G.Rep s) (G.from s) - -class ToVariantHelper (t :: Map Symbol Type) (g :: Type -> Type) where - toVariant' :: g x -> Variant I t - -instance ToVariantHelper t fields => ToVariantHelper t (D1 meta fields) where - toVariant' (M1 fields) = toVariant' @t fields - -instance (Key k t, Value k t ~ v) => - ToVariantHelper t (C1 (G.MetaCons k x y) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v))) - where - toVariant' (M1 (M1 (K1 v))) = injectI @k v - -instance (Key k t, Value k t ~ ()) => - ToVariantHelper t (C1 (G.MetaCons k x y) G.U1) where - toVariant' (M1 G.U1) = injectI @k () - -instance ( ToVariantHelper t t1, - ToVariantHelper t t2 - ) => - ToVariantHelper t (t1 G.:+: t2) - where - toVariant' = \case - G.L1 l -> toVariant' @t l - G.R1 r -> toVariant' @t r - --- --- --- deletion --- --- --- - -type family DiscriminateBalL (l :: Map k v) (r :: Map k v) :: Bool where - DiscriminateBalL (N R _ _ _ _) _ = False - DiscriminateBalL _ _ = True - -class BalanceableL (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where - type BalL l k v r :: Map Symbol q - balLR :: Record f (N color l k v r) -> Record f (BalL l k v r) - balLV :: Variant f (N color l k v r) -> Variant f (BalL l k v r) - -class BalanceableHelperL (b :: Bool) (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where - type BalL' b l k v r :: Map Symbol q - balLR' :: Record f (N color l k v r) -> Record f (BalL' b l k v r) - balLV' :: Variant f (N color l k v r) -> Variant f (BalL' b l k v r) - -instance (DiscriminateBalL l r ~ b, BalanceableHelperL b l k v r) => BalanceableL l k v r where - type BalL l k v r = BalL' (DiscriminateBalL l r) l k v r - balLR = balLR' @_ @b @l @k @v @r - balLV = balLV' @_ @b @l @k @v @r - --- balleft :: RB a -> a -> RB a -> RB a --- balleft (T R a x b) y c = T R (T B a x b) y c -instance BalanceableHelperL False (N R left1 k1 v1 right1) k2 v2 right2 where - type BalL' False (N R left1 k1 v1 right1) k2 v2 right2 = - (N R (N B left1 k1 v1 right1) k2 v2 right2) - balLR' (Node (Node left' v' right') v right) = Node (Node left' v' right') v right - balLV' v = case v of LookLeft x -> LookLeft (case x of LookLeft y -> LookLeft y - Here y -> Here y - LookRight y -> LookRight y) - Here x -> Here x - LookRight x -> LookRight x - --- balleft bl x (T B a y b) = balance bl x (T R a y b) --- the @(N B in the call to balance tree is misleading, as it is ingored... -instance (N R t2 z zv t3 ~ g, BalanceableHelper (ShouldBalance t1 g) t1 y yv g) => - BalanceableHelperL True t1 y yv (N B t2 z zv t3) where - type BalL' True t1 y yv (N B t2 z zv t3) - = Balance t1 y yv (N R t2 z zv t3) - balLR' (Node left1 v1 (Node left2 v2 right2)) = - balanceR @_ @t1 @y @yv @(N R t2 z zv t3) (Node left1 v1 (Node left2 v2 right2)) - balLV' v = balanceV @_ @t1 @y @yv @(N R t2 z zv t3) (case v of - LookLeft l -> LookLeft l - Here x -> Here x - LookRight r -> LookRight (case r of - LookLeft l' -> LookLeft l' - Here x' -> Here x' - LookRight r' -> LookRight r')) - --- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c)) -instance (N R l k kv r ~ g, BalanceableHelper (ShouldBalance t3 g) t3 z zv g) => - BalanceableHelperL True t1 y yv (N R (N B t2 u uv t3) z zv (N B l k kv r)) where - type BalL' True t1 y yv (N R (N B t2 u uv t3) z zv (N B l k kv r)) = - N R (N B t1 y yv t2) u uv (Balance t3 z zv (N R l k kv r)) - balLR' (Node left1 v1 (Node (Node left2 v2 right2) vx (Node left3 v3 right3))) = - Node (Node left1 v1 left2) v2 (balanceR @_ @t3 @z @zv @(N R l k kv r) (Node right2 vx (Node left3 v3 right3))) - balLV' v = case v of LookLeft left1 -> LookLeft (LookLeft left1) - Here v1 -> LookLeft (Here v1) - LookRight (LookLeft (LookLeft left2)) -> LookLeft (LookRight left2) - LookRight (LookLeft (Here v2)) -> Here v2 - LookRight (LookLeft (LookRight right2)) -> LookRight (balanceV @_ @t3 @z @zv @(N R l k kv r) (LookLeft right2)) - LookRight (Here vx) -> LookRight (balanceV @_ @t3 @z @zv @(N R l k kv r) (Here vx)) - LookRight (LookRight rr) -> LookRight (balanceV @_ @t3 @z @zv @(N R l k kv r) (LookRight (case rr of - LookLeft left3 -> LookLeft left3 - Here v3 -> Here v3 - LookRight right3 -> LookRight right3))) - - --- balright :: RB a -> a -> RB a -> RB a --- balright a x (T R b y c) = T R a x (T B b y c) --- balright (T B a x b) y bl = balance (T R a x b) y bl --- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) -type family DiscriminateBalR (l :: Map k v) (r :: Map k v) :: Bool where - DiscriminateBalR _ (N R _ _ _ _) = False - DiscriminateBalR _ _ = True - -class BalanceableR (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where - type BalR l k v r :: Map Symbol q - balRR :: Record f (N color l k v r) -> Record f (BalR l k v r) - balRV :: Variant f (N color l k v r) -> Variant f (BalR l k v r) - -class BalanceableHelperR (b :: Bool) (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where - type BalR' b l k v r :: Map Symbol q - balRR' :: Record f (N color l k v r) -> Record f (BalR' b l k v r) - balRV' :: Variant f (N color l k v r) -> Variant f (BalR' b l k v r) - -instance (DiscriminateBalR l r ~ b, BalanceableHelperR b l k v r) => BalanceableR l k v r where - type BalR l k v r = BalR' (DiscriminateBalR l r) l k v r - balRR = balRR' @_ @b @l @k @v @r - balRV = balRV' @_ @b @l @k @v @r - --- balright :: RB a -> a -> RB a -> RB a --- balright a x (T R b y c) = T R a x (T B b y c) -instance BalanceableHelperR False right2 k2 v2 (N R left1 k1 v1 right1) where - type BalR' False right2 k2 v2 (N R left1 k1 v1 right1) = - (N R right2 k2 v2 (N B left1 k1 v1 right1)) - balRR' (Node right v (Node left' v' right')) = Node right v (Node left' v' right') - balRV' v = case v of LookLeft x -> LookLeft x - Here x -> Here x - LookRight x -> LookRight (case x of LookLeft y -> LookLeft y - Here y -> Here y - LookRight y -> LookRight y) - --- balright (T B a x b) y bl = balance (T R a x b) y bl -instance (N R t2 z zv t3 ~ g, ShouldBalance g t1 ~ shouldbalance, BalanceableHelper shouldbalance g y yv t1) => - BalanceableHelperR True (N B t2 z zv t3) y yv t1 where - type BalR' True (N B t2 z zv t3) y yv t1 - = Balance (N R t2 z zv t3) y yv t1 - balRR' (Node (Node left1 v1 right1) v2 right2) = balanceR @_ @(N R t2 z zv t3) @y @yv @t1 - (Node (Node left1 v1 right1) v2 right2) - balRV' v = balanceV @_ @(N R t2 z zv t3) @y @yv @t1 (case v of - LookLeft l -> LookLeft (case l of - LookLeft l' -> LookLeft l' - Here x' -> Here x' - LookRight r' -> LookRight r') - Here x -> Here x - LookRight r -> LookRight r) - --- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) -instance (N R t2 u uv t3 ~ g, ShouldBalance g l ~ shouldbalance, BalanceableHelper shouldbalance g z zv l) => - BalanceableHelperR True (N R (N B t2 u uv t3) z zv (N B l k kv r)) y yv t1 where - type BalR' True (N R (N B t2 u uv t3) z zv (N B l k kv r)) y yv t1 = - N R (Balance (N R t2 u uv t3) z zv l) k kv (N B r y yv t1) - balRR' (Node (Node (Node left2 v2 right2) vx (Node left3 v3 right3)) v1 left1) = - Node (balanceR @_ @(N R t2 u uv t3) @z @zv @l (Node (Node left2 v2 right2) vx left3)) v3 (Node right3 v1 left1) - balRV' v = case v of - LookLeft (LookLeft rr) -> LookLeft (balanceV @_ @(N R t2 u uv t3) @z @zv @l (LookLeft (case rr of - LookLeft t2 -> LookLeft t2 - Here uv -> Here uv - LookRight t3 -> LookRight t3))) - LookLeft (Here zv) -> LookLeft (balanceV @_ @(N R t2 u uv t3) @z @zv @l (Here zv)) - LookLeft (LookRight (LookLeft l)) -> LookLeft (balanceV @_ @(N R t2 u uv t3) @z @zv @l (LookRight l)) - LookLeft (LookRight (Here kv)) -> Here kv - LookLeft (LookRight (LookRight r)) -> LookRight (LookLeft r) - Here yv -> LookRight (Here yv) - LookRight t1 -> LookRight (LookRight t1) - --- app :: RB a -> RB a -> RB a --- app E x = x --- app x E = x --- app (T R a x b) (T R c y d) = --- case app b c of --- T R b' z c' -> T R(T R a x b') z (T R c' y d) --- bc -> T R a x (T R bc y d) --- app (T B a x b) (T B c y d) = --- case app b c of --- T R b' z c' -> T R(T B a x b') z (T B c' y d) --- bc -> balleft a x (T B bc y d) --- app a (T R b x c) = T R (app a b) x c --- app (T R a x b) c = T R a x (app b c) - - -class Fuseable (l :: Map Symbol q) (r :: Map Symbol q) where - type Fuse l r :: Map Symbol q - fuseRecord :: Record f l -> Record f r -> Record f (Fuse l r) - fuseVariant :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r) - -instance Fuseable E E where - type Fuse E E = E - fuseRecord _ _ = unit - fuseVariant v = case v of - --- app E x = x -instance Fuseable E (N color left k v right) where - type Fuse E (N color left k v right) = N color left k v right - fuseRecord _ r = r - fuseVariant e = case e of - Right v -> v - --- app x E = x -instance Fuseable (N color left k v right) E where - type Fuse (N color left k v right) E = N color left k v right - fuseRecord r _ = r - fuseVariant e = case e of - Left v -> v - --- app a (T R b x c) = T R (app a b) x c -instance Fuseable (N B left1 k1 v1 right1) left2 - => Fuseable (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) where - type Fuse (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R (Fuse (N B left1 k1 v1 right1) left2) k2 v2 right2 - fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node (fuseRecord @_ @(N B left1 k1 v1 right1) (Node left1 v1 right1) left2) v2 right2 - fuseVariant e = case e of - Left l -> case l of - LookLeft left1 -> LookLeft (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Left (LookLeft left1))) - Here v1 -> LookLeft (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Left (Here v1))) - LookRight right1 -> LookLeft (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Left (LookRight right1))) - Right r -> case r of - LookLeft left2 -> LookLeft (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Right left2)) - Here v2 -> Here v2 - LookRight right2 -> LookRight right2 - - --- app (T R a x b) c = T R a x (app b c) -instance Fuseable right1 (N B left2 k2 v2 right2) - => Fuseable (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) where - type Fuse (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) = N R left1 k1 v1 (Fuse right1 (N B left2 k2 v2 right2)) - fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (fuseRecord @_ @_ @(N B left2 k2 v2 right2) right1 (Node left2 v2 right2)) - fuseVariant e = case e of - Left l -> case l of - LookLeft left1 -> LookLeft left1 - Here v1 -> Here v1 - LookRight right1 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Left right1)) - Right r -> case r of - LookLeft left2 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Right (LookLeft left2))) - Here v2 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Right (Here v2))) - LookRight right2 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Right (LookRight right2))) - - --- app (T R a x b) (T R c y d) = -instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper1 fused (N R left1 k1 v1 right1) (N R left2 k2 v2 right2)) - => Fuseable (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where - type Fuse (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = Fuse1 (Fuse right1 left2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) - fuseRecord = fuseRecord1 @_ @(Fuse right1 left2) - fuseVariant = fuseVariant1 @_ @(Fuse right1 left2) - -class FuseableHelper1 (fused :: Map Symbol q) (l :: Map Symbol q) (r :: Map Symbol q) where - type Fuse1 fused l r :: Map Symbol q - fuseRecord1 :: Record f l -> Record f r -> Record f (Fuse l r) - fuseVariant1 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r) - --- app (T R a x b) (T R c y d) = --- case app b c of --- T R b' z c' -> T R (T R a x b') z (T R c' y d) --- FIXME: The Fuseable constraint is repeated from avobe :( -instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z zv s2) - => FuseableHelper1 (N R s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where - type Fuse1 (N R s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R (N R left1 k1 v1 s1) z zv (N R s2 k2 v2 right2) - fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) = - case fuseRecord right1 left2 of - Node s1 zv s2 -> Node (Node left1 v1 s1) zv (Node s2 v2 right2) - fuseVariant1 e = - case e of - Left l -> case l of - LookLeft left1 -> LookLeft (LookLeft left1) - Here v1 -> LookLeft (Here v1) - LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of - LookLeft s1 -> LookLeft (LookRight s1) - Here zv -> Here zv - LookRight s2 -> LookRight (LookLeft s2) - Right r -> case r of - LookLeft left2 -> case fuseVariant @_ @right1 @left2 (Right left2) of - LookLeft s1 -> LookLeft (LookRight s1) - Here zv -> Here zv - LookRight s2 -> LookRight (LookLeft s2) - Here v2 -> LookRight (Here v2) - LookRight right2 -> LookRight (LookRight right2) - - --- app (T R a x b) (T R c y d) = --- case app b c of --- ... --- bc -> T R a x (T R bc y d) --- FIXME: The Fuseable constraint is repeated from above :( -instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z zv s2) - => FuseableHelper1 (N B s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where - type Fuse1 (N B s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R left1 k1 v1 (N R (N B s1 z zv s2) k2 v2 right2) - fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) = - case fuseRecord right1 left2 of - Node s1 zv s2 -> Node left1 v1 (Node (Node s1 zv s2) v2 right2) - fuseVariant1 e = - case e of - Left l -> case l of - LookLeft left1 -> LookLeft left1 - Here v1 -> Here v1 - LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of - LookLeft s1 -> LookRight (LookLeft (LookLeft s1)) - Here zv -> LookRight (LookLeft (Here zv)) - LookRight s2 -> LookRight (LookLeft (LookRight s2)) - Right r -> case r of - LookLeft left2 -> case fuseVariant @_ @right1 @left2 (Right left2) of - LookLeft s1 -> LookRight (LookLeft (LookLeft s1)) - Here zv -> LookRight (LookLeft (Here zv)) - LookRight s2 -> LookRight (LookLeft (LookRight s2)) - Here v2 -> LookRight (Here v2) - LookRight right2 -> LookRight (LookRight right2) - --- app (T R a x b) (T R c y d) = --- case app b c of --- ... --- bc -> T R a x (T R bc y d) -instance FuseableHelper1 E (N R left1 k1 v1 E) (N R E k2 v2 right2) where - type Fuse1 E (N R left1 k1 v1 E) (N R E k2 v2 right2) = N R left1 k1 v1 (N R E k2 v2 right2) - fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (Node Empty v2 right2) - fuseVariant1 e = - case e of - Left l -> case l of - LookLeft left1 -> LookLeft left1 - Here v1 -> Here v1 - Right r -> case r of - Here v2 -> LookRight (Here v2) - LookRight right2 -> LookRight (LookRight right2) - --- app (T B a x b) (T B c y d) = -instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper2 fused (N B left1 k1 v1 right1) (N B left2 k2 v2 right2)) - => Fuseable (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where - type Fuse (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = Fuse2 (Fuse right1 left2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) - fuseRecord = fuseRecord2 @_ @(Fuse right1 left2) - fuseVariant = fuseVariant2 @_ @(Fuse right1 left2) - --- could FuseableHelper1 and FuseableHelper2 be, well... fused? -class FuseableHelper2 (fused :: Map Symbol q) (l :: Map Symbol q) (r :: Map Symbol q) where - type Fuse2 fused l r :: Map Symbol q - fuseRecord2 :: Record f l -> Record f r -> Record f (Fuse l r) - fuseVariant2 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r) - --- app (T B a x b) (T B c y d) = --- case app b c of --- T R b' z c' -> T R (T B a x b') z (T B c' y d) -instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z zv s2) - => FuseableHelper2 (N R s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where - type Fuse2 (N R s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = N R (N B left1 k1 v1 s1) z zv (N B s2 k2 v2 right2) - fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) = - case fuseRecord right1 left2 of - Node s1 zv s2 -> Node (Node left1 v1 s1) zv (Node s2 v2 right2) - fuseVariant2 e = - case e of - Left l -> case l of - LookLeft left1 -> LookLeft (LookLeft left1) - Here v1 -> LookLeft (Here v1) - LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of - LookLeft s1 -> LookLeft (LookRight s1) - Here zv -> Here zv - LookRight s2 -> LookRight (LookLeft s2) - Right r -> case r of - LookLeft left2 -> case fuseVariant @_ @right1 @left2 (Right left2) of - LookLeft s1 -> LookLeft (LookRight s1) - Here zv -> Here zv - LookRight s2 -> LookRight (LookLeft s2) - Here v2 -> LookRight (Here v2) - LookRight right2 -> LookRight (LookRight right2) - --- app (T B a x b) (T B c y d) = --- case app b c of --- ... --- bc -> balleft a x (T B bc y d) -instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z zv s2, BalanceableL left1 k1 v1 (N B (N B s1 z zv s2) k2 v2 right2)) - => FuseableHelper2 (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where - type Fuse2 (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = BalL left1 k1 v1 (N B (N B s1 z zv s2) k2 v2 right2) - fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) = - case fuseRecord @_ @right1 @left2 right1 left2 of - Node s1 zv s2 -> balLR @_ @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (Node left1 v1 (Node (Node s1 zv s2) v2 right2)) - fuseVariant2 e = balLV @_ @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (case e of - Left l -> case l of - LookLeft left1 -> LookLeft left1 - Here v1 -> Here v1 - LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of - LookLeft s1 -> LookRight (LookLeft (LookLeft s1)) - Here zv -> LookRight (LookLeft (Here zv)) - LookRight s2 -> LookRight (LookLeft (LookRight s2)) - Right r -> case r of - LookLeft left2 -> case fuseVariant @_ @right1 @left2 (Right left2) of - LookLeft s1 -> LookRight (LookLeft (LookLeft s1)) - Here zv -> LookRight (LookLeft (Here zv)) - LookRight s2 -> LookRight (LookLeft (LookRight s2)) - Here v2 -> LookRight (Here v2) - LookRight right2 -> LookRight (LookRight right2)) - --- app (T B a x b) (T B c y d) = --- case app b c of --- ... --- bc -> balleft a x (T B bc y d) -instance (BalanceableL left1 k1 v1 (N B E k2 v2 right2)) - => FuseableHelper2 E (N B left1 k1 v1 E) (N B E k2 v2 right2) where - type Fuse2 E (N B left1 k1 v1 E) (N B E k2 v2 right2) = BalL left1 k1 v1 (N B E k2 v2 right2) - fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) = - balLR @_ @left1 @k1 @v1 @(N B E k2 v2 right2) (Node left1 v1 (Node Empty v2 right2)) - fuseVariant2 e = balLV @_ @left1 @k1 @v1 @(N B E k2 v2 right2) (case e of - Left l -> case l of - LookLeft left1 -> LookLeft left1 - Here v1 -> Here v1 - Right r -> case r of - Here v2 -> LookRight (Here v2) - LookRight right2 -> LookRight (LookRight right2)) - - --- del E = E --- del (T _ a y b) --- | xy = delformRight a y b --- | otherwise = app a b -class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where - type Del k v t :: Map Symbol q - del :: Record f t -> Record f (Del k v t) - win :: Variant f t -> Either (Variant f (Del k v t)) (f v) - --- delformLeft a@(T B _ _ _) y b = balleft (del a) y b --- delformLeft a y b = T R (del a) y b --- In the term-level code, the k to delete is already on the environment. -class DelableL (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where - type DelL k v l kx vx r :: Map Symbol q - delL :: Record f (N color l kx vx r) -> Record f (DelL k v l kx vx r) - winL :: Variant f (N color l kx vx r) -> Either (Variant f (DelL k v l kx vx r)) (f v) - --- delformLeft a@(T B _ _ _) y b = balleft (del a) y b -instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableL deleted kx vx right) - => DelableL k v (N B leftz kz vz rightz) kx vx right where - type DelL k v (N B leftz kz vz rightz) kx vx right = BalL (Del k v (N B leftz kz vz rightz)) kx vx right - delL (Node left vx right) = balLR @_ @(Del k v (N B leftz kz vz rightz)) @kx @vx @right (Node (del @_ @k @v left) vx right) - winL v = first (balLV @_ @(Del k v (N B leftz kz vz rightz)) @kx @vx @right) (case v of - LookLeft l -> first LookLeft (win @_ @k @v l) - Here vx -> Left $ Here vx - LookRight r -> Left $ LookRight r) - --- delformLeft a y b = T R (del a) y b -instance (Delable k v (N R leftz kz vz rightz)) - => DelableL k v (N R leftz kz vz rightz) kx vx right where - type DelL k v (N R leftz kz vz rightz) kx vx right = N R (Del k v (N R leftz kz vz rightz)) kx vx right - delL (Node left vx right) = Node (del @_ @k @v left) vx right - winL v = case v of - LookLeft l -> first LookLeft (win @_ @k @v l) - Here vx -> Left (Here vx) - LookRight r -> Left (LookRight r) - --- delformLeft a y b = T R (del a) y b -instance DelableL k v E kx vx right where - type DelL k v E kx vx right = N R E kx vx right - delL (Node left vx right) = Node Empty vx right - winL v = case v of - Here vx -> Left (Here vx) - LookRight r -> Left (LookRight r) - --- delformRight a y b@(T B _ _ _) = balright a y (del b) --- delformRight a y b = T R a y (del b) -class DelableR (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where - type DelR k v l kx vx r :: Map Symbol q - delR :: Record f (N color l kx vx r) -> Record f (DelR k v l kx vx r) - winR :: Variant f (N color l kx vx r) -> Either (Variant f (DelR k v l kx vx r)) (f v) - --- delformRight a y b@(T B _ _ _) = balright a y (del b) -instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableR left kx vx deleted) - => DelableR k v left kx vx (N B leftz kz vz rightz) where - type DelR k v left kx vx (N B leftz kz vz rightz) = BalR left kx vx (Del k v (N B leftz kz vz rightz)) - delR (Node left vx right) = balRR @_ @left @kx @vx @(Del k v (N B leftz kz vz rightz)) (Node left vx (del @_ @k @v right)) - winR v = first (balRV @_ @left @kx @vx @(Del k v (N B leftz kz vz rightz))) (case v of - LookLeft l -> Left $ LookLeft l - Here vx -> Left $ Here vx - LookRight r -> first LookRight (win @_ @k @v r)) - --- delformRight a y b = T R a y (del b) -instance (Delable k v (N R leftz kz vz rightz)) - => DelableR k v left kx vx (N R leftz kz vz rightz) where - type DelR k v left kx vx (N R leftz kz vz rightz) = N R left kx vx (Del k v (N R leftz kz vz rightz)) - delR (Node left vx right) = Node left vx (del @_ @k @v right) - winR v = case v of - LookLeft l -> Left (LookLeft l) - Here vx -> Left (Here vx) - LookRight r -> first LookRight (win @_ @k @v r) - --- delformRight a y b = T R a y (del b) -instance DelableR k v left kx vx E where - type DelR k v left kx vx E = N R left kx vx E - delR (Node left vx right) = Node left vx Empty - winR v = case v of - LookLeft l -> Left (LookLeft l) - Here vx -> Left (Here vx) - --- del E = E -instance Delable k v E where - type Del k v E = E - del _ = unit - win = impossible - --- the color is discarded --- del (T _ a y b) --- | xy = delformRight a y b --- | otherwise = app a b -instance (CmpSymbol kx k ~ ordering, DelableHelper ordering k v left kx vx right) => Delable k v (N color left kx vx right) where - type Del k v (N color left kx vx right) = Del' (CmpSymbol kx k) k v left kx vx right - del = del' @_ @(CmpSymbol kx k) @k @v @left @kx @vx @right - win = win' @_ @(CmpSymbol kx k) @k @v @left @kx @vx @right - -class DelableHelper (ordering :: Ordering) (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where - type Del' ordering k v l kx vx r :: Map Symbol q - del' :: Record f (N color l kx vx r) -> Record f (Del' ordering k v l kx vx r) - win' :: Variant f (N color l kx vx r) -> Either (Variant f (Del' ordering k v l kx vx r)) (f v) - --- | x DelableHelper GT k v left kx vx right where - type Del' GT k v left kx vx right = DelL k v left kx vx right - del' = delL @_ @k @v @left @kx @vx @right - win' = winL @_ @k @v @left @kx @vx @right - --- | otherwise = app a b -instance Fuseable left right => DelableHelper EQ k v left k v right where - type Del' EQ k v left k v right = Fuse left right - del' (Node left _ right) = fuseRecord @_ @left @right left right - win' v = case v of - LookLeft l -> Left $ fuseVariant @_ @left @right (Left l) - Here v -> Right v - LookRight r -> Left $ fuseVariant @_ @left @right (Right r) - --- | x>y = delformRight a y b -instance DelableR k v left kx vx right => DelableHelper LT k v left kx vx right where - type Del' LT k v left kx vx right = DelR k v left kx vx right - del' = delR @_ @k @v @left @kx @vx @right - win' = winR @_ @k @v @left @kx @vx @right - -{- | Class that determines if the pair of a 'Symbol' key and a type can - be deleted from a type-level map. - - The associated type family 'Delete' produces the resulting map. - - At the term level, this manifests in 'delete', which removes a field from - a record, and in 'winnow', which checks if a 'Variant' is of a given - branch and returns the value in the branch if there's a match, or a - reduced 'Variant' if there isn't. 'winnow' tends to be more useful in - practice. - - If the map already has the key but with a /different/ type, the deletion - fails to compile. - -} -class Deletable (k :: Symbol) (v :: q) (t :: Map Symbol q) where - type Delete k v t :: Map Symbol q - _delete :: Record f t -> Record f (Delete k v t) - _winnow :: Variant f t -> Either (Variant f (Delete k v t)) (f v) - -instance (Delable k v t, Del k v t ~ deleted, CanMakeBlack deleted) => Deletable k v t where - type Delete k v t = MakeBlack (Del k v t) - _delete r = makeBlackR (del @_ @k @v r) - _winnow v = first makeBlackV (win @_ @k @v v) - -{- | - Removes a field from a 'Record'. - -} -delete :: forall k v t f . Deletable k v t => Record f t -> Record f (Delete k v t) -delete = _delete @_ @k @v @t - -{- | - Checks if a 'Variant' is of a given branch and returns the value in the - branch if there's a match, or a reduced 'Variant' if there isn't. - -} -winnow :: forall k v t f . Deletable k v t => Variant f t -> Either (Variant f (Delete k v t)) (f v) -winnow = _winnow @_ @k @v @t - -{- | Like 'winnow' but specialized to pure 'Variant's. - ->>> winnow @"bar" @Bool (injectI @"bar" False :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) -Right (I False) - ->>> prettyShowVariantI `first` winnow @"foo" @Char (injectI @"bar" False :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) -Left "bar (False)" - --} -winnowI :: forall k v t . Deletable k v t => Variant I t -> Either (Variant I (Delete k v t)) v -winnowI = fmap unI . winnow @k @v @t - --- The original term-level code, taken from: --- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html --- --- {- Version 1, 'untyped' -} --- data Color = R | B deriving Show --- data RB a = E | T Color (RB a) a (RB a) deriving Show --- --- {- Insertion and membership test as by Okasaki -} --- insert :: Ord a => a -> RB a -> RB a --- insert x s = --- T B a z b --- where --- T _ a z b = ins s --- ins E = T R E x E --- ins s@(T B a y b) --- | xy = balance a y (ins b) --- | otherwise = s --- ins s@(T R a y b) --- | xy = T R a y (ins b) --- | otherwise = s --- --- --- {- balance: first equation is new, --- to make it work with a weaker invariant -} --- balance :: RB a -> a -> RB a -> RB a --- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d) --- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) --- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) --- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) --- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) --- balance a x b = T B a x b --- --- member :: Ord a => a -> RB a -> Bool --- member x E = False --- member x (T _ a y b) --- | xy = member x b --- | otherwise = True --- --- {- deletion a la SMK -} --- delete :: Ord a => a -> RB a -> RB a --- delete x t = --- case del t of {T _ a y b -> T B a y b; _ -> E} --- where --- del E = E --- del (T _ a y b) --- | xy = delformRight a y b --- | otherwise = app a b --- delformLeft a@(T B _ _ _) y b = balleft (del a) y b --- delformLeft a y b = T R (del a) y b --- --- delformRight a y b@(T B _ _ _) = balright a y (del b) --- delformRight a y b = T R a y (del b) --- --- balleft :: RB a -> a -> RB a -> RB a --- balleft (T R a x b) y c = T R (T B a x b) y c --- balleft bl x (T B a y b) = balance bl x (T R a y b) --- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c)) --- --- balright :: RB a -> a -> RB a -> RB a --- balright a x (T R b y c) = T R a x (T B b y c) --- balright (T B a x b) y bl = balance (T R a x b) y bl --- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) --- --- sub1 :: RB a -> RB a --- sub1 (T B a x b) = T R a x b --- sub1 _ = error "invariance violation" --- --- app :: RB a -> RB a -> RB a --- app E x = x --- app x E = x --- app (T R a x b) (T R c y d) = --- case app b c of --- T R b' z c' -> T R (T R a x b') z (T R c' y d) --- bc -> T R a x (T R bc y d) --- app (T B a x b) (T B c y d) = --- case app b c of --- T R b' z c' -> T R(T B a x b') z (T B c' y d) --- bc -> balleft a x (T B bc y d) --- app a (T R b x c) = T R (app a b) x c --- app (T R a x b) c = T R a x (app b c) - +-- | See for +-- the original term-level code by Stefan Kahrs. It is also copied at the end +-- of this file. Some parts of the type-level code include the correspondign +-- term-level parts in their comments. +{-# LANGUAGE DataKinds, + TypeOperators, + ConstraintKinds, + PolyKinds, + TypeFamilies, + GADTs, + MultiParamTypeClasses, + FunctionalDependencies, + FlexibleInstances, + FlexibleContexts, + UndecidableInstances, + UndecidableSuperClasses, + TypeApplications, + ScopedTypeVariables, + AllowAmbiguousTypes, + ExplicitForAll, + RankNTypes, + DefaultSignatures, + PartialTypeSignatures, + LambdaCase, + EmptyCase +#-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} + +module Data.RBR.Internal where + +import Data.Proxy +import Data.Kind +import Data.Typeable +import Data.Coerce +import Data.Functor.Contravariant (Contravariant(contramap)) +import Data.Bifunctor (first) +import Data.Monoid (Endo(..)) +import Data.List (intersperse) +import Data.Foldable (asum) +import GHC.TypeLits +import GHC.Generics (D1,C1,S1(..),M1(..),K1(..),Rec0(..)) +import qualified GHC.Generics as G + +import Data.SOP (I(..),K(..),unI,unK,NP(..),NS(..),All,SListI,type (-.->)(Fn,apFn),mapKIK,(:.:)(..),Top) +import Data.SOP.NP (collapse_NP,liftA_NP,liftA2_NP,cliftA_NP,cliftA2_NP,pure_NP,sequence_NP,sequence'_NP) +import Data.SOP.NS (collapse_NS,ap_NS,injections,Injection) + + +{- $setup + +>>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric +>>> :set -Wno-partial-type-signatures +>>> import Data.RBR +>>> import Data.SOP +>>> import GHC.Generics + +-} + + +-- | The color of a node. +data Color = R + | B + deriving (Show,Eq) + +-- | A Red-Black tree. It will be used as a kind, to index the 'Record' and 'Variant' types. +data Map symbol q = E + | N Color (Map symbol q) symbol q (Map symbol q) + deriving (Show,Eq) + +-- | A map without entries. See also 'unit' and 'impossible'. +type Empty = E + +-- +-- +-- This code has been copied and adapted from the corresponding Data.SOP code (the All constraint). +-- + +-- Why is this KeysValuesAllF type family needed at all? Why is not KeysValuesAll sufficient by itself? +-- In fact, if I delete KeysValuesAllF and use eclusively KeysValuesAll, functions like demoteKeys seem to still work fine. +-- +-- UndecidableSuperClasses and RankNTypes seem to be required by KeysValuesAllF. +type family + KeysValuesAllF (c :: symbol -> q -> Constraint) (t :: Map symbol q) :: Constraint where + KeysValuesAllF _ E = () + KeysValuesAllF c (N color left k v right) = (c k v, KeysValuesAll c left, KeysValuesAll c right) + +{- | Require a constraint for every key-value pair in a tree. This is a generalization of 'Data.SOP.All' from "Data.SOP". +-} +class KeysValuesAllF c t => KeysValuesAll (c :: symbol -> q -> Constraint) (t :: Map symbol q) where + + -- 'cpara_Map' constructs a 'Record' by means of a constraint for producing + -- the nodes of the tree. The constraint is passed as a 'Data.Proxy.Proxy'. + cpara_Map :: + proxy c + -> r E + -> (forall left k v right color . (c k v, KeysValuesAll c left, KeysValuesAll c right) + => r left -> r right -> r (N color left k v right)) + -> r t + +{- | This typeclass provides generalizations of 'Applicative'-like functions + - which work over 'Record's and 'Variant's. +-} +class Maplike (t :: Map Symbol Type) where + {- | + See 'cpure_Record' and 'cpure'_Record' for more useful versions of + this function. + + The naming scheme follows that of 'Data.SOP.NP.pure_NP'. + -} + pure_Record :: (forall v. f v) -> Record f t + {- | + Pulls out an 'Applicative' that wraps each field, resulting in an 'Applicative' containing a pure 'Record'. + + The naming scheme follows that of 'Data.SOP.NP.sequence_NP'. + -} + sequence_Record :: Applicative f => Record f t -> f (Record I t) + {- | + Like 'sequence_Record', but only pulls out the outer 'Applicative' + from an 'Applicative' composition that wraps each field. See '(:.:)'. + + This can be useful for staged computations, where each stage is + represented by an 'Applicative' layer. + + The naming scheme follows that of 'Data.SOP.NP.sequence'_NP'. + -} + sequence'_Record :: Applicative f => Record (f :.: g) t -> f (Record g t) + {- | Apply a transformation to the type constructor which wraps the fields of a 'Record'. + + The naming scheme follows that of 'Data.SOP.NP.liftA_NP'. + -} + liftA_Record :: (forall a. f a -> g a) -> Record f t -> Record g t + {- | + The naming scheme follows that of 'Data.SOP.NP.liftA2_NP'. + -} + liftA2_Record :: (forall a. f a -> g a -> h a) -> Record f t -> Record g t -> Record h t + {- | Apply a transformation to the active branch of a 'Variant'. + + The naming scheme follows that of 'Data.SOP.NS.liftA_NS'. + -} + liftA_Variant :: (forall a. f a -> g a) -> Variant f t -> Variant g t + {- | Given a 'Record' of transformation, apply the one which matches the active branch of 'Variant'. + + The naming scheme follows that of 'Data.SOP.NS.liftA_NS'. + -} + liftA2_Variant :: (forall a. f a -> g a -> h a) -> Record f t -> Variant g t -> Variant h t + {- | + Construct a 'Record' made of functions which take a value of the + field's type and inject it in the 'Variant' branch which corresponds + to the field. + -} + injections_Variant :: Record (VariantInjection f t) t + {- | Collapse a 'Record' composed of 'K' monoidal annotations. + + >>> collapse'_Record (unit :: Record (K [Bool]) Empty) + [] + + >>> collapse'_Record (insert @"bar" (K [False]) unit) + [False] + + The naming scheme follows that of 'Data.SOP.NP.collapse_NP'. + + -} + collapse'_Record :: Monoid a => Record (K a) t -> a + collapse_Variant :: Variant (K a) t -> a + +instance Maplike E where + pure_Record _ = Empty + sequence_Record Empty = pure Empty + sequence'_Record Empty = pure Empty + liftA_Record _ Empty = Empty + liftA2_Record _ Empty Empty = Empty + liftA_Variant _ neverHappens = impossible neverHappens + liftA2_Variant _ Empty neverHappens = impossible neverHappens + injections_Variant = Empty + collapse'_Record Empty = mempty + collapse_Variant = impossible + +instance (Maplike left, Maplike right) => Maplike (N color left k v right) where + pure_Record f = Node (pure_Record f) f (pure_Record f) + sequence_Record (Node left v right) = (\l x r -> Node l (I x) r) <$> sequence_Record left <*> v <*> sequence_Record right + sequence'_Record (Node left (Comp v) right) = (\l x r -> Node l x r) <$> sequence'_Record left <*> v <*> sequence'_Record right + liftA_Record trans (Node left1 v1 right1) = Node (liftA_Record trans left1) (trans v1) (liftA_Record trans right1) + liftA2_Record trans (Node left1 v1 right1) (Node left2 v2 right2) = Node (liftA2_Record trans left1 left2) (trans v1 v2) (liftA2_Record trans right1 right2) + liftA_Variant trans vv = case vv of + Here fv -> Here (trans fv) + LookLeft leftV -> LookLeft (liftA_Variant trans leftV) + LookRight rightV -> LookRight (liftA_Variant trans rightV) + liftA2_Variant trans (Node left rv right) vv = case vv of + Here fv -> Here (trans rv fv) + LookLeft leftV -> LookLeft (liftA2_Variant trans left leftV) + LookRight rightV -> LookRight (liftA2_Variant trans right rightV) + injections_Variant = + let injections_Left = liftA_Record (\(VariantInjection j) -> VariantInjection $ LookLeft . j) (injections_Variant @left) + injections_Right = liftA_Record (\(VariantInjection j) -> VariantInjection $ LookRight . j) (injections_Variant @right) + in Node injections_Left (VariantInjection $ Here) injections_Right + collapse'_Record (Node left (K v) right) = collapse'_Record left <> (v <> collapse'_Record right) + collapse_Variant vv = case vv of + Here (K a) -> a + LookLeft leftV -> collapse_Variant leftV + LookRight rightV -> collapse_Variant rightV + +{- | + A function which takes the value of a field and injects it into the corresponding branch of a 'Variant'. + + See also 'Data.SOP.NS.Injection'. + -} +newtype VariantInjection (f :: q -> Type) (t :: Map Symbol q) (v :: q) = VariantInjection { runVariantInjection :: f v -> Variant f t } + +instance KeysValuesAll c E where + cpara_Map _p nil _step = nil + +instance (c k v, KeysValuesAll c left, KeysValuesAll c right) => KeysValuesAll c (N color left k v right) where + cpara_Map p nil cons = + cons (cpara_Map p nil cons) (cpara_Map p nil cons) + +{- | + Create a 'Record', knowing that both keys and values satisfy a 2-place constraint. The constraint is passed as a 'Data.Proxy.Proxy'. + + The naming scheme follows that of 'Data.SOP.NP.cpure_NP'. + -} +cpure_Record :: forall c t f. KeysValuesAll c t => (Proxy c) -> (forall k v. c k v => f v) -> Record f t +cpure_Record _ fpure = cpara_Map (Proxy @c) unit go + where + go :: forall left k' v' right color. (c k' v', KeysValuesAll c left, KeysValuesAll c right) + => Record f left + -> Record f right + -> Record f (N color left k' v' right) + go left right = Node left (fpure @k' @v') right + +{- | + Create a 'Record', knowing that the keys can be demoted to strings and that + the values satisfy some constraint. The constraint is passed as a + 'Data.Proxy.Proxy'. + + The fuction that constructs each field receives the name of the field as an + argument. + + The naming scheme follows that of 'Data.SOP.NP.cpure_NP'. + -} +cpure'_Record :: forall c t f. KeysValuesAll (KeyValueConstraints KnownSymbol c) t => (Proxy c) -> (forall v. c v => String -> f v) -> Record f t +cpure'_Record _ fpure = cpara_Map (Proxy @(KeyValueConstraints KnownSymbol c)) unit go + where + go :: forall left k' v' right color. (KeyValueConstraints KnownSymbol c k' v', KeysValuesAll (KeyValueConstraints KnownSymbol c) left, KeysValuesAll (KeyValueConstraints KnownSymbol c) right) + => Record f left + -> Record f right + -> Record f (N color left k' v' right) + go left right = Node left (fpure @v' (symbolVal (Proxy @k'))) right + + +{- | Create a 'Record' containing the names of each field. + + The names are represented by a constant functor 'K' carrying an annotation + of type 'String'. This means that there aren't actually any values of the + type that corresponds to each field, only the 'String' annotations. + +>>> putStrLn $ prettyShow_Record show $ demoteKeys @(Insert "foo" Char (Insert "bar" Bool Empty)) +{bar = K "bar", foo = K "foo"} + + For computations involving field names, sometimes 'cpure\'_Record' is a better option. + +-} +demoteKeys :: forall t. KeysValuesAll KnownKey t => Record (K String) t +demoteKeys = cpara_Map (Proxy @KnownKey) unit go + where + go :: forall left k v right color. (KnownKey k v, KeysValuesAll KnownKey left, KeysValuesAll KnownKey right) + => Record (K String) left + -> Record (K String) right + -> Record (K String) (N color left k v right) + go left right = Node left (K (symbolVal (Proxy @k))) right + +{- | + Two-place constraint saying that a 'Symbol' key can be demoted to 'String'. Nothing is required from the corresponding value. + + Defined using the "class synonym" . +-} +class KnownSymbol k => KnownKey (k :: Symbol) (v :: q) +instance KnownSymbol k => KnownKey k v + + +{- | + Create a record containing the names of each field along with a term-level + representation of each type. + +>>> putStrLn $ prettyShow_Record show $ demoteEntries @(Insert "foo" Char (Insert "bar" Bool Empty)) +{bar = K ("bar",Bool), foo = K ("foo",Char)} + + See also 'collapse_Record' for getting the entries as a list. +-} +demoteEntries :: forall t. KeysValuesAll KnownKeyTypeableValue t => Record (K (String,TypeRep)) t +demoteEntries = cpara_Map (Proxy @KnownKeyTypeableValue) unit go + where + go :: forall left k v right color. (KnownKeyTypeableValue k v, KeysValuesAll KnownKeyTypeableValue left, KeysValuesAll KnownKeyTypeableValue right) + => Record (K (String,TypeRep)) left + -> Record (K (String,TypeRep)) right + -> Record (K (String,TypeRep)) (N color left k v right) + go left right = Node left (K (symbolVal (Proxy @k),typeRep (Proxy @v))) right + +{- | + Two-place constraint saying that a 'Symbol' key can be demoted to 'String', and that the corresponding value 'Type' has a term-level representation. + + Defined using the "class synonym" . +-} +class (KnownSymbol k, Typeable v) => KnownKeyTypeableValue (k :: Symbol) (v :: q) +instance (KnownSymbol k, Typeable v) => KnownKeyTypeableValue k v + +{- | + Lifts two one-place constraints (one for keys, one for values) to a two-place constraint. Useful with function like 'cpure_Record'. + + Defined using the "class synonym" . +-} +class (kc k, vc v) => KeyValueConstraints (kc :: Symbol -> Constraint) (vc :: q -> Constraint) (k :: Symbol) (v :: q) +instance (kc k, vc v) => KeyValueConstraints kc vc k v + +{- | + Lifts a one-place constraint for values to a two-place constraint. Useful with function like 'cpure_Record'. + + Defined using the "class synonym" . +-} +class (vc v) => ValueConstraint (vc :: q -> Constraint) (k :: Symbol) (v :: q) +instance (vc v) => ValueConstraint vc k v + +-- +-- + +{- | An extensible product-like type with named fields. + + The values in the 'Record' come wrapped in a type constructor @f@, which + por pure records will be the identity functor 'I'. + + See also 'insert', 'delete' and 'project'. +-} +data Record (f :: q -> Type) (t :: Map Symbol q) where + Empty :: Record f E + Node :: Record f left -> f v -> Record f right -> Record f (N color left k v right) + +instance (Productlike '[] t result, Show (NP f result)) => Show (Record f t) where + show x = "fromNP (" ++ show (toNP x) ++ ")" + + +{-# DEPRECATED collapse_Record "Use collapse'_Record" #-} +collapse_Record :: forall t result a. (Productlike '[] t result) => Record (K a) t -> [a] +collapse_Record = collapse_NP . toNP + + +{- | Show a 'Record' in a friendlier way than the default 'Show' instance. The + function argument will usually be 'show', but it can be used to unwrap the + value of each field before showing it. +-} +prettyShow_Record :: forall t f. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) + => (forall x. Show x => f x -> String) + -> Record f t + -> String +prettyShow_Record showf r = + let showfs = cpure'_Record (Proxy @Show) $ \fieldName -> Comp (fieldName, Case showf) + entries = liftA2_Record (\(Comp (fieldName,Case f)) fv -> K [ fieldName ++ " = " ++ f fv ]) showfs r + in "{" ++ mconcat (intersperse ", " (collapse'_Record entries)) ++ "}" + + +{- | Like 'prettyShow_Record' but specialized to pure records. +-} +prettyShow_RecordI :: forall t. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) => Record I t -> String +prettyShow_RecordI r = prettyShow_Record (show . unI) r + + +{-# DEPRECATED prettyShowRecord "Use prettyShow_Record" #-} +prettyShowRecord :: forall t flat f. (KeysValuesAll KnownKey t,Productlike '[] t flat, All Show flat, SListI flat) + => (forall x. Show x => f x -> String) + -> Record f t + -> String +prettyShowRecord showf r = + let keysflat = toNP @t (demoteKeys @t) + valuesflat = toNP @t r + entries = cliftA2_NP (Proxy @Show) (\(K key) fv -> K (key ++ " = " ++ showf fv)) + keysflat + valuesflat + in "{" ++ mconcat (intersperse ", " (collapse_NP entries)) ++ "}" + + +{-# DEPRECATED prettyShowRecordI "Use prettyShow_RecordI" #-} +prettyShowRecordI :: forall t flat. (KeysValuesAll KnownKey t,Productlike '[] t flat, All Show flat, SListI flat) => Record I t -> String +prettyShowRecordI r = prettyShowRecord (show . unI) r + +{-| A Record without components is a boring, uninformative type whose single value can be conjured out of thin air. +-} +unit :: Record f Empty +unit = Empty + +{- | An extensible sum-like type with named branches. + + The values in the 'Variant' come wrapped in a type constructor @f@, which + por pure variants will be the identity functor 'I'. + + See also 'widen', 'winnow' and 'inject'. +-} +data Variant (f :: q -> Type) (t :: Map Symbol q) where + Here :: f v -> Variant f (N color left k v right) + LookRight :: Variant f t -> Variant f (N color' left' k' v' t) + LookLeft :: Variant f t -> Variant f (N color' t k' v' right') + +instance (Sumlike '[] t result, Show (NS f result)) => Show (Variant f t) where + show x = "fromNS (" ++ show (toNS x) ++ ")" + +{-| A Variant without branches doesn't have any values. From an impossible thing, anything can come out. +-} +impossible :: Variant f Empty -> b +impossible v = case v of + + +{- | Show a 'Variant' in a friendlier way than the default 'Show' instance. The + function argument will usually be 'show', but it can be used to unwrap the + value of the branch before showing it. +-} +prettyShow_Variant :: forall t flat f. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) + => (forall x. Show x => f x -> String) + -> Variant f t + -> String +prettyShow_Variant showf v = + let showfs = cpure'_Record (Proxy @Show) $ \fieldName -> Comp (fieldName, Case showf) + entries = liftA2_Variant (\(Comp (fieldName,Case f)) fv -> K (fieldName ++ " (" ++ f fv ++ ")")) showfs v + in collapse_Variant entries + +{- | Like 'prettyShow_Variant' but specialized to pure variants. +-} +prettyShow_VariantI :: forall t flat. (Maplike t, KeysValuesAll (KeyValueConstraints KnownSymbol Show) t) + => Variant I t -> String +prettyShow_VariantI v = prettyShow_Variant (show . unI) v + + +{-# DEPRECATED prettyShowVariant "Use prettyShow_Variant" #-} +prettyShowVariant :: forall t flat f. (KeysValuesAll KnownKey t,Productlike '[] t flat, Sumlike '[] t flat, All Show flat, SListI flat) + => (forall x. Show x => f x -> String) + -> Variant f t + -> String +prettyShowVariant showf v = + let keysflat = toNP @t (demoteKeys @t) + eliminators = cliftA_NP (Proxy @Show) (\(K k) -> Fn (\fv -> (K (k ++ " (" ++ showf fv ++ ")")))) keysflat + valuesflat = toNS @t v + in collapse_NS (ap_NS eliminators valuesflat) + +{-# DEPRECATED prettyShowVariantI "Use prettyShow_VariantI" #-} +prettyShowVariantI :: forall t flat. (KeysValuesAll KnownKey t,Productlike '[] t flat, Sumlike '[] t flat, All Show flat, SListI flat) + => Variant I t -> String +prettyShowVariantI v = prettyShowVariant (show . unI) v + +-- +-- +-- Insertion + +{- | Insert a list of type level key / value pairs into a type-level map. +-} +type family InsertAll (es :: [(Symbol,q)]) (t :: Map Symbol q) :: Map Symbol q where + InsertAll '[] t = t + InsertAll ( '(name,fieldType) ': es ) t = Insert name fieldType (InsertAll es t) + +{- | Build a type-level map out of a list of type level key / value pairs. +-} +type FromList (es :: [(Symbol,q)]) = InsertAll es Empty + + +{- | + Adds a new field to a 'Record'. + +>>> project @"foo" (insert @"foo" (I 'a') unit) +I 'a' + +>>> project @"foo" (insert @"foo" @Char Nothing unit) +Nothing + + -} +insert :: forall k v t f. Insertable k v t => f v -> Record f t -> Record f (Insert k v t) +insert = _insert @_ @k @v @t @f + +{- | + Lets you use a 'Variant' in a bigger context + than the one in which is was defined. + -} +widen :: forall k v t f. Insertable k v t => Variant f t -> Variant f (Insert k v t) +widen = _widen @_ @k @v @t @f + +{- | Alias for 'insert'. +-} +addField :: forall k v t f. Insertable k v t => f v -> Record f t -> Record f (Insert k v t) +addField = insert @k @v @t @f + +{- | Like 'insert' but specialized to pure 'Record's. + +>>> projectI @"foo" (insertI @"foo" 'a' unit) +'a' + +-} +insertI :: forall k v t . Insertable k v t => v -> Record I t -> Record I (Insert k v t) +insertI = insert @k @v @t . I + +{- | Like 'addField' but specialized to pure 'Record's. +-} +addFieldI :: forall k v t . Insertable k v t => v -> Record I t -> Record I (Insert k v t) +addFieldI = insertI @k @v @t + +{- | Class that determines if the pair of a 'Symbol' key and a type can + be inserted into a type-level map. + + The associated type family 'Insert' produces the resulting map. + + At the term level, this manifests in 'insert', which adds a new field to a + record, and in 'widen', which lets you use a 'Variant' in a bigger context + than the one in which is was defined. 'insert' tends to be more useful in + practice. + + If the map already has the key but with a /different/ type, the + insertion fails to compile. + -} +class Insertable (k :: Symbol) (v :: q) (t :: Map Symbol q) where + type Insert k v t :: Map Symbol q + _insert :: f v -> Record f t -> Record f (Insert k v t) + _widen :: Variant f t -> Variant f (Insert k v t) + +-- insert x s = +-- T B a z b +-- where +-- T _ a z b = ins s +instance (InsertableHelper1 k v t, Insert1 k v t ~ inserted, CanMakeBlack inserted) => Insertable k v t where + type Insert k v t = MakeBlack (Insert1 k v t) + _insert fv r = makeBlackR @_ (insert1 @_ @k @v fv r) + _widen v = makeBlackV @_ (widen1 @_ @k @v v) + +class CanMakeBlack (t :: Map Symbol k) where + type MakeBlack t :: Map Symbol k + makeBlackR :: Record f t -> Record f (MakeBlack t) + makeBlackV :: Variant f t -> Variant f (MakeBlack t) + +instance CanMakeBlack (N color left k v right) where + type MakeBlack (N color left k v right) = N B left k v right + makeBlackR (Node left fv right) = Node left fv right + makeBlackV v = case v of + LookLeft l -> LookLeft l + Here v -> Here v + LookRight r -> LookRight r + +instance CanMakeBlack E where + type MakeBlack E = E + makeBlackR Empty = Empty + makeBlackV = impossible + +class InsertableHelper1 (k :: Symbol) + (v :: q) + (t :: Map Symbol q) where + type Insert1 k v t :: Map Symbol q + insert1 :: f v -> Record f t -> Record f (Insert1 k v t) + widen1 :: Variant f t -> Variant f (Insert1 k v t) + +instance InsertableHelper1 k v E where + type Insert1 k v E = N R E k v E + insert1 fv Empty = Node Empty fv Empty + widen1 = impossible + +instance (CmpSymbol k k' ~ ordering, + InsertableHelper2 ordering k v color left k' v' right + ) + => InsertableHelper1 k v (N color left k' v' right) where + -- FIXME possible duplicate work with CmpSymbol: both in constraint and in associated type family. + -- Is that bad? How to avoid it? + type Insert1 k v (N color left k' v' right) = Insert2 (CmpSymbol k k') k v color left k' v' right + insert1 = insert2 @_ @ordering @k @v @color @left @k' @v' @right + widen1 = widen2 @_ @ordering @k @v @color @left @k' @v' @right + +class InsertableHelper2 (ordering :: Ordering) + (k :: Symbol) + (v :: q) + (color :: Color) + (left :: Map Symbol q) + (k' :: Symbol) + (v' :: q) + (right :: Map Symbol q) where + type Insert2 ordering k v color left k' v' right :: Map Symbol q + insert2 :: f v -> Record f (N color left k' v' right) -> Record f (Insert2 ordering k v color left k' v' right) + widen2 :: Variant f (N color left k' v' right) -> Variant f (Insert2 ordering k v color left k' v' right) + +-- ins s@(T B a y b) +-- | x InsertableHelper2 LT k v B left k' v' right where + type Insert2 LT k v B left k' v' right = Balance (Insert1 k v left) k' v' right + insert2 fv (Node left fv' right) = balanceR @_ @_ @k' @v' @right (Node (insert1 @_ @k @v fv left) fv' right) + widen2 v = balanceV @_ @(Insert1 k v left) @k' @v' @right $ case v of + Here x -> Here x + LookLeft x -> LookLeft (widen1 @_ @k @v x) + LookRight x -> LookRight x + +-- ins s@(T B a y b) +-- | x InsertableHelper2 LT k v R left k' v' right where + type Insert2 LT k v R left k' v' right = N R (Insert1 k v left) k' v' right + insert2 fv (Node left fv' right) = Node (insert1 @_ @k @v fv left) fv' right + widen2 v = case v of + Here x -> Here x + LookLeft x -> LookLeft (widen1 @_ @k @v x) + LookRight x -> LookRight x + + +-- This instance implies that we can't change the type associated to an +-- existing key. If we did that, we wouldn't be able to widen Variants that +-- happen to match that key! +instance InsertableHelper2 EQ k v color left k v right where + type Insert2 EQ k v color left k v right = N color left k v right + insert2 fv (Node left _ right) = Node left fv right + widen2 = id + +-- ins s@(T B a y b) +-- | ... +-- | x>y = balance a y (ins b) +instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted, + Balanceable left k' v' inserted + ) + => InsertableHelper2 GT k v B left k' v' right where + type Insert2 GT k v B left k' v' right = Balance left k' v' (Insert1 k v right) + insert2 fv (Node left fv' right) = balanceR @_ @left @k' @v' @_ (Node left fv' (insert1 @_ @k @v fv right)) + widen2 v = balanceV @_ @left @k' @v' @(Insert1 k v right) $ case v of + Here x -> Here x + LookLeft x -> LookLeft x + LookRight x -> LookRight (widen1 @_ @k @v x) + +-- ins s@(T R a y b) +-- | ... +-- | x>y = T R a y (ins b) +instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted, + Balanceable left k' v' inserted + ) + => InsertableHelper2 GT k v R left k' v' right where + type Insert2 GT k v R left k' v' right = N R left k' v' (Insert1 k v right) + insert2 fv (Node left fv' right) = Node left fv' (insert1 @_ @k @v fv right) + widen2 v = case v of + Here x -> Here x + LookLeft x -> LookLeft x + LookRight x -> LookRight (widen1 @_ @k @v x) + +data BalanceAction = BalanceSpecial + | BalanceLL + | BalanceLR + | BalanceRL + | BalanceRR + | DoNotBalance + deriving Show + +type family ShouldBalance (left :: Map k' v') (right :: Map k' v') :: BalanceAction where + ShouldBalance (N R _ _ _ _) (N R _ _ _ _) = BalanceSpecial + ShouldBalance (N R (N R _ _ _ _) _ _ _) _ = BalanceLL + ShouldBalance (N R _ _ _ (N R _ _ _ _)) _ = BalanceLR + ShouldBalance _ (N R (N R _ _ _ _) _ _ _) = BalanceRL + ShouldBalance _ (N R _ _ _ (N R _ _ _ _)) = BalanceRR + ShouldBalance _ _ = DoNotBalance + +class Balanceable (left :: Map Symbol q) (k :: Symbol) (v :: q) (right :: Map Symbol q) where + type Balance left k v right :: Map Symbol q + balanceR :: Record f (N color left k v right) -> Record f (Balance left k v right) + balanceV :: Variant f (N color left k v right) -> Variant f (Balance left k v right) + +instance (ShouldBalance left right ~ action, + BalanceableHelper action left k v right + ) + => Balanceable left k v right where + -- FIXME possible duplicate work with ShouldBalance: both in constraint and in associated type family. + -- Is that bad? How to avoid it? + type Balance left k v right = Balance' (ShouldBalance left right) left k v right + balanceR = balanceR' @_ @action @left @k @v @right + balanceV = balanceV' @_ @action @left @k @v @right + +class BalanceableHelper (action :: BalanceAction) + (left :: Map Symbol q) + (k :: Symbol) + (v :: q) + (right :: Map Symbol q) where + type Balance' action left k v right :: Map Symbol q + balanceR' :: Record f (N color left k v right) -> Record f (Balance' action left k v right) + balanceV' :: Variant f (N color left k v right) -> Variant f (Balance' action left k v right) + +-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d) +instance BalanceableHelper BalanceSpecial (N R left1 k1 v1 right1) kx vx (N R left2 k2 v2 right2) where + type Balance' BalanceSpecial (N R left1 k1 v1 right1) kx vx (N R left2 k2 v2 right2) = + N R (N B left1 k1 v1 right1) kx vx (N B left2 k2 v2 right2) + balanceR' (Node (Node left1 v1 right1) vx (Node left2 v2 right2)) = + (Node (Node left1 v1 right1) vx (Node left2 v2 right2)) + balanceV' v = case v of + LookLeft (LookLeft x) -> LookLeft (LookLeft x) + LookLeft (Here x) -> LookLeft (Here x) + LookLeft (LookRight x) -> LookLeft (LookRight x) + Here x -> Here x + LookRight (LookLeft x) -> LookRight (LookLeft x) + LookRight (Here x) -> LookRight (Here x) + LookRight (LookRight x) -> LookRight (LookRight x) + +-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) +instance BalanceableHelper BalanceLL (N R (N R a k1 v1 b) k2 v2 c) k3 v3 d where + type Balance' BalanceLL (N R (N R a k1 v1 b) k2 v2 c) k3 v3 d = + N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d) + balanceR' (Node (Node (Node a fv1 b) fv2 c) fv3 d) = + Node (Node a fv1 b) fv2 (Node c fv3 d) + balanceV' v = case v of + LookLeft (LookLeft x) -> LookLeft (case x of LookLeft y -> LookLeft y + Here y -> Here y + LookRight y -> LookRight y) + LookLeft (Here x) -> Here x + LookLeft (LookRight x) -> LookRight (LookLeft x) + Here x -> LookRight (Here x) + LookRight x -> LookRight (LookRight x) + +-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) +instance BalanceableHelper BalanceLR (N R a k1 v1 (N R b k2 v2 c)) k3 v3 d where + type Balance' BalanceLR (N R a k1 v1 (N R b k2 v2 c)) k3 v3 d = + N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d) + balanceR' (Node (Node a fv1 (Node b fv2 c)) fv3 d) = + Node (Node a fv1 b) fv2 (Node c fv3 d) + balanceV' v = case v of + LookLeft (LookLeft x) -> LookLeft (LookLeft x) + LookLeft (Here x) -> LookLeft (Here x) + LookLeft (LookRight x) -> case x of LookLeft y -> LookLeft (LookRight y) + Here y -> Here y + LookRight y -> LookRight (LookLeft y) + Here x -> LookRight (Here x) + LookRight x -> LookRight (LookRight x) + +-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) +instance BalanceableHelper BalanceRL a k1 v1 (N R (N R b k2 v2 c) k3 v3 d) where + type Balance' BalanceRL a k1 v1 (N R (N R b k2 v2 c) k3 v3 d) = + N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d) + balanceR' (Node a fv1 (Node (Node b fv2 c) fv3 d)) = + Node (Node a fv1 b) fv2 (Node c fv3 d) + balanceV' v = case v of + LookLeft x -> LookLeft (LookLeft x) + Here x -> LookLeft (Here x) + LookRight (LookLeft x) -> case x of LookLeft y -> LookLeft (LookRight y) + Here y -> Here y + LookRight y -> LookRight (LookLeft y) + LookRight (Here x) -> LookRight (Here x) + LookRight (LookRight x) -> LookRight (LookRight x) + + +-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) +instance BalanceableHelper BalanceRR a k1 v1 (N R b k2 v2 (N R c k3 v3 d)) where + type Balance' BalanceRR a k1 v1 (N R b k2 v2 (N R c k3 v3 d)) = + N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d) + balanceR' (Node a fv1 (Node b fv2 (Node c fv3 d))) = + Node (Node a fv1 b) fv2 (Node c fv3 d) + balanceV' v = case v of + LookLeft x -> LookLeft (LookLeft x) + Here x -> LookLeft (Here x) + LookRight (LookLeft x) -> LookLeft (LookRight x) + LookRight (Here x) -> Here x + LookRight (LookRight x) -> LookRight (case x of LookLeft y -> LookLeft y + Here y -> Here y + LookRight y -> LookRight y) + +-- balance a x b = T B a x b +instance BalanceableHelper DoNotBalance a k v b where + type Balance' DoNotBalance a k v b = N B a k v b + balanceR' (Node left v right) = (Node left v right) + balanceV' v = case v of + LookLeft l -> LookLeft l + Here v -> Here v + LookRight r -> LookRight r + + +-- +-- +-- Accessing fields + +-- +-- These two type families exist to avoid duplicating expensive type-level +-- computations, in particular the Value' computations. +-- +-- Record accessors are compiled WAY slower without them! +-- +{- | Auxiliary type family to avoid repetition and help improve compilation times. + -} +type family Field (f :: q -> Type) (t :: Map Symbol q) (v :: q) where + Field f t v = Record f t -> (f v -> Record f t, f v) + +{- | Auxiliary type family to avoid repetition and help improve compilation times. + -} +type family Branch (f :: q -> Type) (t :: Map Symbol q) (v :: q) where + Branch f t v = (Variant f t -> Maybe (f v), f v -> Variant f t) + +-- +{- | + Class that determines if a given 'Symbol' key is present in a type-level + map. + + The 'Value' type family gives the 'Type' corresponding to the key. +-} +class Key (k :: Symbol) (t :: Map Symbol q) where + type Value k t :: q + _field :: Field f t (Value k t) + _branch :: Branch f t (Value k t) + +{- | + Takes a field name (given through @TypeApplications@) and a + 'Record', and returns a pair of a setter for the field and the original + value of the field. +-} +field :: forall k t f. Key k t => Field f t (Value k t) +field = _field @_ @k @t + +{- | + Takes a branch name (given through @TypeApplications@) and + returns a pair of a match function and a constructor. +-} +branch :: forall k t f. Key k t => Branch f t (Value k t) +branch = _branch @_ @k @t + +-- member :: Ord a => a -> RB a -> Bool +class KeyHelper (ordering :: Ordering) (k :: Symbol) (left :: Map Symbol q) (v :: q) (right :: Map Symbol q) where + type Value' ordering k left v right :: q + field' :: Field f (N colorx left kx v right) (Value' ordering k left v right) + branch' :: Branch f (N colorx left kx v right) (Value' ordering k left v right) + +instance (CmpSymbol k' k ~ ordering, KeyHelper ordering k left v' right) => Key k (N color left k' v' right) where + type Value k (N color left k' v' right) = Value' (CmpSymbol k' k) k left v' right + _field = field' @_ @ordering @k @left @v' @right + _branch = branch' @_ @ordering @k @left @v' @right + +-- | x KeyHelper LT k left v (N color2 left2 k2 v2 right2) where + type Value' LT k left v (N color2 left2 k2 v2 right2) = Value' (CmpSymbol k2 k) k left2 v2 right2 + field' (Node left fv right) = + let (setter,x) = field' @_ @ordering @k @left2 @v2 @right2 right + in (\z -> Node left fv (setter z),x) + branch' = + let (match,inj) = branch' @_ @ordering @k @left2 @v2 @right2 + in (\case LookRight x -> match x + _ -> Nothing, + \fv -> LookRight (inj fv)) + +-- | x>y = member x b +instance (CmpSymbol k2 k ~ ordering, KeyHelper ordering k left2 v2 right2) + => KeyHelper GT k (N color2 left2 k2 v2 right2) v' right where + type Value' GT k (N color2 left2 k2 v2 right2) v' right = Value' (CmpSymbol k2 k) k left2 v2 right2 + field' (Node left fv right) = + let (setter,x) = field' @_ @ordering @k @left2 @v2 @right2 left + in (\z -> Node (setter z) fv right,x) + branch' = + let (match,inj) = branch' @_ @ordering @k @left2 @v2 @right2 + in (\case LookLeft x -> match x + _ -> Nothing, + \fv -> LookLeft (inj fv)) + +-- | otherwise = True +instance KeyHelper EQ k left v right where + type Value' EQ k left v right = v + field' (Node left fv right) = (\x -> Node left x right, fv) + branch' = (\case Here x -> Just x + _ -> Nothing, + Here) + +{- | Get the value of a field for a 'Record'. + + +-} +project :: forall k t f . Key k t => Record f t -> f (Value k t) +project = snd . field @k @t + +{- | Alias for 'project'. +-} +getField :: forall k t f . Key k t => Record f t -> f (Value k t) +getField = project @k @t @f + +{- | Set the value of a field for a 'Record'. +-} +setField :: forall k t f . Key k t => f (Value k t) -> Record f t -> Record f t +setField fv r = fst (field @k @t @f r) fv + +{- | Modify the value of a field for a 'Record'. +-} +modifyField :: forall k t f . Key k t => (f (Value k t) -> f (Value k t)) -> Record f t -> Record f t +modifyField f r = uncurry ($) (fmap f (field @k @t @f r)) + +{- | Put a value into the branch of a 'Variant'. + +>>> match @"foo" (inject @"foo" (I 'a') :: Variant I (Insert "foo" Char Empty)) +Just (I 'a') + +-} +inject :: forall k t f. Key k t => f (Value k t) -> Variant f t +inject = snd (branch @k @t) + +{- | Check if a 'Variant' value is the given branch. +-} +match :: forall k t f. Key k t => Variant f t -> Maybe (f (Value k t)) +match = fst (branch @k @t) + +{- | Like 'project' but specialized to pure 'Record's. + +>>> projectI @"foo" (insertI @"foo" 'a' (insertI @"bar" False unit)) +'a' + +-} +projectI :: forall k t . Key k t => Record I t -> Value k t +projectI = unI . snd . field @k @t + +{- | Like 'getField' but specialized to pure 'Record's. +-} +getFieldI :: forall k t . Key k t => Record I t -> Value k t +getFieldI = projectI @k @t + +{- | Like 'setField' but specialized to pure 'Record's. +-} +setFieldI :: forall k t . Key k t => Value k t -> Record I t -> Record I t +setFieldI v r = fst (field @k @t r) (I v) + +{- | Like 'modifyField' but specialized to pure 'Record's. +-} +modifyFieldI :: forall k t . Key k t => (Value k t -> Value k t) -> Record I t -> Record I t +modifyFieldI f = modifyField @k @t (I . f . unI) + +{- | Like 'inject' but specialized to pure 'Variant's. + +>>> matchI @"foo" (injectI @"foo" 'a' :: Variant I (Insert "foo" Char Empty)) +Just 'a' + +-} +injectI :: forall k t. Key k t => Value k t -> Variant I t +injectI = snd (branch @k @t) . I + +{- | Like 'match' but specialized to pure 'Variants's. +-} +matchI :: forall k t . Key k t => Variant I t -> Maybe (Value k t) +matchI v = unI <$> fst (branch @k @t) v + +{-# DEPRECATED eliminate "Use eliminate_Variant instead." #-} +eliminate :: (Productlike '[] t result, Sumlike '[] t result, SListI result) => Record (Case f r) t -> Variant f t -> r +eliminate cases variant = + let adapt (Case e) = Fn (\fv -> K (e fv)) + in collapse_NS (ap_NS (liftA_NP adapt (toNP cases)) (toNS variant)) + +{- | Process a 'Variant' using a eliminator 'Record' that carries + handlers for each possible branch of the 'Variant'. + +>>> eliminate_Variant (addCaseI @"foo" @Int succ (addCaseI @"bar" pred unit)) (injectI @"bar" 33) +32 + +-} +eliminate_Variant :: Maplike t => Record (Case f r) t -> Variant f t -> r +eliminate_Variant cases variant = + let adapt (Case f) x = K (f x) + in collapse_Variant $ liftA2_Variant adapt cases variant + +{- | Represents a handler for a branch of a 'Variant'. +-} +newtype Case f a b = Case (f b -> a) + +instance Functor f => Contravariant (Case f a) where + contramap g (Case c) = Case (c . fmap g) + +{- | A form of 'addField' for creating eliminators for 'Variant's. +-} +addCase :: forall k v t f a. Insertable k v t => (f v -> a) -> Record (Case f a) t -> Record (Case f a) (Insert k v t) +addCase f = addField @k @v @t (Case f) + +{- | A pure version of 'addCase'. +-} +addCaseI :: forall k v t a. Insertable k v t => (v -> a) -> Record (Case I a) t -> Record (Case I a) (Insert k v t) +addCaseI f = addField @k @v @t (Case (f . unI)) + +-- +-- +-- Subsetting + +newtype SetField f a b = SetField { getSetField :: f b -> a -> a } + +{- | For a given 'Map', produces a two-place constraint confirming the presence + - of a entry. + - + Defined using the "class synonym" . +-} +class (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q) +instance (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q) + +{-# DEPRECATED ProductlikeSubset "This constraint is obsolete" #-} +type ProductlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (flat :: [q]) = + (KeysValuesAll (PresentIn whole) subset, + Productlike '[] subset flat, + SListI flat) + +{-# DEPRECATED fieldSubset "Use Data.RBR.Subset.fieldSubset" #-} +fieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) + => Record f whole -> (Record f subset -> Record f whole, Record f subset) +fieldSubset r = + (,) + (let goset :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left, + KeysValuesAll (PresentIn whole) right) + => Record (SetField f (Record f whole)) left + -> Record (SetField f (Record f whole)) right + -> Record (SetField f (Record f whole)) (N color left k v right) + goset left right = Node left (SetField (\v w -> fst (field @k @whole w) v)) right + setters = toNP @subset @_ @(SetField f (Record f whole)) (cpara_Map (Proxy @(PresentIn whole)) unit goset) + appz (SetField func) fv = K (Endo (func fv)) + in \toset -> appEndo (mconcat (collapse_NP (liftA2_NP appz setters (toNP toset)))) r) + (let goget :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left, + KeysValuesAll (PresentIn whole) right) + => Record f left + -> Record f right + -> Record f (N color left k v right) + goget left right = Node left (project @k @whole r) right + in cpara_Map (Proxy @(PresentIn whole)) unit goget) + +{-# DEPRECATED projectSubset "Use Data.RBR.Subset.projectSubset" #-} +projectSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) + => Record f whole + -> Record f subset +projectSubset = snd . fieldSubset + +{-# DEPRECATED getFieldSubset "Use Data.RBR.Subset.getFieldSubset" #-} +getFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) + => Record f whole + -> Record f subset +getFieldSubset = projectSubset + +{-# DEPRECATED setFieldSubset "Use Data.RBR.Subset.setFieldSubset" #-} +setFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) + => Record f subset + -> Record f whole + -> Record f whole +setFieldSubset subset whole = fst (fieldSubset whole) subset + +{-# DEPRECATED modifyFieldSubset "Use Data.RBR.Subset.modifyFieldSubset" #-} +modifyFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat) + => (Record f subset -> Record f subset) + -> Record f whole + -> Record f whole +modifyFieldSubset f r = uncurry ($) (fmap f (fieldSubset @subset @whole r)) + + +{-# DEPRECATED SumlikeSubset "This constraint is obsolete" #-} +type SumlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (subflat :: [q]) (wholeflat :: [q]) = + (KeysValuesAll (PresentIn whole) subset, + Productlike '[] whole wholeflat, + Sumlike '[] whole wholeflat, + SListI wholeflat, + Productlike '[] subset subflat, + Sumlike '[] subset subflat, + SListI subflat) + +{-# DEPRECATED branchSubset "Use Data.RBR.Subset.branchSubset" #-} +branchSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat) + => (Variant f whole -> Maybe (Variant f subset), Variant f subset -> Variant f whole) +branchSubset = + let inj2case :: forall t flat f v. Sumlike '[] t flat => (_ -> _) -> Injection _ flat v -> Case _ _ v + inj2case = \adapt -> \fn -> Case (\fv -> adapt (fromNS @t (unK (apFn fn fv)))) + -- The intuition is that getting the setter and the getter together might be faster at compile-time. + -- The intuition might be wrong. + subs :: forall f. Record f whole -> (Record f subset -> Record f whole, Record f subset) + subs = fieldSubset @subset @whole + in + (,) + (let injs :: Record (Case f (Maybe (Variant f subset))) subset + injs = fromNP @subset (liftA_NP (inj2case Just) (injections @subflat)) + wholeinjs :: Record (Case f (Maybe (Variant f subset))) whole + wholeinjs = fromNP @whole (pure_NP (Case (\_ -> Nothing))) + mixedinjs = fst (subs wholeinjs) injs + in eliminate mixedinjs) + (let wholeinjs :: Record (Case f (Variant f whole)) whole + wholeinjs = fromNP @whole (liftA_NP (inj2case id) (injections @wholeflat)) + injs = snd (subs wholeinjs) + in eliminate injs) + + +{-# DEPRECATED injectSubset "Use Data.RBR.Subset.injectSubset" #-} +injectSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat) + => Variant f subset -> Variant f whole +injectSubset = snd (branchSubset @subset @whole @subflat @wholeflat) + +{-# DEPRECATED matchSubset "Use Data.RBR.Subset.matchSubset" #-} +matchSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat) + => Variant f whole -> Maybe (Variant f subset) +matchSubset = fst (branchSubset @subset @whole @subflat @wholeflat) + +{-# DEPRECATED eliminateSubset "Use Data.RBR.Subset.eliminateSubset" #-} +eliminateSubset :: forall subset whole subflat wholeflat f r. (SumlikeSubset subset whole subflat wholeflat) + => Record (Case f r) whole -> Variant f subset -> r +eliminateSubset cases = + let reducedCases = getFieldSubset @subset @whole cases + in eliminate reducedCases + +-- +-- Interaction with Data.SOP + +{- | Class from converting 'Record's to and from the n-ary product type 'NP' from "Data.SOP". + + 'prefixNP' flattens a 'Record' and adds it to the initial part of the product. + + 'breakNP' reconstructs a 'Record' from the initial part of the product and returns the unconsumed part. + + The functions 'toNP' and 'fromNP' are usually easier to use. +-} +class Productlike (start :: [k]) + (t :: Map Symbol k) + (result :: [k]) | start t -> result, result t -> start where + _prefixNP:: Record f t -> NP f start -> NP f result + _breakNP :: NP f result -> (Record f t, NP f start) + +instance Productlike start E start where + _prefixNP _ start = start + _breakNP start = (Empty, start) + +instance (Productlike start right middle, + Productlike (v ': middle) left result) + => Productlike start (N color left k v right) result where + _prefixNP (Node left fv right) start = + _prefixNP @_ @_ @left @result left (fv :* prefixNP @start @right @middle right start) + _breakNP result = + let (left, fv :* middle) = _breakNP @_ @_ @left @result result + (right, start) = _breakNP @_ @start @right middle + in (Node left fv right, start) + +{- | + Flattens a 'Record' and adds it to the initial part of the product. +-} +prefixNP:: forall start t result f. Productlike start t result => Record f t -> NP f start -> NP f result +prefixNP = _prefixNP @_ @start @t @result + +{- | + Reconstructs a 'Record' from the initial part of the product and returns the unconsumed part. +-} +breakNP :: forall start t result f. Productlike start t result => NP f result -> (Record f t, NP f start) +breakNP = _breakNP @_ @start @t @result + +{- | Convert a 'Record' into a n-ary product. The order of the elements in the + product is not the order of insertion in the record. + +>>> toNP (insertI @"foo" 'a' (insertI @"bar" True unit)) +I True :* I 'a' :* Nil + +-} +toNP :: forall t result f. Productlike '[] t result => Record f t -> NP f result +toNP r = prefixNP r Nil + +{- | Convert a n-ary product into a compatible 'Record'. Usually follows an invocation of 'toNP'. + +>>> prettyShow_RecordI . fromNP @(Insert "foo" _ (Insert "bar" _ Empty)) . toNP $ insertI @"foo" 'a' (insertI @"bar" True unit) +"{bar = True, foo = 'a'}" + +-} +fromNP :: forall t result f. Productlike '[] t result => NP f result -> Record f t +fromNP np = let (r,Nil) = breakNP np in r + +{- | Class from converting 'Variant's to and from the n-ary sum type 'NS' from "Data.SOP". + + 'prefixNS' flattens a 'Variant' and adds it to the initial part of the sum. + + 'breakNS' reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part. + + The functions 'toNS' and 'fromNS' are usually easier to use. +-} +class Sumlike (start :: [k]) + (t :: Map Symbol k) + (result :: [k]) | start t -> result, result t -> start where + _prefixNS :: Either (NS f start) (Variant f t) -> NS f result + _breakNS :: NS f result -> Either (NS f start) (Variant f t) + +instance Sumlike start + (N color E k v E) + (v ': start) where + _prefixNS = \case + Left l -> S l + Right x -> case x of Here fv -> Z @_ @v @start fv + _breakNS = \case + Z x -> Right (Here x) + S x -> Left x + +instance (Sumlike start (N colorR leftR kR vR rightR) middle, + Sumlike (v ': middle) (N colorL leftL kL vL rightL) result) + => Sumlike start + (N color (N colorL leftL kL vL rightL) k v (N colorR leftR kR vR rightR)) + result where + _prefixNS = \case + Left x -> + _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (S (_prefixNS @_ @_ @(N colorR leftR kR vR rightR) (Left x)))) + Right x -> + case x of LookLeft x -> _prefixNS @_ @(v ': middle) @(N colorL leftL kL vL rightL) @result (Right x) + Here x -> _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (Z x)) + LookRight x -> _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (S (_prefixNS @_ (Right x)))) + _breakNS ns = case _breakNS @_ @(v ': middle) @(N colorL leftL kL vL rightL) ns of + Left x -> case x of + Z x -> Right (Here x) + S x -> case _breakNS @_ @start @(N colorR leftR kR vR rightR) x of + Left ns -> Left ns + Right v -> Right (LookRight v) + Right v -> Right (LookLeft v) + +instance Sumlike (v ': start) (N colorL leftL kL vL rightL) result + => Sumlike start (N color (N colorL leftL kL vL rightL) k v E) result where + _prefixNS = \case + Left x -> + _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (S x)) + Right x -> + case x of LookLeft x -> _prefixNS @_ @(v ': start) @(N colorL leftL kL vL rightL) @result (Right x) + Here x -> _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (Z x)) + _breakNS ns = case _breakNS @_ @(v ': start) @(N colorL leftL kL vL rightL) ns of + Left x -> case x of + Z x -> Right (Here x) + S x -> Left x + Right v -> Right (LookLeft v) + +instance Sumlike start (N colorR leftR kR vR rightR) middle + => Sumlike start (N color E k v (N colorR leftR kR vR rightR)) (v ': middle) where + _prefixNS = \case + Left x -> S (_prefixNS @_ @_ @(N colorR leftR kR vR rightR) (Left x)) + Right x -> + case x of Here x -> Z x + LookRight x -> S (_prefixNS @_ @_ @(N colorR leftR kR vR rightR) (Right x)) + _breakNS = \case + Z x -> Right (Here x) + S x -> case _breakNS @_ @_ @(N colorR leftR kR vR rightR) x of + Left ns -> Left ns + Right v -> Right (LookRight v) + +{- | + + Flattens a 'Variant' and adds it to the initial part of the sum. +-} +prefixNS :: forall start t result f. Sumlike start t result => Either (NS f start) (Variant f t) -> NS f result +prefixNS = _prefixNS @_ @start @t @result + +{- | + Reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part. +-} +breakNS :: forall start t result f. Sumlike start t result => NS f result -> Either (NS f start) (Variant f t) +breakNS = _breakNS @_ @start @t @result + +{- | Convert a 'Variant' into a n-ary sum. + +>>> toNS (injectI @"foo" 'a' :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) +S (Z (I 'a')) + +-} +toNS :: forall t result f. Sumlike '[] t result => Variant f t -> NS f result +toNS = prefixNS . Right + +{- | Convert a n-ary sum into a compatible 'Variant'. + +>>> prettyShow_VariantI $ fromNS @(Insert "foo" _ (Insert "bar" _ Empty)) . toNS $ (injectI @"foo" 'a' :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) +"foo ('a')" + +-} +fromNS :: forall t result f. Sumlike '[] t result => NS f result -> Variant f t +fromNS ns = case breakNS ns of + Left _ -> error "this never happens" + Right x -> x + +-- +-- +-- Interfacing with normal records + +class ToRecord (r :: Type) where + type RecordCode r :: Map Symbol Type + -- https://stackoverflow.com/questions/22087549/defaultsignatures-and-associated-type-families/22088808 + type RecordCode r = RecordCode' E (G.Rep r) + toRecord :: r -> Record I (RecordCode r) + default toRecord :: (G.Generic r,ToRecordHelper E (G.Rep r),RecordCode r ~ RecordCode' E (G.Rep r)) => r -> Record I (RecordCode r) + toRecord r = toRecord' unit (G.from r) + +class ToRecordHelper (start :: Map Symbol Type) (g :: Type -> Type) where + type RecordCode' start g :: Map Symbol Type + toRecord' :: Record I start -> g x -> Record I (RecordCode' start g) + +instance ToRecordHelper E fields => ToRecordHelper E (D1 meta (C1 metacons fields)) where + type RecordCode' E (D1 meta (C1 metacons fields)) = RecordCode' E fields + toRecord' r (M1 (M1 g)) = toRecord' @E @fields r g + +instance (Insertable k v start) => + ToRecordHelper start + (S1 ('G.MetaSel ('Just k) + unpackedness + strictness + laziness) + (Rec0 v)) + where + type RecordCode' start + (S1 ('G.MetaSel ('Just k) + unpackedness + strictness + laziness) + (Rec0 v)) = Insert k v start + toRecord' start (M1 (K1 v)) = insertI @k v start + +instance ( ToRecordHelper start t2, + RecordCode' start t2 ~ middle, + ToRecordHelper middle t1 + ) => + ToRecordHelper start (t1 G.:*: t2) + where + type RecordCode' start (t1 G.:*: t2) = RecordCode' (RecordCode' start t2) t1 + toRecord' start (t1 G.:*: t2) = toRecord' @middle (toRecord' @start start t2) t1 + +-- +-- +class ToRecord r => FromRecord (r :: Type) where + fromRecord :: Record I (RecordCode r) -> r + default fromRecord :: (G.Generic r, FromRecordHelper (RecordCode r) (G.Rep r)) => Record I (RecordCode r) -> r + fromRecord r = G.to (fromRecord' @(RecordCode r) @(G.Rep r) r) + +{- | + The naming scheme follows that of 'Generics.SOP.IsProductType'. + -} +type IsRecordType (r :: Type) (t :: Map Symbol Type) = (G.Generic r, ToRecord r, RecordCode r ~ t, FromRecord r) + +-- {- | +-- A version of 'fromRecord' which accepts 'Record' values with more fields than the target nominal record, and possibly in an incompatible order. +-- -} +-- fromRecordSuperset :: forall r subset whole flat. (FromRecord r, RecordCode r ~ subset, ProductlikeSubset subset whole flat) => Record I whole -> r +-- fromRecordSuperset = fromRecord @r . projectSubset @subset @whole @flat + +class FromRecordHelper (t :: Map Symbol Type) (g :: Type -> Type) where + fromRecord' :: Record I t -> g x + +instance FromRecordHelper t fields => FromRecordHelper t (D1 meta (C1 metacons fields)) where + fromRecord' r = M1 (M1 (fromRecord' @t @fields r)) + +instance (Key k t, Value k t ~ v) => + FromRecordHelper t + (S1 ('G.MetaSel ('Just k) + unpackedness + strictness + laziness) + (Rec0 v)) + where + fromRecord' r = let v = projectI @k r in M1 (K1 v) + +instance ( FromRecordHelper t t1, + FromRecordHelper t t2 + ) => + FromRecordHelper t (t1 G.:*: t2) + where + fromRecord' r = + let v1 = fromRecord' @_ @t1 r + v2 = fromRecord' @_ @t2 r + in v1 G.:*: v2 + +-- +-- +-- +type family VariantCode (s :: Type) :: Map Symbol Type where + VariantCode s = VariantCode' E (G.Rep s) + +type family VariantCode' (acc :: Map Symbol Type) (g :: Type -> Type) :: Map Symbol Type where + VariantCode' acc (D1 meta fields) = VariantCode' acc fields + VariantCode' acc (t1 G.:+: t2) = VariantCode' (VariantCode' acc t2) t1 + VariantCode' acc (C1 (G.MetaCons k _ _) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v))) = Insert k v acc + VariantCode' acc (C1 (G.MetaCons k _ _) G.U1) = Insert k () acc + +class FromVariant (s :: Type) where + fromVariant :: Variant I (VariantCode s) -> s + default fromVariant :: (G.Generic s, FromVariantHelper (VariantCode s) (G.Rep s)) => Variant I (VariantCode s) -> s + fromVariant v = case fromVariant' @(VariantCode s) v of + Just x -> G.to x + Nothing -> error "fromVariant match fail. Should not happen." + +{- | + The naming scheme follows that of 'Generics.SOP.IsProductType'. + -} +type IsVariantType (v :: Type) (t :: Map Symbol Type) = (G.Generic v, ToVariant v, VariantCode v ~ t, FromVariant v) + +class FromVariantHelper (t :: Map Symbol Type) (g :: Type -> Type) where + fromVariant' :: Variant I t -> Maybe (g x) + +instance FromVariantHelper t fields => FromVariantHelper t (D1 meta fields) where + fromVariant' v = M1 <$> fromVariant' @t v + +instance (Key k t, Value k t ~ v) + => FromVariantHelper t (C1 (G.MetaCons k x y) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v))) + where + fromVariant' v = case matchI @k @t v of + Just x -> Just (M1 (M1 (K1 x)) ) + Nothing -> Nothing + +instance (Key k t, Value k t ~ ()) + => FromVariantHelper t (C1 (G.MetaCons k x y) G.U1) + where + fromVariant' v = case matchI @k @t v of + Just x -> Just (M1 G.U1) + Nothing -> Nothing + +instance ( FromVariantHelper t t1, + FromVariantHelper t t2 + ) => + FromVariantHelper t (t1 G.:+: t2) + where + fromVariant' v = case fromVariant' @t @t1 v of + Just x1 -> Just (G.L1 x1) + Nothing -> case fromVariant' @t @t2 v of + Just x2 -> Just (G.R1 x2) + Nothing -> Nothing + +-- +-- +class ToVariant (s :: Type) where + toVariant :: s -> Variant I (VariantCode s) + default toVariant :: (G.Generic s, ToVariantHelper (VariantCode s) (G.Rep s)) => s -> Variant I (VariantCode s) + toVariant s = toVariant' @(VariantCode s) @(G.Rep s) (G.from s) + +class ToVariantHelper (t :: Map Symbol Type) (g :: Type -> Type) where + toVariant' :: g x -> Variant I t + +instance ToVariantHelper t fields => ToVariantHelper t (D1 meta fields) where + toVariant' (M1 fields) = toVariant' @t fields + +instance (Key k t, Value k t ~ v) => + ToVariantHelper t (C1 (G.MetaCons k x y) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v))) + where + toVariant' (M1 (M1 (K1 v))) = injectI @k v + +instance (Key k t, Value k t ~ ()) => + ToVariantHelper t (C1 (G.MetaCons k x y) G.U1) where + toVariant' (M1 G.U1) = injectI @k () + +instance ( ToVariantHelper t t1, + ToVariantHelper t t2 + ) => + ToVariantHelper t (t1 G.:+: t2) + where + toVariant' = \case + G.L1 l -> toVariant' @t l + G.R1 r -> toVariant' @t r + +-- +-- +-- deletion +-- +-- +-- + +type family DiscriminateBalL (l :: Map k v) (r :: Map k v) :: Bool where + DiscriminateBalL (N R _ _ _ _) _ = False + DiscriminateBalL _ _ = True + +class BalanceableL (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where + type BalL l k v r :: Map Symbol q + balLR :: Record f (N color l k v r) -> Record f (BalL l k v r) + balLV :: Variant f (N color l k v r) -> Variant f (BalL l k v r) + +class BalanceableHelperL (b :: Bool) (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where + type BalL' b l k v r :: Map Symbol q + balLR' :: Record f (N color l k v r) -> Record f (BalL' b l k v r) + balLV' :: Variant f (N color l k v r) -> Variant f (BalL' b l k v r) + +instance (DiscriminateBalL l r ~ b, BalanceableHelperL b l k v r) => BalanceableL l k v r where + type BalL l k v r = BalL' (DiscriminateBalL l r) l k v r + balLR = balLR' @_ @b @l @k @v @r + balLV = balLV' @_ @b @l @k @v @r + +-- balleft :: RB a -> a -> RB a -> RB a +-- balleft (T R a x b) y c = T R (T B a x b) y c +instance BalanceableHelperL False (N R left1 k1 v1 right1) k2 v2 right2 where + type BalL' False (N R left1 k1 v1 right1) k2 v2 right2 = + (N R (N B left1 k1 v1 right1) k2 v2 right2) + balLR' (Node (Node left' v' right') v right) = Node (Node left' v' right') v right + balLV' v = case v of LookLeft x -> LookLeft (case x of LookLeft y -> LookLeft y + Here y -> Here y + LookRight y -> LookRight y) + Here x -> Here x + LookRight x -> LookRight x + +-- balleft bl x (T B a y b) = balance bl x (T R a y b) +-- the @(N B in the call to balance tree is misleading, as it is ingored... +instance (N R t2 z zv t3 ~ g, BalanceableHelper (ShouldBalance t1 g) t1 y yv g) => + BalanceableHelperL True t1 y yv (N B t2 z zv t3) where + type BalL' True t1 y yv (N B t2 z zv t3) + = Balance t1 y yv (N R t2 z zv t3) + balLR' (Node left1 v1 (Node left2 v2 right2)) = + balanceR @_ @t1 @y @yv @(N R t2 z zv t3) (Node left1 v1 (Node left2 v2 right2)) + balLV' v = balanceV @_ @t1 @y @yv @(N R t2 z zv t3) (case v of + LookLeft l -> LookLeft l + Here x -> Here x + LookRight r -> LookRight (case r of + LookLeft l' -> LookLeft l' + Here x' -> Here x' + LookRight r' -> LookRight r')) + +-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c)) +instance (N R l k kv r ~ g, BalanceableHelper (ShouldBalance t3 g) t3 z zv g) => + BalanceableHelperL True t1 y yv (N R (N B t2 u uv t3) z zv (N B l k kv r)) where + type BalL' True t1 y yv (N R (N B t2 u uv t3) z zv (N B l k kv r)) = + N R (N B t1 y yv t2) u uv (Balance t3 z zv (N R l k kv r)) + balLR' (Node left1 v1 (Node (Node left2 v2 right2) vx (Node left3 v3 right3))) = + Node (Node left1 v1 left2) v2 (balanceR @_ @t3 @z @zv @(N R l k kv r) (Node right2 vx (Node left3 v3 right3))) + balLV' v = case v of LookLeft left1 -> LookLeft (LookLeft left1) + Here v1 -> LookLeft (Here v1) + LookRight (LookLeft (LookLeft left2)) -> LookLeft (LookRight left2) + LookRight (LookLeft (Here v2)) -> Here v2 + LookRight (LookLeft (LookRight right2)) -> LookRight (balanceV @_ @t3 @z @zv @(N R l k kv r) (LookLeft right2)) + LookRight (Here vx) -> LookRight (balanceV @_ @t3 @z @zv @(N R l k kv r) (Here vx)) + LookRight (LookRight rr) -> LookRight (balanceV @_ @t3 @z @zv @(N R l k kv r) (LookRight (case rr of + LookLeft left3 -> LookLeft left3 + Here v3 -> Here v3 + LookRight right3 -> LookRight right3))) + + +-- balright :: RB a -> a -> RB a -> RB a +-- balright a x (T R b y c) = T R a x (T B b y c) +-- balright (T B a x b) y bl = balance (T R a x b) y bl +-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) +type family DiscriminateBalR (l :: Map k v) (r :: Map k v) :: Bool where + DiscriminateBalR _ (N R _ _ _ _) = False + DiscriminateBalR _ _ = True + +class BalanceableR (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where + type BalR l k v r :: Map Symbol q + balRR :: Record f (N color l k v r) -> Record f (BalR l k v r) + balRV :: Variant f (N color l k v r) -> Variant f (BalR l k v r) + +class BalanceableHelperR (b :: Bool) (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where + type BalR' b l k v r :: Map Symbol q + balRR' :: Record f (N color l k v r) -> Record f (BalR' b l k v r) + balRV' :: Variant f (N color l k v r) -> Variant f (BalR' b l k v r) + +instance (DiscriminateBalR l r ~ b, BalanceableHelperR b l k v r) => BalanceableR l k v r where + type BalR l k v r = BalR' (DiscriminateBalR l r) l k v r + balRR = balRR' @_ @b @l @k @v @r + balRV = balRV' @_ @b @l @k @v @r + +-- balright :: RB a -> a -> RB a -> RB a +-- balright a x (T R b y c) = T R a x (T B b y c) +instance BalanceableHelperR False right2 k2 v2 (N R left1 k1 v1 right1) where + type BalR' False right2 k2 v2 (N R left1 k1 v1 right1) = + (N R right2 k2 v2 (N B left1 k1 v1 right1)) + balRR' (Node right v (Node left' v' right')) = Node right v (Node left' v' right') + balRV' v = case v of LookLeft x -> LookLeft x + Here x -> Here x + LookRight x -> LookRight (case x of LookLeft y -> LookLeft y + Here y -> Here y + LookRight y -> LookRight y) + +-- balright (T B a x b) y bl = balance (T R a x b) y bl +instance (N R t2 z zv t3 ~ g, ShouldBalance g t1 ~ shouldbalance, BalanceableHelper shouldbalance g y yv t1) => + BalanceableHelperR True (N B t2 z zv t3) y yv t1 where + type BalR' True (N B t2 z zv t3) y yv t1 + = Balance (N R t2 z zv t3) y yv t1 + balRR' (Node (Node left1 v1 right1) v2 right2) = balanceR @_ @(N R t2 z zv t3) @y @yv @t1 + (Node (Node left1 v1 right1) v2 right2) + balRV' v = balanceV @_ @(N R t2 z zv t3) @y @yv @t1 (case v of + LookLeft l -> LookLeft (case l of + LookLeft l' -> LookLeft l' + Here x' -> Here x' + LookRight r' -> LookRight r') + Here x -> Here x + LookRight r -> LookRight r) + +-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) +instance (N R t2 u uv t3 ~ g, ShouldBalance g l ~ shouldbalance, BalanceableHelper shouldbalance g z zv l) => + BalanceableHelperR True (N R (N B t2 u uv t3) z zv (N B l k kv r)) y yv t1 where + type BalR' True (N R (N B t2 u uv t3) z zv (N B l k kv r)) y yv t1 = + N R (Balance (N R t2 u uv t3) z zv l) k kv (N B r y yv t1) + balRR' (Node (Node (Node left2 v2 right2) vx (Node left3 v3 right3)) v1 left1) = + Node (balanceR @_ @(N R t2 u uv t3) @z @zv @l (Node (Node left2 v2 right2) vx left3)) v3 (Node right3 v1 left1) + balRV' v = case v of + LookLeft (LookLeft rr) -> LookLeft (balanceV @_ @(N R t2 u uv t3) @z @zv @l (LookLeft (case rr of + LookLeft t2 -> LookLeft t2 + Here uv -> Here uv + LookRight t3 -> LookRight t3))) + LookLeft (Here zv) -> LookLeft (balanceV @_ @(N R t2 u uv t3) @z @zv @l (Here zv)) + LookLeft (LookRight (LookLeft l)) -> LookLeft (balanceV @_ @(N R t2 u uv t3) @z @zv @l (LookRight l)) + LookLeft (LookRight (Here kv)) -> Here kv + LookLeft (LookRight (LookRight r)) -> LookRight (LookLeft r) + Here yv -> LookRight (Here yv) + LookRight t1 -> LookRight (LookRight t1) + +-- app :: RB a -> RB a -> RB a +-- app E x = x +-- app x E = x +-- app (T R a x b) (T R c y d) = +-- case app b c of +-- T R b' z c' -> T R(T R a x b') z (T R c' y d) +-- bc -> T R a x (T R bc y d) +-- app (T B a x b) (T B c y d) = +-- case app b c of +-- T R b' z c' -> T R(T B a x b') z (T B c' y d) +-- bc -> balleft a x (T B bc y d) +-- app a (T R b x c) = T R (app a b) x c +-- app (T R a x b) c = T R a x (app b c) + + +class Fuseable (l :: Map Symbol q) (r :: Map Symbol q) where + type Fuse l r :: Map Symbol q + fuseRecord :: Record f l -> Record f r -> Record f (Fuse l r) + fuseVariant :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r) + +instance Fuseable E E where + type Fuse E E = E + fuseRecord _ _ = unit + fuseVariant v = case v of + +-- app E x = x +instance Fuseable E (N color left k v right) where + type Fuse E (N color left k v right) = N color left k v right + fuseRecord _ r = r + fuseVariant e = case e of + Right v -> v + +-- app x E = x +instance Fuseable (N color left k v right) E where + type Fuse (N color left k v right) E = N color left k v right + fuseRecord r _ = r + fuseVariant e = case e of + Left v -> v + +-- app a (T R b x c) = T R (app a b) x c +instance Fuseable (N B left1 k1 v1 right1) left2 + => Fuseable (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) where + type Fuse (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R (Fuse (N B left1 k1 v1 right1) left2) k2 v2 right2 + fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node (fuseRecord @_ @(N B left1 k1 v1 right1) (Node left1 v1 right1) left2) v2 right2 + fuseVariant e = case e of + Left l -> case l of + LookLeft left1 -> LookLeft (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Left (LookLeft left1))) + Here v1 -> LookLeft (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Left (Here v1))) + LookRight right1 -> LookLeft (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Left (LookRight right1))) + Right r -> case r of + LookLeft left2 -> LookLeft (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Right left2)) + Here v2 -> Here v2 + LookRight right2 -> LookRight right2 + + +-- app (T R a x b) c = T R a x (app b c) +instance Fuseable right1 (N B left2 k2 v2 right2) + => Fuseable (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) where + type Fuse (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) = N R left1 k1 v1 (Fuse right1 (N B left2 k2 v2 right2)) + fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (fuseRecord @_ @_ @(N B left2 k2 v2 right2) right1 (Node left2 v2 right2)) + fuseVariant e = case e of + Left l -> case l of + LookLeft left1 -> LookLeft left1 + Here v1 -> Here v1 + LookRight right1 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Left right1)) + Right r -> case r of + LookLeft left2 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Right (LookLeft left2))) + Here v2 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Right (Here v2))) + LookRight right2 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Right (LookRight right2))) + + +-- app (T R a x b) (T R c y d) = +instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper1 fused (N R left1 k1 v1 right1) (N R left2 k2 v2 right2)) + => Fuseable (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where + type Fuse (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = Fuse1 (Fuse right1 left2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) + fuseRecord = fuseRecord1 @_ @(Fuse right1 left2) + fuseVariant = fuseVariant1 @_ @(Fuse right1 left2) + +class FuseableHelper1 (fused :: Map Symbol q) (l :: Map Symbol q) (r :: Map Symbol q) where + type Fuse1 fused l r :: Map Symbol q + fuseRecord1 :: Record f l -> Record f r -> Record f (Fuse l r) + fuseVariant1 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r) + +-- app (T R a x b) (T R c y d) = +-- case app b c of +-- T R b' z c' -> T R (T R a x b') z (T R c' y d) +-- FIXME: The Fuseable constraint is repeated from avobe :( +instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z zv s2) + => FuseableHelper1 (N R s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where + type Fuse1 (N R s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R (N R left1 k1 v1 s1) z zv (N R s2 k2 v2 right2) + fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) = + case fuseRecord right1 left2 of + Node s1 zv s2 -> Node (Node left1 v1 s1) zv (Node s2 v2 right2) + fuseVariant1 e = + case e of + Left l -> case l of + LookLeft left1 -> LookLeft (LookLeft left1) + Here v1 -> LookLeft (Here v1) + LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of + LookLeft s1 -> LookLeft (LookRight s1) + Here zv -> Here zv + LookRight s2 -> LookRight (LookLeft s2) + Right r -> case r of + LookLeft left2 -> case fuseVariant @_ @right1 @left2 (Right left2) of + LookLeft s1 -> LookLeft (LookRight s1) + Here zv -> Here zv + LookRight s2 -> LookRight (LookLeft s2) + Here v2 -> LookRight (Here v2) + LookRight right2 -> LookRight (LookRight right2) + + +-- app (T R a x b) (T R c y d) = +-- case app b c of +-- ... +-- bc -> T R a x (T R bc y d) +-- FIXME: The Fuseable constraint is repeated from above :( +instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z zv s2) + => FuseableHelper1 (N B s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where + type Fuse1 (N B s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R left1 k1 v1 (N R (N B s1 z zv s2) k2 v2 right2) + fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) = + case fuseRecord right1 left2 of + Node s1 zv s2 -> Node left1 v1 (Node (Node s1 zv s2) v2 right2) + fuseVariant1 e = + case e of + Left l -> case l of + LookLeft left1 -> LookLeft left1 + Here v1 -> Here v1 + LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of + LookLeft s1 -> LookRight (LookLeft (LookLeft s1)) + Here zv -> LookRight (LookLeft (Here zv)) + LookRight s2 -> LookRight (LookLeft (LookRight s2)) + Right r -> case r of + LookLeft left2 -> case fuseVariant @_ @right1 @left2 (Right left2) of + LookLeft s1 -> LookRight (LookLeft (LookLeft s1)) + Here zv -> LookRight (LookLeft (Here zv)) + LookRight s2 -> LookRight (LookLeft (LookRight s2)) + Here v2 -> LookRight (Here v2) + LookRight right2 -> LookRight (LookRight right2) + +-- app (T R a x b) (T R c y d) = +-- case app b c of +-- ... +-- bc -> T R a x (T R bc y d) +instance FuseableHelper1 E (N R left1 k1 v1 E) (N R E k2 v2 right2) where + type Fuse1 E (N R left1 k1 v1 E) (N R E k2 v2 right2) = N R left1 k1 v1 (N R E k2 v2 right2) + fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (Node Empty v2 right2) + fuseVariant1 e = + case e of + Left l -> case l of + LookLeft left1 -> LookLeft left1 + Here v1 -> Here v1 + Right r -> case r of + Here v2 -> LookRight (Here v2) + LookRight right2 -> LookRight (LookRight right2) + +-- app (T B a x b) (T B c y d) = +instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper2 fused (N B left1 k1 v1 right1) (N B left2 k2 v2 right2)) + => Fuseable (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where + type Fuse (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = Fuse2 (Fuse right1 left2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) + fuseRecord = fuseRecord2 @_ @(Fuse right1 left2) + fuseVariant = fuseVariant2 @_ @(Fuse right1 left2) + +-- could FuseableHelper1 and FuseableHelper2 be, well... fused? +class FuseableHelper2 (fused :: Map Symbol q) (l :: Map Symbol q) (r :: Map Symbol q) where + type Fuse2 fused l r :: Map Symbol q + fuseRecord2 :: Record f l -> Record f r -> Record f (Fuse l r) + fuseVariant2 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r) + +-- app (T B a x b) (T B c y d) = +-- case app b c of +-- T R b' z c' -> T R (T B a x b') z (T B c' y d) +instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z zv s2) + => FuseableHelper2 (N R s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where + type Fuse2 (N R s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = N R (N B left1 k1 v1 s1) z zv (N B s2 k2 v2 right2) + fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) = + case fuseRecord right1 left2 of + Node s1 zv s2 -> Node (Node left1 v1 s1) zv (Node s2 v2 right2) + fuseVariant2 e = + case e of + Left l -> case l of + LookLeft left1 -> LookLeft (LookLeft left1) + Here v1 -> LookLeft (Here v1) + LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of + LookLeft s1 -> LookLeft (LookRight s1) + Here zv -> Here zv + LookRight s2 -> LookRight (LookLeft s2) + Right r -> case r of + LookLeft left2 -> case fuseVariant @_ @right1 @left2 (Right left2) of + LookLeft s1 -> LookLeft (LookRight s1) + Here zv -> Here zv + LookRight s2 -> LookRight (LookLeft s2) + Here v2 -> LookRight (Here v2) + LookRight right2 -> LookRight (LookRight right2) + +-- app (T B a x b) (T B c y d) = +-- case app b c of +-- ... +-- bc -> balleft a x (T B bc y d) +instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z zv s2, BalanceableL left1 k1 v1 (N B (N B s1 z zv s2) k2 v2 right2)) + => FuseableHelper2 (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where + type Fuse2 (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = BalL left1 k1 v1 (N B (N B s1 z zv s2) k2 v2 right2) + fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) = + case fuseRecord @_ @right1 @left2 right1 left2 of + Node s1 zv s2 -> balLR @_ @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (Node left1 v1 (Node (Node s1 zv s2) v2 right2)) + fuseVariant2 e = balLV @_ @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (case e of + Left l -> case l of + LookLeft left1 -> LookLeft left1 + Here v1 -> Here v1 + LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of + LookLeft s1 -> LookRight (LookLeft (LookLeft s1)) + Here zv -> LookRight (LookLeft (Here zv)) + LookRight s2 -> LookRight (LookLeft (LookRight s2)) + Right r -> case r of + LookLeft left2 -> case fuseVariant @_ @right1 @left2 (Right left2) of + LookLeft s1 -> LookRight (LookLeft (LookLeft s1)) + Here zv -> LookRight (LookLeft (Here zv)) + LookRight s2 -> LookRight (LookLeft (LookRight s2)) + Here v2 -> LookRight (Here v2) + LookRight right2 -> LookRight (LookRight right2)) + +-- app (T B a x b) (T B c y d) = +-- case app b c of +-- ... +-- bc -> balleft a x (T B bc y d) +instance (BalanceableL left1 k1 v1 (N B E k2 v2 right2)) + => FuseableHelper2 E (N B left1 k1 v1 E) (N B E k2 v2 right2) where + type Fuse2 E (N B left1 k1 v1 E) (N B E k2 v2 right2) = BalL left1 k1 v1 (N B E k2 v2 right2) + fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) = + balLR @_ @left1 @k1 @v1 @(N B E k2 v2 right2) (Node left1 v1 (Node Empty v2 right2)) + fuseVariant2 e = balLV @_ @left1 @k1 @v1 @(N B E k2 v2 right2) (case e of + Left l -> case l of + LookLeft left1 -> LookLeft left1 + Here v1 -> Here v1 + Right r -> case r of + Here v2 -> LookRight (Here v2) + LookRight right2 -> LookRight (LookRight right2)) + + +-- del E = E +-- del (T _ a y b) +-- | xy = delformRight a y b +-- | otherwise = app a b +class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where + type Del k v t :: Map Symbol q + del :: Record f t -> Record f (Del k v t) + win :: Variant f t -> Either (Variant f (Del k v t)) (f v) + +-- delformLeft a@(T B _ _ _) y b = balleft (del a) y b +-- delformLeft a y b = T R (del a) y b +-- In the term-level code, the k to delete is already on the environment. +class DelableL (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where + type DelL k v l kx vx r :: Map Symbol q + delL :: Record f (N color l kx vx r) -> Record f (DelL k v l kx vx r) + winL :: Variant f (N color l kx vx r) -> Either (Variant f (DelL k v l kx vx r)) (f v) + +-- delformLeft a@(T B _ _ _) y b = balleft (del a) y b +instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableL deleted kx vx right) + => DelableL k v (N B leftz kz vz rightz) kx vx right where + type DelL k v (N B leftz kz vz rightz) kx vx right = BalL (Del k v (N B leftz kz vz rightz)) kx vx right + delL (Node left vx right) = balLR @_ @(Del k v (N B leftz kz vz rightz)) @kx @vx @right (Node (del @_ @k @v left) vx right) + winL v = first (balLV @_ @(Del k v (N B leftz kz vz rightz)) @kx @vx @right) (case v of + LookLeft l -> first LookLeft (win @_ @k @v l) + Here vx -> Left $ Here vx + LookRight r -> Left $ LookRight r) + +-- delformLeft a y b = T R (del a) y b +instance (Delable k v (N R leftz kz vz rightz)) + => DelableL k v (N R leftz kz vz rightz) kx vx right where + type DelL k v (N R leftz kz vz rightz) kx vx right = N R (Del k v (N R leftz kz vz rightz)) kx vx right + delL (Node left vx right) = Node (del @_ @k @v left) vx right + winL v = case v of + LookLeft l -> first LookLeft (win @_ @k @v l) + Here vx -> Left (Here vx) + LookRight r -> Left (LookRight r) + +-- delformLeft a y b = T R (del a) y b +instance DelableL k v E kx vx right where + type DelL k v E kx vx right = N R E kx vx right + delL (Node left vx right) = Node Empty vx right + winL v = case v of + Here vx -> Left (Here vx) + LookRight r -> Left (LookRight r) + +-- delformRight a y b@(T B _ _ _) = balright a y (del b) +-- delformRight a y b = T R a y (del b) +class DelableR (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where + type DelR k v l kx vx r :: Map Symbol q + delR :: Record f (N color l kx vx r) -> Record f (DelR k v l kx vx r) + winR :: Variant f (N color l kx vx r) -> Either (Variant f (DelR k v l kx vx r)) (f v) + +-- delformRight a y b@(T B _ _ _) = balright a y (del b) +instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableR left kx vx deleted) + => DelableR k v left kx vx (N B leftz kz vz rightz) where + type DelR k v left kx vx (N B leftz kz vz rightz) = BalR left kx vx (Del k v (N B leftz kz vz rightz)) + delR (Node left vx right) = balRR @_ @left @kx @vx @(Del k v (N B leftz kz vz rightz)) (Node left vx (del @_ @k @v right)) + winR v = first (balRV @_ @left @kx @vx @(Del k v (N B leftz kz vz rightz))) (case v of + LookLeft l -> Left $ LookLeft l + Here vx -> Left $ Here vx + LookRight r -> first LookRight (win @_ @k @v r)) + +-- delformRight a y b = T R a y (del b) +instance (Delable k v (N R leftz kz vz rightz)) + => DelableR k v left kx vx (N R leftz kz vz rightz) where + type DelR k v left kx vx (N R leftz kz vz rightz) = N R left kx vx (Del k v (N R leftz kz vz rightz)) + delR (Node left vx right) = Node left vx (del @_ @k @v right) + winR v = case v of + LookLeft l -> Left (LookLeft l) + Here vx -> Left (Here vx) + LookRight r -> first LookRight (win @_ @k @v r) + +-- delformRight a y b = T R a y (del b) +instance DelableR k v left kx vx E where + type DelR k v left kx vx E = N R left kx vx E + delR (Node left vx right) = Node left vx Empty + winR v = case v of + LookLeft l -> Left (LookLeft l) + Here vx -> Left (Here vx) + +-- del E = E +instance Delable k v E where + type Del k v E = E + del _ = unit + win = impossible + +-- the color is discarded +-- del (T _ a y b) +-- | xy = delformRight a y b +-- | otherwise = app a b +instance (CmpSymbol kx k ~ ordering, DelableHelper ordering k v left kx vx right) => Delable k v (N color left kx vx right) where + type Del k v (N color left kx vx right) = Del' (CmpSymbol kx k) k v left kx vx right + del = del' @_ @(CmpSymbol kx k) @k @v @left @kx @vx @right + win = win' @_ @(CmpSymbol kx k) @k @v @left @kx @vx @right + +class DelableHelper (ordering :: Ordering) (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where + type Del' ordering k v l kx vx r :: Map Symbol q + del' :: Record f (N color l kx vx r) -> Record f (Del' ordering k v l kx vx r) + win' :: Variant f (N color l kx vx r) -> Either (Variant f (Del' ordering k v l kx vx r)) (f v) + +-- | x DelableHelper GT k v left kx vx right where + type Del' GT k v left kx vx right = DelL k v left kx vx right + del' = delL @_ @k @v @left @kx @vx @right + win' = winL @_ @k @v @left @kx @vx @right + +-- | otherwise = app a b +instance Fuseable left right => DelableHelper EQ k v left k v right where + type Del' EQ k v left k v right = Fuse left right + del' (Node left _ right) = fuseRecord @_ @left @right left right + win' v = case v of + LookLeft l -> Left $ fuseVariant @_ @left @right (Left l) + Here v -> Right v + LookRight r -> Left $ fuseVariant @_ @left @right (Right r) + +-- | x>y = delformRight a y b +instance DelableR k v left kx vx right => DelableHelper LT k v left kx vx right where + type Del' LT k v left kx vx right = DelR k v left kx vx right + del' = delR @_ @k @v @left @kx @vx @right + win' = winR @_ @k @v @left @kx @vx @right + +{- | Class that determines if the pair of a 'Symbol' key and a type can + be deleted from a type-level map. + + The associated type family 'Delete' produces the resulting map. + + At the term level, this manifests in 'delete', which removes a field from + a record, and in 'winnow', which checks if a 'Variant' is of a given + branch and returns the value in the branch if there's a match, or a + reduced 'Variant' if there isn't. 'winnow' tends to be more useful in + practice. + + If the map already has the key but with a /different/ type, the deletion + fails to compile. + -} +class Deletable (k :: Symbol) (v :: q) (t :: Map Symbol q) where + type Delete k v t :: Map Symbol q + _delete :: Record f t -> Record f (Delete k v t) + _winnow :: Variant f t -> Either (Variant f (Delete k v t)) (f v) + +instance (Delable k v t, Del k v t ~ deleted, CanMakeBlack deleted) => Deletable k v t where + type Delete k v t = MakeBlack (Del k v t) + _delete r = makeBlackR (del @_ @k @v r) + _winnow v = first makeBlackV (win @_ @k @v v) + +{- | + Removes a field from a 'Record'. + -} +delete :: forall k v t f . Deletable k v t => Record f t -> Record f (Delete k v t) +delete = _delete @_ @k @v @t + +{- | + Checks if a 'Variant' is of a given branch and returns the value in the + branch if there's a match, or a reduced 'Variant' if there isn't. + -} +winnow :: forall k v t f . Deletable k v t => Variant f t -> Either (Variant f (Delete k v t)) (f v) +winnow = _winnow @_ @k @v @t + +{- | Like 'winnow' but specialized to pure 'Variant's. + +>>> winnow @"bar" @Bool (injectI @"bar" False :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) +Right (I False) + +>>> prettyShow_VariantI `first` winnow @"foo" @Char (injectI @"bar" False :: Variant I (Insert "foo" Char (Insert "bar" Bool Empty))) +Left "bar (False)" + +-} +winnowI :: forall k v t . Deletable k v t => Variant I t -> Either (Variant I (Delete k v t)) v +winnowI = fmap unI . winnow @k @v @t + +-- The original term-level code, taken from: +-- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html +-- +-- {- Version 1, 'untyped' -} +-- data Color = R | B deriving Show +-- data RB a = E | T Color (RB a) a (RB a) deriving Show +-- +-- {- Insertion and membership test as by Okasaki -} +-- insert :: Ord a => a -> RB a -> RB a +-- insert x s = +-- T B a z b +-- where +-- T _ a z b = ins s +-- ins E = T R E x E +-- ins s@(T B a y b) +-- | xy = balance a y (ins b) +-- | otherwise = s +-- ins s@(T R a y b) +-- | xy = T R a y (ins b) +-- | otherwise = s +-- +-- +-- {- balance: first equation is new, +-- to make it work with a weaker invariant -} +-- balance :: RB a -> a -> RB a -> RB a +-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d) +-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) +-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) +-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) +-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) +-- balance a x b = T B a x b +-- +-- member :: Ord a => a -> RB a -> Bool +-- member x E = False +-- member x (T _ a y b) +-- | xy = member x b +-- | otherwise = True +-- +-- {- deletion a la SMK -} +-- delete :: Ord a => a -> RB a -> RB a +-- delete x t = +-- case del t of {T _ a y b -> T B a y b; _ -> E} +-- where +-- del E = E +-- del (T _ a y b) +-- | xy = delformRight a y b +-- | otherwise = app a b +-- delformLeft a@(T B _ _ _) y b = balleft (del a) y b +-- delformLeft a y b = T R (del a) y b +-- +-- delformRight a y b@(T B _ _ _) = balright a y (del b) +-- delformRight a y b = T R a y (del b) +-- +-- balleft :: RB a -> a -> RB a -> RB a +-- balleft (T R a x b) y c = T R (T B a x b) y c +-- balleft bl x (T B a y b) = balance bl x (T R a y b) +-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c)) +-- +-- balright :: RB a -> a -> RB a -> RB a +-- balright a x (T R b y c) = T R a x (T B b y c) +-- balright (T B a x b) y bl = balance (T R a x b) y bl +-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl) +-- +-- sub1 :: RB a -> RB a +-- sub1 (T B a x b) = T R a x b +-- sub1 _ = error "invariance violation" +-- +-- app :: RB a -> RB a -> RB a +-- app E x = x +-- app x E = x +-- app (T R a x b) (T R c y d) = +-- case app b c of +-- T R b' z c' -> T R (T R a x b') z (T R c' y d) +-- bc -> T R a x (T R bc y d) +-- app (T B a x b) (T B c y d) = +-- case app b c of +-- T R b' z c' -> T R(T B a x b') z (T B c' y d) +-- bc -> balleft a x (T B bc y d) +-- app a (T R b x c) = T R (app a b) x c +-- app (T R a x b) c = T R a x (app b c) + diff --git a/lib/Data/RBR/Subset.hs b/lib/Data/RBR/Subset.hs new file mode 100644 --- /dev/null +++ b/lib/Data/RBR/Subset.hs @@ -0,0 +1,208 @@ +{-| + This module contains versions of functions from 'Data.RBR', generalized to + work with a subset of the fields of a 'Record' or the branches of a + 'Variant'. + + __Edit:__ There are functions of the same name in the 'Data.RBR' module, + but they are deprecated. The functions from this module should be used + instead, preferably qualified. The changes have to do mainly with the + required constraints. +-} +{-# LANGUAGE DataKinds, + TypeOperators, + ConstraintKinds, + PolyKinds, + TypeFamilies, + GADTs, + MultiParamTypeClasses, + FunctionalDependencies, + FlexibleInstances, + FlexibleContexts, + UndecidableInstances, + UndecidableSuperClasses, + TypeApplications, + ScopedTypeVariables, + AllowAmbiguousTypes, + ExplicitForAll, + RankNTypes, + DefaultSignatures, + PartialTypeSignatures, + LambdaCase, + EmptyCase +#-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} +module Data.RBR.Subset ( + Subset, + fieldSubset, + projectSubset, + getFieldSubset, + setFieldSubset, + modifyFieldSubset, + branchSubset, + injectSubset, + matchSubset, + eliminateSubset, + fromRecordSuperset + ) where + +import Data.Proxy +import Data.Kind +import Data.Monoid (Endo(..)) +import GHC.TypeLits +import Data.SOP (K(..),I(..)) + +import Data.RBR.Internal hiding + ( + ProductlikeSubset, + fieldSubset, + projectSubset, + getFieldSubset, + setFieldSubset, + modifyFieldSubset, + SumlikeSubset, + branchSubset, + injectSubset, + matchSubset, + eliminateSubset + ) + +{- $setup + +>>> :set -XDataKinds -XTypeApplications -XPartialTypeSignatures -XFlexibleContexts -XTypeFamilies -XDeriveGeneric +>>> :set -Wno-partial-type-signatures +>>> import Data.RBR +>>> import qualified Data.RBR.Subset as S +>>> import Data.SOP +>>> import GHC.Generics + +-} + +{- | A map is a subset of another if all of its entries are present in the other map. + +-} +type Subset (subset :: Map Symbol q) (whole :: Map Symbol q) = KeysValuesAll (PresentIn whole) subset + + +{- | Like 'field', but targets multiple fields at the same time + +-} +fieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) + => Record f whole -> (Record f subset -> Record f whole, Record f subset) +fieldSubset r = + (,) + (let goset :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left, + KeysValuesAll (PresentIn whole) right) + => Record (SetField f (Record f whole)) left + -> Record (SetField f (Record f whole)) right + -> Record (SetField f (Record f whole)) (N color left k v right) + goset left right = Node left (SetField (\v w -> fst (field @k @whole w) v)) right + setters :: Record (SetField f (Record f whole)) _ = cpara_Map (Proxy @(PresentIn whole)) unit goset + appz (SetField func) fv = K (Endo (func fv)) + in \toset -> appEndo (collapse'_Record (liftA2_Record appz setters toset)) r) + (let goget :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left, + KeysValuesAll (PresentIn whole) right) + => Record f left + -> Record f right + -> Record f (N color left k v right) + goget left right = Node left (project @k @whole r) right + in cpara_Map (Proxy @(PresentIn whole)) unit goget) + + + + +{- | Like 'project', but extracts multiple fields at the same time. + + The types in the subset tree can often be inferred and left as wildcards in type signature. + +>>> prettyShow_RecordI $ S.projectSubset @(Insert "foo" _ (Insert "bar" _ Empty)) (insertI @"foo" 'a' (insertI @"bar" True (insertI @"baz" (Just ()) unit))) +"{bar = True, foo = 'a'}" + + Can also be used to convert between 'Record's with structurally dissimilar + type-level maps that nevertheless hold the same entries. +-} +projectSubset :: forall subset whole f. (Maplike subset, Subset subset whole) + => Record f whole + -> Record f subset +projectSubset = snd . fieldSubset + +{- | Alias for 'projectSubset'. +-} +getFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) + => Record f whole + -> Record f subset +getFieldSubset = projectSubset + +{- | Like 'setField', but sets multiple fields at the same time. + +-} +setFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) + => Record f subset + -> Record f whole + -> Record f whole +setFieldSubset subset whole = fst (fieldSubset whole) subset + +{- | Like 'modifyField', but modifies multiple fields at the same time. + +-} +modifyFieldSubset :: forall subset whole f. (Maplike subset, Subset subset whole) + => (Record f subset -> Record f subset) + -> Record f whole + -> Record f whole +modifyFieldSubset f r = uncurry ($) (fmap f (fieldSubset @subset @whole r)) + + +{- | Like 'branch', but targets multiple branches at the same time. +-} +branchSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole) + => (Variant f whole -> Maybe (Variant f subset), Variant f subset -> Variant f whole) +branchSubset = + let inj2case = \adapt (VariantInjection vif) -> Case $ \fv -> adapt (vif fv) -- (\fv -> adapt (fromNS @t (unK (apFn fn fv)))) + -- The intuition is that getting the setter and the getter together might be faster at compile-time. + -- The intuition might be wrong. + subs :: forall f. Record f whole -> (Record f subset -> Record f whole, Record f subset) + subs = fieldSubset @subset @whole + in + (,) + (let injs :: Record (Case f (Maybe (Variant f subset))) subset + injs = liftA_Record (inj2case Just) (injections_Variant @subset) + -- fixme: possibly inefficient? + wholeinjs :: Record (Case f (Maybe (Variant f subset))) whole + wholeinjs = pure_Record (Case (\_ -> Nothing)) + mixedinjs = fst (subs wholeinjs) injs + in eliminate_Variant mixedinjs) + (let wholeinjs :: Record (Case f (Variant f whole)) whole + wholeinjs = liftA_Record (inj2case id) (injections_Variant @whole) + injs = snd (subs wholeinjs) + in eliminate_Variant injs) + +{- | Like 'inject', but injects one of several possible branches. + + Can also be used to convert between 'Variant's with structurally + dissimilar type-level maps that nevertheless hold the same entries. +-} +injectSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole) + => Variant f subset -> Variant f whole +injectSubset = snd (branchSubset @subset @whole) + +{- | Like 'match', but matches more than one branch. +-} +matchSubset :: forall subset whole f. (Maplike subset, Maplike whole, Subset subset whole) + => Variant f whole -> Maybe (Variant f subset) +matchSubset = fst (branchSubset @subset @whole) + +{- | + Like 'eliminate', but allows the eliminator 'Record' to have more fields + than there are branches in the 'Variant'. +-} +eliminateSubset :: forall subset whole f r. (Maplike subset, Maplike whole, Subset subset whole) + => Record (Case f r) whole -> Variant f subset -> r +eliminateSubset cases = + let reducedCases = getFieldSubset @subset @whole cases + in eliminate_Variant reducedCases + +{- | + A common composition of 'fromRecord' and 'projectSubset'. +-} +fromRecordSuperset :: forall r t whole. (IsRecordType r t, Maplike t, Subset t whole) => Record I whole -> r +fromRecordSuperset = fromRecord . projectSubset + diff --git a/red-black-record.cabal b/red-black-record.cabal --- a/red-black-record.cabal +++ b/red-black-record.cabal @@ -1,77 +1,78 @@ -cabal-version: 2.0 -name: red-black-record -version: 2.1.0.3 -synopsis: Extensible records and variants indexed by a type-level Red-Black tree. - -description: A library that provides extensible records and variants, - both indexed by a type-level red-black tree that maps - Symbol keys to value types of any kind. - . - The keys correspond to fields - names in records, and to branch names in variants. - . - At the term level, value types come wrapped in a type - constructor of kind @q -> Type@, where @q@ is the kind of - value types. - . - The records and variants can be converted to and from - regular Haskell datatypes; also to and from the unlabelled - n-ary products and sums of the @sop-core@ package. - -license: BSD3 -license-file: LICENSE -author: Daniel Diaz -maintainer: diaz_carrete@yahoo.com -category: Data -extra-source-files: CHANGELOG.md, - README.md -build-type: Simple - -source-repository head - type: git - location: https://github.com/danidiaz/red-black-record.git - -library - exposed-modules: Data.RBR - Data.RBR.Internal - Data.RBR.Examples - build-depends: base >= 4.10.0.0 && < 5, - sop-core >= 0.4.0.0 && < 0.6 - hs-source-dirs: lib - default-language: Haskell2010 - -library demoted - exposed-modules: Data.RBR.Demoted - build-depends: base >= 4.10.0.0 && < 5, - sop-core >= 0.4.0.0 && < 0.6, - red-black-record - hs-source-dirs: lib-demoted - default-language: Haskell2010 - -test-suite doctests - type: exitcode-stdio-1.0 - hs-source-dirs: tests - ghc-options: -threaded - main-is: doctests.hs - build-depends: base >= 4.10.0.0 && < 5, - sop-core >= 0.4.0.0 && < 0.6, - red-black-record, - aeson >= 1.4.0.0 && < 1.5, - bytestring >= 0.10, - text >= 1.1, - profunctors >= 5, - doctest >= 0.16.2 - default-language: Haskell2010 - -test-suite tests - type: exitcode-stdio-1.0 - hs-source-dirs: tests - main-is: tests.hs - build-depends: - base >= 4.10.0.0 && < 5, - sop-core >= 0.4.0.0 && < 0.6, - tasty >= 0.10.1.1, - tasty-hunit >= 0.9.2, - red-black-record, - demoted - default-language: Haskell2010 +cabal-version: 2.0 +name: red-black-record +version: 2.1.1.0 +synopsis: Extensible records and variants indexed by a type-level Red-Black tree. + +description: A library that provides extensible records and variants, + both indexed by a type-level red-black tree that maps + Symbol keys to value types of any kind. + . + The keys correspond to fields + names in records, and to branch names in variants. + . + At the term level, value types come wrapped in a type + constructor of kind @q -> Type@, where @q@ is the kind of + value types. + . + The records and variants can be converted to and from + regular Haskell datatypes; also to and from the unlabelled + n-ary products and sums of the @sop-core@ package. + +license: BSD3 +license-file: LICENSE +author: Daniel Diaz +maintainer: diaz_carrete@yahoo.com +category: Data +extra-source-files: CHANGELOG.md, + README.md +build-type: Simple + +source-repository head + type: git + location: https://github.com/danidiaz/red-black-record.git + +library + exposed-modules: Data.RBR + Data.RBR.Subset + Data.RBR.Internal + Data.RBR.Examples + build-depends: base >= 4.10.0.0 && < 5, + sop-core >= 0.4.0.0 && < 0.6 + hs-source-dirs: lib + default-language: Haskell2010 + +library demoted + exposed-modules: Data.RBR.Demoted + build-depends: base >= 4.10.0.0 && < 5, + sop-core >= 0.4.0.0 && < 0.6, + red-black-record + hs-source-dirs: lib-demoted + default-language: Haskell2010 + +test-suite doctests + type: exitcode-stdio-1.0 + hs-source-dirs: tests + ghc-options: -threaded + main-is: doctests.hs + build-depends: base >= 4.10.0.0 && < 5, + sop-core >= 0.4.0.0 && < 0.6, + red-black-record, + aeson >= 1.4.0.0 && < 1.5, + bytestring >= 0.10, + text >= 1.1, + profunctors >= 5, + doctest >= 0.16.2 + default-language: Haskell2010 + +test-suite tests + type: exitcode-stdio-1.0 + hs-source-dirs: tests + main-is: tests.hs + build-depends: + base >= 4.10.0.0 && < 5, + sop-core >= 0.4.0.0 && < 0.6, + tasty >= 0.10.1.1, + tasty-hunit >= 0.9.2, + red-black-record, + demoted + default-language: Haskell2010 diff --git a/tests/doctests.hs b/tests/doctests.hs --- a/tests/doctests.hs +++ b/tests/doctests.hs @@ -1,7 +1,8 @@ -import Test.DocTest - -main = doctest ["-ilib", - "lib/Data/RBR.hs", - "lib/Data/RBR/Internal.hs", - "lib/Data/RBR/Examples.hs" - ] +import Test.DocTest + +main = doctest ["-ilib", + "lib/Data/RBR.hs", + "lib/Data/RBR/Subset.hs", + "lib/Data/RBR/Examples.hs", + "lib/Data/RBR/Internal.hs" + ] diff --git a/tests/tests.hs b/tests/tests.hs --- a/tests/tests.hs +++ b/tests/tests.hs @@ -1,555 +1,556 @@ -{-# LANGUAGE DataKinds, - TypeOperators, - TypeFamilies, - TypeApplications, - DeriveGeneric, - StandaloneDeriving, - UndecidableInstances, - KindSignatures, - PartialTypeSignatures, - FlexibleContexts, - ScopedTypeVariables -#-} -{-# OPTIONS_GHC -Wno-partial-type-signatures #-} -module Main where - -import Data.RBR -import Data.RBR.Demoted (emptyMap,DemotableMap(demoteMap),t_insert,t_delete) -import Data.SOP -import Data.SOP.NP (cpure_NP,collapse_NP) -import Data.Typeable -import Data.Proxy -import GHC.TypeLits -import Data.Kind -import GHC.Generics (Generic) - -import Test.Tasty -import Test.Tasty.HUnit (testCase,Assertion,assertEqual,assertBool) - - -main :: IO () -main = defaultMain tests - -tests :: TestTree -tests = testGroup "Tests" [ testCase "recordGetSet01" testRecordGetSet01, - testCase "variantInjectMatch01" testVariantInjectMatch01, - testCase "projectSubset01" testProjectSubset01, - testGroup "nominalConversion" [ - testCase "toRecord01" testToRecord01, - testCase "fromRecord01" testFromRecord01, - testCase "toVariant01" testToVariant01, - testCase "toVariant02Units" testToVariant02Units, - testCase "fromVariant01" testFromVariant01, - testCase "fromVariant02Units" testFromVariant02Units - ], - testGroup "deletion" [ - testGroup "records" [ - testCase "recordDeletionSingleElem" testRecordDeletionSingleElem, - testCase "recordDeletionLeftElem" testRecordDeletionLeftElem, - testCase "recordDeletionRightElem" testRecordDeletionRightElem - ], - testGroup "variants" [ - testCase "variantDeletionSingleElem" testVariantDeletionSingleElem, - testCase "variantDeletionLeftElem" testVariantDeletionLeftElem, - testCase "variantDeletionRightElem" testVariantDeletionRightElem, - testCase "variantDeletion3Elem" testVariantDeletion3Elem, - testCase "variantDeletionMany" testVariantDeletionMany, - testCase "variantDeletionManyB" testVariantDeletionManyB - ] - ], - testGroup "typeLevelTermLvel" [ - testCase "tandem01" testInTandem01, - testCase "tandem02" testInTandem02, - testCase "tandem03" testInTandem03, - testCase "tandem04" testInTandem04 - ], - testGroup "polyKindedMap" [ - testCase "polyKinded01" polyKinded01, - testCase "polyKinded02" polyKinded02 - ] - ] - - -testRecordGetSet01 :: Assertion -testRecordGetSet01 = do - let r = insertI @"bfoo" 'c' - . insertI @"bbar" True - . insertI @"bbaz" (1::Int) - . insertI @"afoo" 'd' - . insertI @"abar" False - . insertI @"abaz" (2::Int) - . insertI @"zfoo" 'x' - . insertI @"zbar" False - . insertI @"zbaz" (4::Int) - . insertI @"dfoo" 'z' - . insertI @"dbar" True - . insertI @"dbaz" (5::Int) - . insertI @"fbaz" (6::Int) - $ unit - s = setFieldI @"fbaz" 9 (setFieldI @"zfoo" 'k' r) - assertEqual "bfoo" (getFieldI @"bfoo" s) 'c' - assertEqual "bbar" (getFieldI @"bbar" s) True - assertEqual "bbaz" (getFieldI @"bbaz" s) (1::Int) - assertEqual "afoo" (getFieldI @"afoo" s) 'd' - assertEqual "abar" (getFieldI @"abar" s) False - assertEqual "abaz" (getFieldI @"abaz" s) (2::Int) - assertEqual "zfoo" (getFieldI @"zfoo" s) 'k' - assertEqual "zbar" (getFieldI @"zbar" s) False - assertEqual "zbaz" (getFieldI @"zbaz" s) (4::Int) - assertEqual "dfoo" (getFieldI @"dfoo" s) 'z' - assertEqual "dbar" (getFieldI @"dbar" s) True - assertEqual "dbaz" (getFieldI @"dbaz" s) (5::Int) - assertEqual "fbaz" (getFieldI @"fbaz" s) (9::Int) - return () - -type Tree01 = FromList [ '("bfoo",Char), - '("bbar",Bool), - '("bbaz",Int), - '("afoo",Char), - '("abar",Bool), - '("abaz",Int), - '("zfoo",Char), - '("zbar",Bool), - '("zbaz",Int), - '("dfoo",Char), - '("dbar",Bool), - '("dbaz",Int), - '("fbaz",Int), - '("kgoz",Int) ] - -testVariantInjectMatch01 :: Assertion -testVariantInjectMatch01 = do - let r0 = injectI @"bfoo" @Tree01 'c' - r1 = injectI @"bbar" @Tree01 True - r2 = injectI @"bbaz" @Tree01 (1::Int) - r3 = injectI @"afoo" @Tree01 'd' - r4 = injectI @"abar" @Tree01 False - r5 = injectI @"abaz" @Tree01 (2::Int) - r6 = injectI @"zfoo" @Tree01 'x' - r7 = injectI @"zbar" @Tree01 False - r8 = injectI @"zbaz" @Tree01 (4::Int) - r9 = injectI @"dfoo" @Tree01 'z' - r10 = injectI @"dbar" @Tree01 True - r11 = injectI @"dbaz" @Tree01 (5::Int) - r12 = injectI @"fbaz" @Tree01 (6::Int) - r13 = injectI @"kgoz" @Tree01 (9::Int) - assertEqual "bfoo" (matchI @"bfoo" r0 ) $ Just 'c' - assertEqual "bbar" (matchI @"bbar" r1 ) $ Just True - assertEqual "bbaz" (matchI @"bbaz" r2 ) $ Just (1::Int) - assertEqual "afoo" (matchI @"afoo" r3 ) $ Just 'd' - assertEqual "abar" (matchI @"abar" r4 ) $ Just False - assertEqual "abaz" (matchI @"abaz" r5 ) $ Just (2::Int) - assertEqual "zfoo" (matchI @"zfoo" r6 ) $ Just 'x' - assertEqual "zbar" (matchI @"zbar" r7 ) $ Just False - assertEqual "zbaz" (matchI @"zbaz" r8 ) $ Just (4::Int) - assertEqual "dfoo" (matchI @"dfoo" r9 ) $ Just 'z' - assertEqual "dbar" (matchI @"dbar" r10) $ Just True - assertEqual "dbaz" (matchI @"dbaz" r11) $ Just (5::Int) - assertEqual "fbaz" (matchI @"fbaz" r12) $ Just (6::Int) - assertEqual "kgoz" (matchI @"kgoz" r13) $ Just (9::Int) - return () - - -testProjectSubset01 :: Assertion -testProjectSubset01 = do - let r = insertI @"foo" 'c' - . insertI @"bar" True - . insertI @"baz" (1::Int) - $ unit - s = projectSubset @(FromList '[ '("bar",_), - '("baz",_) ]) r - bar = getFieldI @"bar" s - baz = getFieldI @"baz" s - assertEqual "bar" bar True - assertEqual "baz" baz 1 - -data Person = Person { name :: String, age :: Int, whatever :: Char } deriving (Generic,Eq,Show) - -instance ToRecord Person -instance FromRecord Person - -testToRecord01 :: Assertion -testToRecord01 = do - let r = toRecord (Person "Foo" 50 'z') - assertEqual "name" "Foo" (getFieldI @"name" r) - assertEqual "age" 50 (getFieldI @"age" r) - assertEqual "whatever" 'z' (getFieldI @"whatever" r) - -testFromRecord01 :: Assertion -testFromRecord01 = do - let r = insertI @"name" "Foo" - . insertI @"age" 50 - . insertI @"whatever" 'z' - $ unit - assertEqual "person" (Person "Foo" 50 'z') (fromRecord r) - -data Variant01 = Variant01A Int - | Variant01B Char - | Variant01C Bool - | Variant01D Bool - deriving (Generic,Eq,Show) - -instance ToVariant Variant01 -instance FromVariant Variant01 - -testToVariant01 :: Assertion -testToVariant01 = do - let val1 = Variant01A 0 - val2 = Variant01B 'c' - val3 = Variant01C True - cases = addCaseI @"Variant01A" (const 'F') - . addCaseI @"Variant01B" id - . addCaseI @"Variant01C" (const 'F') - . addCaseI @"Variant01D" (const 'F') - $ unit - variant = toVariant (Variant01B 'T') - -- Eliminate would also work because the order of the eliminators is the - -- same as the order of the cases. - assertEqual "T" 'T' (eliminateSubset cases variant) - -data Variant02Unit = - Variant02A - | Variant02B Char - | Variant02C deriving (Generic,Eq,Show) - -instance ToVariant Variant02Unit -instance FromVariant Variant02Unit - -testToVariant02Units :: Assertion -testToVariant02Units = do - let cases = addCaseI @"Variant02A" (const 'a') - . addCaseI @"Variant02B" id - . addCaseI @"Variant02C" (const 'c') - $ unit - variantA = toVariant Variant02A - variantB = toVariant (Variant02B 'b') - variantC = toVariant Variant02C - -- Eliminate would also work because the order of the eliminators is the - -- same as the order of the cases. - assertEqual "a" 'a' (eliminateSubset cases variantA) - assertEqual "b" 'b' (eliminateSubset cases variantB) - assertEqual "c" 'c' (eliminateSubset cases variantC) - -testFromVariant01 :: IO () -testFromVariant01 = do - let val1 = fromVariant (injectI @"Variant01A" 1) - val2 = fromVariant (injectI @"Variant01B" 'z') - val3 = fromVariant (injectI @"Variant01C" True) - val4 = fromVariant (injectI @"Variant01D" False) - assertEqual "Variant01A" val1 (Variant01A 1) - assertEqual "Variant01B" val2 (Variant01B 'z') - assertEqual "Variant01C" val3 (Variant01C True) - assertEqual "Variant01D" val4 (Variant01D False) - -testFromVariant02Units :: IO () -testFromVariant02Units = do - let val1 = fromVariant (injectI @"Variant02A" ()) - val2 = fromVariant (injectI @"Variant02B" 'b') - val3 = fromVariant (injectI @"Variant02C" ()) - assertEqual "Variant02A" val1 Variant02A - assertEqual "Variant02B" val2 (Variant02B 'b') - assertEqual "Variant02C" val3 Variant02C - -testRecordDeletionSingleElem :: IO () -testRecordDeletionSingleElem = do - let r = insertI @"bar" False - . insertI @"foo" 'c' - . delete @"foo" @Bool - . insertI @"foo" True - $ unit - assertEqual "foo" (getFieldI @"foo" r) 'c' - assertEqual "bar" (getFieldI @"bar" r) False - -testVariantDeletionSingleElem :: IO () -testVariantDeletionSingleElem = do - let v = injectI @"foo" @(FromList '[ '("foo",Bool) ]) False - Right r = winnowI @"foo" @Bool v - assertEqual "foo" False r - -testRecordDeletionRightElem :: IO () -testRecordDeletionRightElem = do - let r = delete @"foo" @Char - . insertI @"foo" 'f' - . insertI @"bar" 'b' - $ unit - assertEqual "bar" (getFieldI @"bar" r) 'b' - -testVariantDeletionRightElem :: IO () -testVariantDeletionRightElem = do - let v = injectI @"foo" @(FromList '[ '("foo",Bool), '("bar",Char) ]) False - Left v' = winnowI @"bar" @Char v - Right r = winnowI @"foo" @Bool v' - assertEqual "foo" False r - -testRecordDeletionLeftElem :: IO () -testRecordDeletionLeftElem = do - let r = delete @"bar" @Char - . insertI @"foo" 'f' - . insertI @"bar" 'b' - $ unit - assertEqual "foo" (getFieldI @"foo" r) 'f' - -testVariantDeletionLeftElem :: IO () -testVariantDeletionLeftElem = do - let v = injectI @"bar" @(FromList '[ '("foo",Bool), '("bar",Char) ]) 'b' - Left v' = winnowI @"foo" @Bool v - Right r = winnowI @"bar" @Char v' - assertEqual "bar" 'b' r - -type TreeX3 = FromList [ '("bfoo",Char), - '("bbar",Bool), - '("bbaz",Int) ] - -testVariantDeletion3Elem :: IO () -testVariantDeletion3Elem = do - let v = injectI @"bbaz" @TreeX3 1 - Right r = winnowI @"bbaz" @Int v - assertEqual "bbaz" 1 r - - -type Tree02 = FromList [ - '("bfoo",Char), - '("bbar",Bool), - '("bbaz",Int), - '("afoo",Char), - '("abar",Bool), - '("abaz",Int), - '("zfoo",Char), - '("zbar",Bool), - '("zbaz",Int), - '("dfoo",Char), - '("dbar",Bool), - '("dbaz",Int), - '("fbaz",Int), - '("kgoz",Int) - ] - -testVariantDeletionMany :: IO () -testVariantDeletionMany = do - let a00 = injectI @"bfoo" @Tree02 'z' - Left a02 = winnowI @"bbar" @Bool a00 - Left a03 = winnowI @"bbaz" @Int a02 - Left a04 = winnowI @"afoo" @Char a03 - Left a05 = winnowI @"abar" @Bool a04 - Left a06 = winnowI @"abaz" @Int a05 - Left a07 = winnowI @"zfoo" @Char a06 - Left a08 = winnowI @"zbar" @Bool a07 - Left a09 = winnowI @"zbaz" @Int a08 - Left a10 = winnowI @"dfoo" @Char a09 - Left a11 = winnowI @"dbar" @Bool a10 - Left a12 = winnowI @"dbaz" @Int a11 - Left a13 = winnowI @"fbaz" @Int a12 - Left a14 = winnowI @"kgoz" @Int a13 - Right a = winnowI @"bfoo" @Char a14 - assertEqual "bfoo" a 'z' - return () - -type Tree02b = FromList [ - '("bfoo",Char), - '("bbar",Bool), - '("bbaz",Int), - '("afoo",Char), - '("abar",Bool), - '("abaz",Int), - '("zfoo",Char), - '("zbar",Bool), - '("zbaz",Int), - '("dfoo",Char), - '("dbar",Bool), - '("dbaz",Int), - '("fbaz",Int), - '("kgoz",Int) - ] - -testVariantDeletionManyB :: IO () -testVariantDeletionManyB = do - let a00 = injectI @"bfoo" @Tree02b 'z' - a00' = widen @"ggg" @Char a00 - Left a02 = winnowI @"bbar" @Bool a00 - Left a03 = winnowI @"bbaz" @Int a02 - Left a04 = winnowI @"afoo" @Char a03 - Left a05 = winnowI @"abar" @Bool a04 - Left a06 = winnowI @"abaz" @Int a05 - a06b = widen @"bbb" @Int a06 - Left a07 = winnowI @"zfoo" @Char a06b - Left a08 = winnowI @"zbar" @Bool a07 - Left a09 = winnowI @"zbaz" @Int a08 - Left a10 = winnowI @"dfoo" @Char a09 - Left a10b = winnowI @"zzz" @Float a10 -- non-existent entry - Right m = winnowI @"bfoo" @Char a10b - Left a11 = winnowI @"dbar" @Bool a10b - Left a12 = winnowI @"dbaz" @Int a11 - Left a13 = winnowI @"fbaz" @Int a12 - Left a14 = winnowI @"kgoz" @Int a13 - Left a15 = winnowI @"ggg" @Char a14 - Right a = winnowI @"bfoo" @Char a15 - assertEqual "bfoo" m 'z' - assertEqual "bfoo" a 'z' - return () - -type Actions01 = [Act In "f1" Bool, - Act In "f2" Char, - Act In "f3" Float, - Act In "f4" (Int -> Int), - Act In "f5" Bool, - Act In "f6" Char, - Act In "f7" String, - Act In "f8" (Char -> Char), - Act In "f9" Bool, - Act In "f10" Char, - Act In "f11" Float - ] - -testInTandem01 :: IO () -testInTandem01 = assertEqual "" (demoteMap (Proxy @(Perform Actions01))) (perform (demoteActions (Proxy @Actions01))) - -type Actions02 = [Act In "f11" Bool, - Act In "f10" Int, - Act In "f9" Char, - Act In "f8" (Char -> Char), - Act In "f7" Int, - Act In "f6" Char, - Act In "f5" Float, - Act In "f4" Int, - Act In "f3" (Char -> Int), - Act In "f2" Bool, - Act In "f1" Char - ] - -testInTandem02 :: IO () -testInTandem02 = assertEqual "" (demoteMap (Proxy @(Perform Actions02))) (perform (demoteActions (Proxy @Actions02))) - -type Actions03 = [Act In "ff1" Bool, - Act In "af2" Char, - Act In "wf3" Int, - Act In "uf4" Bool, - Act In "uf5" Char, - Act In "af6" Int, - Act In "pf7" Bool, - Act De "qf5" Char, - Act De "bf2" Char, - Act In "hf8" (Int -> Int), - Act De "mf4" Bool, - Act In "af9" Bool, - Act In "yf10" Char, - Act In "mf11" String, - Act De "zf3" Int - ] - -testInTandem03 :: IO () -testInTandem03 = assertEqual "" (demoteMap (Proxy @(Perform Actions03))) (perform (demoteActions (Proxy @Actions03))) - - -type Actions04 = [Act In "ef1" Bool, - Act In "ef2" Char, - Act De "ef3" Int, -- we can delete entries that don't exist - Act In "af3" Int, - Act De "af3" Int, - Act In "kf4" Bool, - Act De "kf4" Bool, - Act In "pf5" Char, - Act De "pf5" Char, - Act In "zf6" Int, - Act De "zf6" Int, - Act In "ff7" Bool, - Act De "ff7" Bool, - Act In "rf5" Char, - Act De "rf5" Char, - Act De "ef2" Char, - Act In "lf8" (Int -> Int), - Act In "lll" Bool, - Act De "lll" Bool, - Act De "lf8" (Int -> Int), - Act In "ef1" Bool, -- we can re-add the exact same entry - Act De "ef1" Bool - ] - -testInTandem04 :: IO () -testInTandem04 = assertEqual "" (demoteMap (Proxy @(Perform Actions04))) (perform (demoteActions (Proxy @Actions04))) - - --- sequences of actions for tests --- --- -data InsertOrDelete = In - | De - deriving (Show, Eq) - -class DemotableInsertOrDelete (iod :: InsertOrDelete) where - demoteIoD :: Proxy iod -> InsertOrDelete - -instance DemotableInsertOrDelete 'In where - demoteIoD _ = In - -instance DemotableInsertOrDelete 'De where - demoteIoD _ = De - -data Action s t = Act InsertOrDelete s t deriving (Show, Eq) - -class DemotableAction (a :: Action Symbol Type) where - demoteAction :: Proxy a -> Action String TypeRep - -instance (DemotableInsertOrDelete iod, KnownSymbol s, Typeable t) => DemotableAction (Act iod s t) where - demoteAction _ = Act (demoteIoD (Proxy @iod)) - (symbolVal (Proxy @s)) - (typeRep (Proxy @t)) - -demoteActions :: forall as. All DemotableAction as => Proxy (as :: [Action Symbol Type]) -> [Action String TypeRep] -demoteActions _ = collapse_NP $ cpure_NP @_ @as (Proxy @DemotableAction) conjure - where - conjure :: forall a. DemotableAction a => K (Action String TypeRep) a - conjure = K (demoteAction (Proxy @a)) - -type family Perform (as :: [Action Symbol Type]) :: Map Symbol Type where - Perform (Act In s v ': as) = Insert s v (Perform as) - Perform (Act De s v ': as) = Delete s v (Perform as) - Perform '[] = Empty - -perform :: [Action String TypeRep] -> Map String TypeRep -perform = foldr (\(Act iod s v) t -> case iod of In -> t_insert s v t - De -> t_delete s t) - emptyMap - --- --- --- - -type PolyKinded01 = FromList '[ '("aaa","v1"), - '("bbb","v2"), - '("ccc","v3"), - '("ddd","v4"), - '("eee","v5") ] - -polyKindedRecord01 :: Record Proxy PolyKinded01 -polyKindedRecord01 = - insert @"aaa" (Proxy @"v1") - . insert @"bbb" (Proxy @"v2") - . insert @"ccc" (Proxy @"v3") - . insert @"ddd" (Proxy @"v4") - . insert @"eee" (Proxy @"v5") - $ unit - -polyKinded01 :: Assertion -polyKinded01 = do - let r = insert @"aaa" (Proxy @"v1") - . insert @"bbb" (Proxy @"v2") - . insert @"ccc" (Proxy @"v3") - . insert @"ddd" (Proxy @"v4") - . insert @"eee" (Proxy @"v5") - . insert @"abb" (Proxy @"v2") - . insert @"acc" (Proxy @"v3") - . insert @"add" (Proxy @"v4") - . insert @"aee" (Proxy @"v5") - $ unit - proxy :: Proxy "v2" - proxy = getField @"abb" r - return () - -polyKinded02 :: Assertion -polyKinded02 = do - let r = demoteEntries @PolyKinded01 - K (_,trep) = getField @"eee" r - assertEqual "" trep (typeRep (Proxy @"v5")) - return () - - +{-# LANGUAGE DataKinds, + TypeOperators, + TypeFamilies, + TypeApplications, + DeriveGeneric, + StandaloneDeriving, + UndecidableInstances, + KindSignatures, + PartialTypeSignatures, + FlexibleContexts, + ScopedTypeVariables +#-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} +module Main where + +import Data.RBR +import qualified Data.RBR.Subset as S +import Data.RBR.Demoted (emptyMap,DemotableMap(demoteMap),t_insert,t_delete) +import Data.SOP +import Data.SOP.NP (cpure_NP,collapse_NP) +import Data.Typeable +import Data.Proxy +import GHC.TypeLits +import Data.Kind +import GHC.Generics (Generic) + +import Test.Tasty +import Test.Tasty.HUnit (testCase,Assertion,assertEqual,assertBool) + + +main :: IO () +main = defaultMain tests + +tests :: TestTree +tests = testGroup "Tests" [ testCase "recordGetSet01" testRecordGetSet01, + testCase "variantInjectMatch01" testVariantInjectMatch01, + testCase "projectSubset01" testProjectSubset01, + testGroup "nominalConversion" [ + testCase "toRecord01" testToRecord01, + testCase "fromRecord01" testFromRecord01, + testCase "toVariant01" testToVariant01, + testCase "toVariant02Units" testToVariant02Units, + testCase "fromVariant01" testFromVariant01, + testCase "fromVariant02Units" testFromVariant02Units + ], + testGroup "deletion" [ + testGroup "records" [ + testCase "recordDeletionSingleElem" testRecordDeletionSingleElem, + testCase "recordDeletionLeftElem" testRecordDeletionLeftElem, + testCase "recordDeletionRightElem" testRecordDeletionRightElem + ], + testGroup "variants" [ + testCase "variantDeletionSingleElem" testVariantDeletionSingleElem, + testCase "variantDeletionLeftElem" testVariantDeletionLeftElem, + testCase "variantDeletionRightElem" testVariantDeletionRightElem, + testCase "variantDeletion3Elem" testVariantDeletion3Elem, + testCase "variantDeletionMany" testVariantDeletionMany, + testCase "variantDeletionManyB" testVariantDeletionManyB + ] + ], + testGroup "typeLevelTermLvel" [ + testCase "tandem01" testInTandem01, + testCase "tandem02" testInTandem02, + testCase "tandem03" testInTandem03, + testCase "tandem04" testInTandem04 + ], + testGroup "polyKindedMap" [ + testCase "polyKinded01" polyKinded01, + testCase "polyKinded02" polyKinded02 + ] + ] + + +testRecordGetSet01 :: Assertion +testRecordGetSet01 = do + let r = insertI @"bfoo" 'c' + . insertI @"bbar" True + . insertI @"bbaz" (1::Int) + . insertI @"afoo" 'd' + . insertI @"abar" False + . insertI @"abaz" (2::Int) + . insertI @"zfoo" 'x' + . insertI @"zbar" False + . insertI @"zbaz" (4::Int) + . insertI @"dfoo" 'z' + . insertI @"dbar" True + . insertI @"dbaz" (5::Int) + . insertI @"fbaz" (6::Int) + $ unit + s = setFieldI @"fbaz" 9 (setFieldI @"zfoo" 'k' r) + assertEqual "bfoo" (getFieldI @"bfoo" s) 'c' + assertEqual "bbar" (getFieldI @"bbar" s) True + assertEqual "bbaz" (getFieldI @"bbaz" s) (1::Int) + assertEqual "afoo" (getFieldI @"afoo" s) 'd' + assertEqual "abar" (getFieldI @"abar" s) False + assertEqual "abaz" (getFieldI @"abaz" s) (2::Int) + assertEqual "zfoo" (getFieldI @"zfoo" s) 'k' + assertEqual "zbar" (getFieldI @"zbar" s) False + assertEqual "zbaz" (getFieldI @"zbaz" s) (4::Int) + assertEqual "dfoo" (getFieldI @"dfoo" s) 'z' + assertEqual "dbar" (getFieldI @"dbar" s) True + assertEqual "dbaz" (getFieldI @"dbaz" s) (5::Int) + assertEqual "fbaz" (getFieldI @"fbaz" s) (9::Int) + return () + +type Tree01 = FromList [ '("bfoo",Char), + '("bbar",Bool), + '("bbaz",Int), + '("afoo",Char), + '("abar",Bool), + '("abaz",Int), + '("zfoo",Char), + '("zbar",Bool), + '("zbaz",Int), + '("dfoo",Char), + '("dbar",Bool), + '("dbaz",Int), + '("fbaz",Int), + '("kgoz",Int) ] + +testVariantInjectMatch01 :: Assertion +testVariantInjectMatch01 = do + let r0 = injectI @"bfoo" @Tree01 'c' + r1 = injectI @"bbar" @Tree01 True + r2 = injectI @"bbaz" @Tree01 (1::Int) + r3 = injectI @"afoo" @Tree01 'd' + r4 = injectI @"abar" @Tree01 False + r5 = injectI @"abaz" @Tree01 (2::Int) + r6 = injectI @"zfoo" @Tree01 'x' + r7 = injectI @"zbar" @Tree01 False + r8 = injectI @"zbaz" @Tree01 (4::Int) + r9 = injectI @"dfoo" @Tree01 'z' + r10 = injectI @"dbar" @Tree01 True + r11 = injectI @"dbaz" @Tree01 (5::Int) + r12 = injectI @"fbaz" @Tree01 (6::Int) + r13 = injectI @"kgoz" @Tree01 (9::Int) + assertEqual "bfoo" (matchI @"bfoo" r0 ) $ Just 'c' + assertEqual "bbar" (matchI @"bbar" r1 ) $ Just True + assertEqual "bbaz" (matchI @"bbaz" r2 ) $ Just (1::Int) + assertEqual "afoo" (matchI @"afoo" r3 ) $ Just 'd' + assertEqual "abar" (matchI @"abar" r4 ) $ Just False + assertEqual "abaz" (matchI @"abaz" r5 ) $ Just (2::Int) + assertEqual "zfoo" (matchI @"zfoo" r6 ) $ Just 'x' + assertEqual "zbar" (matchI @"zbar" r7 ) $ Just False + assertEqual "zbaz" (matchI @"zbaz" r8 ) $ Just (4::Int) + assertEqual "dfoo" (matchI @"dfoo" r9 ) $ Just 'z' + assertEqual "dbar" (matchI @"dbar" r10) $ Just True + assertEqual "dbaz" (matchI @"dbaz" r11) $ Just (5::Int) + assertEqual "fbaz" (matchI @"fbaz" r12) $ Just (6::Int) + assertEqual "kgoz" (matchI @"kgoz" r13) $ Just (9::Int) + return () + + +testProjectSubset01 :: Assertion +testProjectSubset01 = do + let r = insertI @"foo" 'c' + . insertI @"bar" True + . insertI @"baz" (1::Int) + $ unit + s = S.projectSubset @(FromList '[ '("bar",_), + '("baz",_) ]) r + bar = getFieldI @"bar" s + baz = getFieldI @"baz" s + assertEqual "bar" bar True + assertEqual "baz" baz 1 + +data Person = Person { name :: String, age :: Int, whatever :: Char } deriving (Generic,Eq,Show) + +instance ToRecord Person +instance FromRecord Person + +testToRecord01 :: Assertion +testToRecord01 = do + let r = toRecord (Person "Foo" 50 'z') + assertEqual "name" "Foo" (getFieldI @"name" r) + assertEqual "age" 50 (getFieldI @"age" r) + assertEqual "whatever" 'z' (getFieldI @"whatever" r) + +testFromRecord01 :: Assertion +testFromRecord01 = do + let r = insertI @"name" "Foo" + . insertI @"age" 50 + . insertI @"whatever" 'z' + $ unit + assertEqual "person" (Person "Foo" 50 'z') (fromRecord r) + +data Variant01 = Variant01A Int + | Variant01B Char + | Variant01C Bool + | Variant01D Bool + deriving (Generic,Eq,Show) + +instance ToVariant Variant01 +instance FromVariant Variant01 + +testToVariant01 :: Assertion +testToVariant01 = do + let val1 = Variant01A 0 + val2 = Variant01B 'c' + val3 = Variant01C True + cases = addCaseI @"Variant01A" (const 'F') + . addCaseI @"Variant01B" id + . addCaseI @"Variant01C" (const 'F') + . addCaseI @"Variant01D" (const 'F') + $ unit + variant = toVariant (Variant01B 'T') + -- Eliminate would also work because the order of the eliminators is the + -- same as the order of the cases. + assertEqual "T" 'T' (S.eliminateSubset cases variant) + +data Variant02Unit = + Variant02A + | Variant02B Char + | Variant02C deriving (Generic,Eq,Show) + +instance ToVariant Variant02Unit +instance FromVariant Variant02Unit + +testToVariant02Units :: Assertion +testToVariant02Units = do + let cases = addCaseI @"Variant02A" (const 'a') + . addCaseI @"Variant02B" id + . addCaseI @"Variant02C" (const 'c') + $ unit + variantA = toVariant Variant02A + variantB = toVariant (Variant02B 'b') + variantC = toVariant Variant02C + -- Eliminate would also work because the order of the eliminators is the + -- same as the order of the cases. + assertEqual "a" 'a' (S.eliminateSubset cases variantA) + assertEqual "b" 'b' (S.eliminateSubset cases variantB) + assertEqual "c" 'c' (S.eliminateSubset cases variantC) + +testFromVariant01 :: IO () +testFromVariant01 = do + let val1 = fromVariant (injectI @"Variant01A" 1) + val2 = fromVariant (injectI @"Variant01B" 'z') + val3 = fromVariant (injectI @"Variant01C" True) + val4 = fromVariant (injectI @"Variant01D" False) + assertEqual "Variant01A" val1 (Variant01A 1) + assertEqual "Variant01B" val2 (Variant01B 'z') + assertEqual "Variant01C" val3 (Variant01C True) + assertEqual "Variant01D" val4 (Variant01D False) + +testFromVariant02Units :: IO () +testFromVariant02Units = do + let val1 = fromVariant (injectI @"Variant02A" ()) + val2 = fromVariant (injectI @"Variant02B" 'b') + val3 = fromVariant (injectI @"Variant02C" ()) + assertEqual "Variant02A" val1 Variant02A + assertEqual "Variant02B" val2 (Variant02B 'b') + assertEqual "Variant02C" val3 Variant02C + +testRecordDeletionSingleElem :: IO () +testRecordDeletionSingleElem = do + let r = insertI @"bar" False + . insertI @"foo" 'c' + . delete @"foo" @Bool + . insertI @"foo" True + $ unit + assertEqual "foo" (getFieldI @"foo" r) 'c' + assertEqual "bar" (getFieldI @"bar" r) False + +testVariantDeletionSingleElem :: IO () +testVariantDeletionSingleElem = do + let v = injectI @"foo" @(FromList '[ '("foo",Bool) ]) False + Right r = winnowI @"foo" @Bool v + assertEqual "foo" False r + +testRecordDeletionRightElem :: IO () +testRecordDeletionRightElem = do + let r = delete @"foo" @Char + . insertI @"foo" 'f' + . insertI @"bar" 'b' + $ unit + assertEqual "bar" (getFieldI @"bar" r) 'b' + +testVariantDeletionRightElem :: IO () +testVariantDeletionRightElem = do + let v = injectI @"foo" @(FromList '[ '("foo",Bool), '("bar",Char) ]) False + Left v' = winnowI @"bar" @Char v + Right r = winnowI @"foo" @Bool v' + assertEqual "foo" False r + +testRecordDeletionLeftElem :: IO () +testRecordDeletionLeftElem = do + let r = delete @"bar" @Char + . insertI @"foo" 'f' + . insertI @"bar" 'b' + $ unit + assertEqual "foo" (getFieldI @"foo" r) 'f' + +testVariantDeletionLeftElem :: IO () +testVariantDeletionLeftElem = do + let v = injectI @"bar" @(FromList '[ '("foo",Bool), '("bar",Char) ]) 'b' + Left v' = winnowI @"foo" @Bool v + Right r = winnowI @"bar" @Char v' + assertEqual "bar" 'b' r + +type TreeX3 = FromList [ '("bfoo",Char), + '("bbar",Bool), + '("bbaz",Int) ] + +testVariantDeletion3Elem :: IO () +testVariantDeletion3Elem = do + let v = injectI @"bbaz" @TreeX3 1 + Right r = winnowI @"bbaz" @Int v + assertEqual "bbaz" 1 r + + +type Tree02 = FromList [ + '("bfoo",Char), + '("bbar",Bool), + '("bbaz",Int), + '("afoo",Char), + '("abar",Bool), + '("abaz",Int), + '("zfoo",Char), + '("zbar",Bool), + '("zbaz",Int), + '("dfoo",Char), + '("dbar",Bool), + '("dbaz",Int), + '("fbaz",Int), + '("kgoz",Int) + ] + +testVariantDeletionMany :: IO () +testVariantDeletionMany = do + let a00 = injectI @"bfoo" @Tree02 'z' + Left a02 = winnowI @"bbar" @Bool a00 + Left a03 = winnowI @"bbaz" @Int a02 + Left a04 = winnowI @"afoo" @Char a03 + Left a05 = winnowI @"abar" @Bool a04 + Left a06 = winnowI @"abaz" @Int a05 + Left a07 = winnowI @"zfoo" @Char a06 + Left a08 = winnowI @"zbar" @Bool a07 + Left a09 = winnowI @"zbaz" @Int a08 + Left a10 = winnowI @"dfoo" @Char a09 + Left a11 = winnowI @"dbar" @Bool a10 + Left a12 = winnowI @"dbaz" @Int a11 + Left a13 = winnowI @"fbaz" @Int a12 + Left a14 = winnowI @"kgoz" @Int a13 + Right a = winnowI @"bfoo" @Char a14 + assertEqual "bfoo" a 'z' + return () + +type Tree02b = FromList [ + '("bfoo",Char), + '("bbar",Bool), + '("bbaz",Int), + '("afoo",Char), + '("abar",Bool), + '("abaz",Int), + '("zfoo",Char), + '("zbar",Bool), + '("zbaz",Int), + '("dfoo",Char), + '("dbar",Bool), + '("dbaz",Int), + '("fbaz",Int), + '("kgoz",Int) + ] + +testVariantDeletionManyB :: IO () +testVariantDeletionManyB = do + let a00 = injectI @"bfoo" @Tree02b 'z' + a00' = widen @"ggg" @Char a00 + Left a02 = winnowI @"bbar" @Bool a00 + Left a03 = winnowI @"bbaz" @Int a02 + Left a04 = winnowI @"afoo" @Char a03 + Left a05 = winnowI @"abar" @Bool a04 + Left a06 = winnowI @"abaz" @Int a05 + a06b = widen @"bbb" @Int a06 + Left a07 = winnowI @"zfoo" @Char a06b + Left a08 = winnowI @"zbar" @Bool a07 + Left a09 = winnowI @"zbaz" @Int a08 + Left a10 = winnowI @"dfoo" @Char a09 + Left a10b = winnowI @"zzz" @Float a10 -- non-existent entry + Right m = winnowI @"bfoo" @Char a10b + Left a11 = winnowI @"dbar" @Bool a10b + Left a12 = winnowI @"dbaz" @Int a11 + Left a13 = winnowI @"fbaz" @Int a12 + Left a14 = winnowI @"kgoz" @Int a13 + Left a15 = winnowI @"ggg" @Char a14 + Right a = winnowI @"bfoo" @Char a15 + assertEqual "bfoo" m 'z' + assertEqual "bfoo" a 'z' + return () + +type Actions01 = [Act In "f1" Bool, + Act In "f2" Char, + Act In "f3" Float, + Act In "f4" (Int -> Int), + Act In "f5" Bool, + Act In "f6" Char, + Act In "f7" String, + Act In "f8" (Char -> Char), + Act In "f9" Bool, + Act In "f10" Char, + Act In "f11" Float + ] + +testInTandem01 :: IO () +testInTandem01 = assertEqual "" (demoteMap (Proxy @(Perform Actions01))) (perform (demoteActions (Proxy @Actions01))) + +type Actions02 = [Act In "f11" Bool, + Act In "f10" Int, + Act In "f9" Char, + Act In "f8" (Char -> Char), + Act In "f7" Int, + Act In "f6" Char, + Act In "f5" Float, + Act In "f4" Int, + Act In "f3" (Char -> Int), + Act In "f2" Bool, + Act In "f1" Char + ] + +testInTandem02 :: IO () +testInTandem02 = assertEqual "" (demoteMap (Proxy @(Perform Actions02))) (perform (demoteActions (Proxy @Actions02))) + +type Actions03 = [Act In "ff1" Bool, + Act In "af2" Char, + Act In "wf3" Int, + Act In "uf4" Bool, + Act In "uf5" Char, + Act In "af6" Int, + Act In "pf7" Bool, + Act De "qf5" Char, + Act De "bf2" Char, + Act In "hf8" (Int -> Int), + Act De "mf4" Bool, + Act In "af9" Bool, + Act In "yf10" Char, + Act In "mf11" String, + Act De "zf3" Int + ] + +testInTandem03 :: IO () +testInTandem03 = assertEqual "" (demoteMap (Proxy @(Perform Actions03))) (perform (demoteActions (Proxy @Actions03))) + + +type Actions04 = [Act In "ef1" Bool, + Act In "ef2" Char, + Act De "ef3" Int, -- we can delete entries that don't exist + Act In "af3" Int, + Act De "af3" Int, + Act In "kf4" Bool, + Act De "kf4" Bool, + Act In "pf5" Char, + Act De "pf5" Char, + Act In "zf6" Int, + Act De "zf6" Int, + Act In "ff7" Bool, + Act De "ff7" Bool, + Act In "rf5" Char, + Act De "rf5" Char, + Act De "ef2" Char, + Act In "lf8" (Int -> Int), + Act In "lll" Bool, + Act De "lll" Bool, + Act De "lf8" (Int -> Int), + Act In "ef1" Bool, -- we can re-add the exact same entry + Act De "ef1" Bool + ] + +testInTandem04 :: IO () +testInTandem04 = assertEqual "" (demoteMap (Proxy @(Perform Actions04))) (perform (demoteActions (Proxy @Actions04))) + + +-- sequences of actions for tests +-- +-- +data InsertOrDelete = In + | De + deriving (Show, Eq) + +class DemotableInsertOrDelete (iod :: InsertOrDelete) where + demoteIoD :: Proxy iod -> InsertOrDelete + +instance DemotableInsertOrDelete 'In where + demoteIoD _ = In + +instance DemotableInsertOrDelete 'De where + demoteIoD _ = De + +data Action s t = Act InsertOrDelete s t deriving (Show, Eq) + +class DemotableAction (a :: Action Symbol Type) where + demoteAction :: Proxy a -> Action String TypeRep + +instance (DemotableInsertOrDelete iod, KnownSymbol s, Typeable t) => DemotableAction (Act iod s t) where + demoteAction _ = Act (demoteIoD (Proxy @iod)) + (symbolVal (Proxy @s)) + (typeRep (Proxy @t)) + +demoteActions :: forall as. All DemotableAction as => Proxy (as :: [Action Symbol Type]) -> [Action String TypeRep] +demoteActions _ = collapse_NP $ cpure_NP @_ @as (Proxy @DemotableAction) conjure + where + conjure :: forall a. DemotableAction a => K (Action String TypeRep) a + conjure = K (demoteAction (Proxy @a)) + +type family Perform (as :: [Action Symbol Type]) :: Map Symbol Type where + Perform (Act In s v ': as) = Insert s v (Perform as) + Perform (Act De s v ': as) = Delete s v (Perform as) + Perform '[] = Empty + +perform :: [Action String TypeRep] -> Map String TypeRep +perform = foldr (\(Act iod s v) t -> case iod of In -> t_insert s v t + De -> t_delete s t) + emptyMap + +-- +-- +-- + +type PolyKinded01 = FromList '[ '("aaa","v1"), + '("bbb","v2"), + '("ccc","v3"), + '("ddd","v4"), + '("eee","v5") ] + +polyKindedRecord01 :: Record Proxy PolyKinded01 +polyKindedRecord01 = + insert @"aaa" (Proxy @"v1") + . insert @"bbb" (Proxy @"v2") + . insert @"ccc" (Proxy @"v3") + . insert @"ddd" (Proxy @"v4") + . insert @"eee" (Proxy @"v5") + $ unit + +polyKinded01 :: Assertion +polyKinded01 = do + let r = insert @"aaa" (Proxy @"v1") + . insert @"bbb" (Proxy @"v2") + . insert @"ccc" (Proxy @"v3") + . insert @"ddd" (Proxy @"v4") + . insert @"eee" (Proxy @"v5") + . insert @"abb" (Proxy @"v2") + . insert @"acc" (Proxy @"v3") + . insert @"add" (Proxy @"v4") + . insert @"aee" (Proxy @"v5") + $ unit + proxy :: Proxy "v2" + proxy = getField @"abb" r + return () + +polyKinded02 :: Assertion +polyKinded02 = do + let r = demoteEntries @PolyKinded01 + K (_,trep) = getField @"eee" r + assertEqual "" trep (typeRep (Proxy @"v5")) + return () + +