red-black-record (empty) → 1.0.0.0
raw patch · 8 files changed
+1630/−0 lines, 8 filesdep +aesondep +basedep +bytestring
Dependencies added: aeson, base, bytestring, doctest, profunctors, red-black-record, sop-core, tasty, tasty-hunit, text
Files
- CHANGELOG.md +5/−0
- LICENSE +30/−0
- lib/Data/RBR.hs +119/−0
- lib/Data/RBR/Examples.hs +244/−0
- lib/Data/RBR/Internal.hs +986/−0
- red-black-record.cabal +62/−0
- tests/doctests.hs +6/−0
- tests/tests.hs +178/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for red-black-record + +## 1.0.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +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.
+ lib/Data/RBR.hs view
@@ -0,0 +1,119 @@+module Data.RBR ( + -- * Type-level Red-Black tree + -- $typelevel + Color (..), + RBT (..), + KeysValuesAll, + KnownKey, + demoteKeys, + -- * Records and Variants + Record, + unit, + prettyShowRecord, + prettyShowRecordI, + Variant, + impossible, + prettyShowVariant, + prettyShowVariantI, + -- ** Inserting and widening + Insertable (..), + addField, + insertI, + addFieldI, + InsertAll, + FromList, + -- ** Projecting and injecting + Key (..), + 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 (..), + fromNP, + toNP, + Sumlike (..), + fromNS, + toNS, + -- * 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 Red-Black tree that is used at the type level, with @DataKinds@. The tree + keeps track of what keys are present and to what types they correspond. + + +-} + +{- $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. + +-}
+ lib/Data/RBR/Examples.hs view
@@ -0,0 +1,244 @@+module Data.RBR.Examples ( + -- * 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 + + -- * 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 + ) 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) +>>> import Data.String +>>> import Data.Proxy +>>> 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 + +-} + + +{- $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 pr = transform $ fromNP @c (cpure_NP (Proxy @FromJSON) (Star parseJSON)) + mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) + Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c demoteKeys) (toNP pr)) + 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 + + 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. + +>>> :{ + 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 pr = fromNP @c (cpure_NP (Proxy @FromJSON) (Star parseJSON)) + mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) + Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c aliases) (toNP pr)) + 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 = 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 whole flat wholeflat. (KeysValuesAll KnownKey whole, + Productlike '[] whole wholeflat, + ProductlikeSubset subset whole flat, + All FromJSON wholeflat) + => Data.Aeson.Value + -> Parser (Record I subset) + parseFieldSubset = + let pNP = cpure_NP (Proxy @FromJSON) (Star parseJSON) + mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name)) + objpNP = liftA2_NP mapKSS (toNP @whole demoteKeys) pNP + subNP = toNP @subset $ getFieldSubset @subset $ fromNP @whole objpNP + Star subparser = fromNP @subset <$> sequence_NP subNP + 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",_) ]) @(RecordCode Person) + Just s = parseMaybe subsetParser v + in fromRecord @Person . setFieldSubset s $ toRecord original + :} +Person {name = "Mark", age = 70, whatever = True} + +-}
+ lib/Data/RBR/Internal.hs view
@@ -0,0 +1,986 @@+{-# 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.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) + +-- | The color of a node. +data Color = R + | B + deriving Show + +-- | The Red-Black tree. It will be used, as a kind, to index the 'Record' and 'Variant' types. +data RBT k v = E + | N Color (RBT k v) k v (RBT k v) + deriving Show + +-- +-- +-- 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 :: k -> v -> Constraint) (t :: RBT k v) :: 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". + + 'cpara_RBT' constructs a 'Record' by means of a constraint for producing + the nodes of the tree. The constraint is passed as a 'Data.Proxy.Proxy'. + This function seldom needs to be called directly. +-} +class KeysValuesAllF c t => KeysValuesAll (c :: k -> v -> Constraint) (t :: RBT k v) where + cpara_RBT :: + 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_RBT _p nil _step = nil + +instance (c k v, KeysValuesAll c left, KeysValuesAll c right) => KeysValuesAll c (N color left k v right) where + cpara_RBT p nil cons = + cons (cpara_RBT p nil cons) (cpara_RBT p nil cons) + +{- | 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 of the type + that corresponds to each field, only the 'String' annotations. +-} +demoteKeys :: forall t. KeysValuesAll KnownKey t => Record (K String) t +demoteKeys = cpara_RBT (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 + +-- the "class synonym" trick. https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ +class KnownSymbol k => KnownKey (k :: Symbol) (v :: z) +instance KnownSymbol k => KnownKey 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'. +-} +data Record (f :: Type -> Type) (t :: RBT Symbol Type) 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) ++ ")" + +{- | 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 E +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'. +-} +data Variant (f :: Type -> Type) (t :: RBT Symbol Type) 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 E -> 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 tree. +-} +type family InsertAll (es :: [(Symbol,Type)]) (t :: RBT Symbol Type) :: RBT Symbol Type where + InsertAll '[] t = t + InsertAll ( '(name,fieldType) ': es ) t = Insert name fieldType (InsertAll es t) + +{- | Build a type-level tree out of a list of type level key / value pairs. +-} +type FromList (es :: [(Symbol,Type)]) = InsertAll es E + +{- | 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. +-} +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 + +-- +-- +-- The original term-level code, from the post "Persistent Red Black Trees in Haskell" +-- +-- https://abhiroop.github.io/Haskell-Red-Black-Tree/ +-- +-- insert :: (Ord a) => a -> Tree a -> Tree a +-- insert x s = makeBlack $ ins s +-- where ins E = T R E x E +-- ins (T color a y b) +-- | x < y = balance color (ins a) y b +-- | x == y = T color a y b +-- | x > y = balance color a y (ins b) +-- makeBlack (T _ a y b) = T B a y b +-- +-- balance :: Color -> Tree a -> a -> Tree a -> Tree a +-- balance B (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 B (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 B 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 B 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 color a x b = T color a x b + +{- | Class that determines if the pair of a 'Symbol' key and a 'Type' can + be inserted into a type-level tree. + + The associated type family 'Insert' produces the resulting tree. + + 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 tree already has the key but with a /different/ type, the insertion + fails to compile. + -} +class Insertable (k :: Symbol) (v :: Type) (t :: RBT Symbol Type) where + type Insert k v t :: RBT Symbol Type + insert :: f v -> Record f t -> Record f (Insert k v t) + widen :: Variant f t -> Variant f (Insert k v t) + +instance (InsertableHelper1 k v t, CanMakeBlack (Insert1 k v t)) => 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 :: RBT Symbol Type) where + type MakeBlack t :: RBT Symbol Type + 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 (Here fv) = Here fv + +class InsertableHelper1 (k :: Symbol) + (v :: Type) + (t :: RBT Symbol Type) where + type Insert1 k v t :: RBT Symbol Type + 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 :: Type) + (color :: Color) + (left :: RBT Symbol Type) + (k' :: Symbol) + (v' :: Type) + (right :: RBT Symbol Type) where + type Insert2 ordering k v color left k' v' right :: RBT Symbol Type + 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) + +instance (InsertableHelper1 k v left, + Balanceable color (Insert1 k v left) k' v' right + ) + => InsertableHelper2 LT k v color left k' v' right where + type Insert2 LT k v color left k' v' right = Balance color (Insert1 k v left) k' v' right + insert2 fv (Node left fv' right) = balanceR @color @_ @k' @v' @right (Node (insert1 @k @v fv left) fv' right) + widen2 v = balanceV @color @(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 + + +-- 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 + +instance (InsertableHelper1 k v right, + Balanceable color left k' v' (Insert1 k v right) + ) + => InsertableHelper2 GT k v color left k' v' right where + type Insert2 GT k v color left k' v' right = Balance color left k' v' (Insert1 k v right) + insert2 fv (Node left fv' right) = balanceR @color @left @k' @v' @_ (Node left fv' (insert1 @k @v fv right)) + widen2 v = balanceV @color @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) + +data BalanceAction = BalanceLL + | BalanceLR + | BalanceRL + | BalanceRR + | DoNotBalance + deriving Show + +type family ShouldBalance (color :: Color) + (left :: RBT k' v') + (right :: RBT k' v') :: BalanceAction where + ShouldBalance B (N R (N R _ _ _ _) _ _ _) _ = BalanceLL + ShouldBalance B (N R _ _ _ (N R _ _ _ _)) _ = BalanceLR + ShouldBalance B _ (N R (N R _ _ _ _) _ _ _) = BalanceRL + ShouldBalance B _ (N R _ _ _ (N R _ _ _ _)) = BalanceRR + ShouldBalance _ _ _ = DoNotBalance + +class Balanceable (color :: Color) + (left :: RBT Symbol Type) + (k :: Symbol) + (v :: Type) + (right :: RBT Symbol Type) where + type Balance color left k v right :: RBT Symbol Type + balanceR :: Record f (N color left k v right) -> Record f (Balance color left k v right) + balanceV :: Variant f (N color left k v right) -> Variant f (Balance color left k v right) + +instance (ShouldBalance color left right ~ action, + BalanceableHelper action color left k v right + ) + => Balanceable color 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 color left k v right = Balance' (ShouldBalance color left right) color left k v right + balanceR = balanceR' @action @color @left @k @v @right + balanceV = balanceV' @action @color @left @k @v @right + +class BalanceableHelper (action :: BalanceAction) + (color :: Color) + (left :: RBT Symbol Type) + (k :: Symbol) + (v :: Type) + (right :: RBT Symbol Type) where + type Balance' action color left k v right :: RBT Symbol Type + balanceR' :: Record f (N color left k v right) -> Record f (Balance' action color left k v right) + balanceV' :: Variant f (N color left k v right) -> Variant f (Balance' action color left k v right) + +instance BalanceableHelper BalanceLL B (N R (N R a k1 v1 b) k2 v2 c) k3 v3 d where + type Balance' BalanceLL B (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) + +instance BalanceableHelper BalanceLR B (N R a k1 v1 (N R b k2 v2 c)) k3 v3 d where + type Balance' BalanceLR B (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) + +instance BalanceableHelper BalanceRL B a k1 v1 (N R (N R b k2 v2 c) k3 v3 d) where + type Balance' BalanceRL B 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) + +instance BalanceableHelper BalanceRR B a k1 v1 (N R b k2 v2 (N R c k3 v3 d)) where + type Balance' BalanceRR B 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) + +instance BalanceableHelper DoNotBalance color a k v b where + type Balance' DoNotBalance color a k v b = N color a k v b + balanceR' = id + balanceV' = id + +-- +-- +-- Accessing fields + +{- | + Class that determines if a given 'Symbol' key is present in a type-level + tree. + + The 'Value' type family gives the 'Type' corresponding to the key. + + 'field' 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. + + 'branch' takes a branch name (given through @TypeApplications@) and + returns a pair of a match function and a constructor. +-} + +class Key (k :: Symbol) (t :: RBT Symbol Type) where + type Value k t :: Type + field :: Record f t -> (f (Value k t) -> Record f t, f (Value k t)) + branch :: (Variant f t -> Maybe (f (Value k t)), f (Value k t) -> Variant f t) + +class KeyHelper (ordering :: Ordering) (k :: Symbol) (t :: RBT Symbol Type) where + type Value' ordering k t :: Type + field' :: Record f t -> (f (Value' ordering k t) -> Record f t, f (Value' ordering k t)) + branch' :: (Variant f t -> Maybe (f (Value' ordering k t)), f (Value' ordering k t) -> Variant f t) + +instance (CmpSymbol k' k ~ ordering, KeyHelper ordering k (N color left k' 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 (N color left k' v' right) + field = field' @ordering @k + branch = branch' @ordering @k + +instance Key k right => KeyHelper LT k (N color left k' v' right) where + type Value' LT k (N color left k' v' right) = Value k right + field' (Node left fv right) = + let (setter,x) = field @k right + in (\z -> Node left fv (setter z),x) + branch' = + let (match,inj) = branch @k @right + in (\case LookRight x -> match x + _ -> Nothing, + \fv -> LookRight (inj fv)) + +instance Key k left => KeyHelper GT k (N color left k' v' right) where + type Value' GT k (N color left k' v' right) = Value k left + field' (Node left fv right) = + let (setter,x) = field @k left + in (\z -> Node (setter z) fv right,x) + branch' = + let (match,inj) = branch @k @left + in (\case LookLeft x -> match x + _ -> Nothing, + \fv -> LookLeft (inj fv)) + +instance KeyHelper EQ k (N color left k v right) where + type Value' EQ k (N color left k 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'. +-} +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 :: 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. +-} +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 :: (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) + +{- | 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 :: RBT Symbol Type) (k :: Symbol) (v :: Type) +instance (Key k t, Value k t ~ v) => PresentIn (t :: RBT Symbol Type) (k :: Symbol) (v :: Type) + +{- | Constraint for trees that represent subsets of fields of 'Record'-like types. +-} +type ProductlikeSubset (subset :: RBT Symbol Type) (whole :: RBT Symbol Type) (flat :: [Type]) = + (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_RBT (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_RBT (Proxy @(PresentIn whole)) unit goget) + +{- | Like 'project', but extracts multiple fields at the same time. + + Can also be used to convert between structurally dissimilar trees that + nevertheless have 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 trees that represent subsets of branches of 'Variant'-like types. +-} +type SumlikeSubset (subset :: RBT Symbol Type) (whole :: RBT Symbol Type) (subflat :: [Type]) (wholeflat :: [Type]) = + (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. +-} +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 :: [Type]) + (t :: RBT Symbol Type) + (result :: [Type]) | 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) + +{- | Convert a 'Record' into a n-ary product. +-} +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'. +-} +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 :: [Type]) + (t :: RBT Symbol Type) + (result :: [Type]) | 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) + +{- | Convert a 'Variant' into a n-ary sum. +-} +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'. +-} +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 :: RBT 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 :: RBT Symbol Type) (g :: Type -> Type) where + type RecordCode' start g :: RBT 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 :: RBT 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) :: RBT Symbol Type where + VariantCode s = VariantCode' E (G.Rep s) + +type family VariantCode' (acc :: RBT Symbol Type) (g :: Type -> Type) :: RBT 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 + +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 :: RBT 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 ( 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 :: RBT 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 ( 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 +
+ red-black-record.cabal view
@@ -0,0 +1,62 @@+cabal-version: >=2.0 +name: red-black-record +version: 1.0.0.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. + . + The keys correspond to fields + names in records, and to branch names in variants. + . + Each value type in a field or branch comes wrapped in a + type constructor of kind @Type -> Type@. + . + 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 +build-type: Simple + +library + exposed-modules: Data.RBR + Data.RBR.Examples + Data.RBR.Internal + build-depends: base >= 4.10.0.0 && < 5, + sop-core >= 0.4.0.0 && < 0.5 + hs-source-dirs: lib + 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.5, + red-black-record, + aeson >= 1.4.0.0 && < 1.5, + bytestring >= 0.10, + text >= 1.1, + profunctors >= 5, + doctest >= 0.16 + 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.5, + red-black-record, + tasty >= 0.10.1.1, + tasty-hunit >= 0.9.2 + default-language: Haskell2010
+ tests/doctests.hs view
@@ -0,0 +1,6 @@+import Test.DocTest + +main = doctest ["-ilib", + "lib/Data/RBR.hs", + "lib/Data/RBR/Examples.hs" + ]
+ tests/tests.hs view
@@ -0,0 +1,178 @@+{-# LANGUAGE DataKinds, + TypeApplications, + DeriveGeneric, + StandaloneDeriving, + PartialTypeSignatures +#-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} +module Main where + +import Data.RBR +import Data.SOP +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 "testRecordGetSet01" testRecordGetSet01, + testCase "testVariantInjectMatch01" testVariantInjectMatch01, + testCase "testProjectSubset01" testProjectSubset01, + testCase "testToRecord01" testToRecord01, + testCase "testFromRecord01" testFromRecord01, + testCase "testToVariant01" testToVariant01, + testCase "testFromVariant01" testFromVariant01 + ] + + +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) + +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) +