@@ -0,0 +1,184 @@
1+{-# LANGUAGE DataKinds #-}
2+{-# LANGUAGE ExplicitNamespaces #-}
3+{-# LANGUAGE FlexibleContexts #-}
4+{-# LANGUAGE FlexibleInstances #-}
5+{-# LANGUAGE GADTs #-}
6+{-# LANGUAGE KindSignatures #-}
7+{-# LANGUAGE MultiParamTypeClasses #-}
8+{-# LANGUAGE PolyKinds #-}
9+{-# LANGUAGE RankNTypes #-}
10+{-# LANGUAGE ScopedTypeVariables #-}
11+{-# LANGUAGE TypeFamilies #-}
12+{-# LANGUAGE TypeOperators #-}
13+{-|
14+Module : Generics.SOP.DMapUtilities
15+Description : Utilities for converting between the NS/NP types of generics-sop and Dependent Maps.
16+-}
17+
18+module Generics.SOP.DMapUtilities
19+ (
20+ -- * Type Functions
21+ FunctorWrapTypeList
22+ , FunctorWrapTypeListOfLists
23+
24+ -- * Types
25+ , TypeListTag
26+
27+ -- * Conversions
28+ -- ** 'NP' \<-\> 'DM.DMap'
29+ , npToDMap
30+ , dMapToNP
31+ -- ** 'NS' \<-\> 'DSum'
32+ , nsToDSum
33+ , dSumToNS
34+
35+ -- * Functor wrapping/unwrapping utilities for 'NP'
36+ , npUnCompose
37+ , nsOfnpUnCompose
38+ , npReCompose
39+ , nsOfnpReCompose
40+
41+ -- * Utilities
42+ , npSequenceViaDMap
43+
44+ -- * Proofs
45+ , functorWrappedSListIsSList
46+ )where
47+
48+import Generics.SOP ((:.:) (Comp), K (..), NP (..), NS (..), Proxy (..), SList (..), SListI (..), SListI2, fn,
49+ hcollapse, hmap, unComp)
50+import Generics.SOP.Dict (Dict (Dict), withDict)
51+import Generics.SOP.NP (sequence'_NP)
52+import Generics.SOP.NS (ap_NS)
53+
54+import qualified Data.Dependent.Map as DM
55+import Data.Dependent.Sum (DSum ((:=>)))
56+import qualified Data.Dependent.Sum as DS
57+
58+import Data.GADT.Compare ((:~:) (..), GCompare (..), GEq (..), GOrdering (..))
59+
60+import Data.Functor.Identity (Identity (runIdentity))
61+
62+-- |A Tag type for making a 'DM.DMap' keyed by a type-level list
63+data TypeListTag (xs :: [k]) (x :: k) where -- x is in xs
64+ TLHead :: TypeListTag (x ': xs) x -- x begins xs
65+ TLTail :: TypeListTag xs x -> TypeListTag (y ': xs) x -- given that x is in xs, x is also in (y ': xs)
66+
67+instance GEq (TypeListTag xs) where
68+ geq TLHead TLHead = Just Refl
69+ geq (TLTail x) (TLTail y) = geq x y
70+ geq _ _ = Nothing
71+
72+instance GCompare (TypeListTag xs) where
73+ gcompare TLHead TLHead = GEQ
74+ gcompare TLHead (TLTail _) = GLT
75+ gcompare (TLTail _) TLHead = GGT
76+ gcompare (TLTail x) (TLTail y) = gcompare x y
77+
78+-- |Convert an 'NP' indexed by typelist xs into a 'DM.DMap' indexed by 'TypeListTag' xs
79+npToDMap :: NP f xs -> DM.DMap (TypeListTag xs) f
80+npToDMap Nil = DM.empty
81+npToDMap (fx :* npTail) = DM.insert TLHead fx $ DM.mapKeysMonotonic TLTail $ npToDMap npTail
82+
83+-- |Convert a 'DM.DMap' indexed by 'TypeListTag' xs to an 'NP'
84+-- |NB: This can fail since there is no guarantee that the 'DM.DMap' has entries for every tag. Hence it returns a 'Maybe'
85+dMapToNP :: forall xs f. SListI xs => DM.DMap (TypeListTag xs) f -> Maybe (NP f xs)
86+dMapToNP dm = sequence'_NP $ hmap (Comp . flip DM.lookup dm) makeTypeListTagNP
87+
88+-- |Convert a 'NS' indexed by a typelist xs to a 'DS.DSum' indexed by 'TypeListTag' xs
89+nsToDSum :: SListI xs => NS f xs -> DS.DSum (TypeListTag xs) f
90+nsToDSum = hcollapse . ap_NS (hmap (\tag -> (fn $ \val -> K (tag :=> val))) makeTypeListTagNP)
91+{- let nsFToNSDSum::SListI xs=>NS f xs -> NS (K (DS.DSum (TypeListTag xs) f)) xs
92+ nsFToNSDSum ns' = ap_NS (tagsToFs makeTypeListTagNP) ns'
93+ tagsToFs::SListI xs=>NP (TypeListTag xs) xs -> NP (f -.-> K (DS.DSum (TypeListTag xs) f)) xs
94+ tagsToFs = hmap (\tag -> (Fn $ \val -> K (tag :=> val)))
95+ in hcollapse . nsFToNSDSum
96+-}
97+
98+-- |Convert a 'DS.DSum' indexed by 'TypeListTag' xs into a 'NS' indexed by xs
99+dSumToNS :: DS.DSum (TypeListTag xs) f -> NS f xs
100+dSumToNS (tag :=> fa) = go tag fa
101+ where
102+ go::TypeListTag ys y -> f y -> NS f ys
103+ go TLHead fy = Z fy
104+ go (TLTail nextTag) fy = S $ go nextTag fy
105+
106+-- | Produce an NP of TypeListTags matching the type-list of the NP
107+makeTypeListTagNP :: SListI xs => NP (TypeListTag xs) xs
108+makeTypeListTagNP = go sList
109+ where
110+ go :: SList ys -> NP (TypeListTag ys) ys
111+ go SNil = Nil
112+ go SCons = TLHead :* hmap TLTail (go sList)
113+
114+-- these are here to allow moving functors in and out of typelists
115+type family FunctorWrapTypeList (f :: * -> *) (xs :: [*]) :: [*] where
116+ FunctorWrapTypeList f '[] = '[]
117+ FunctorWrapTypeList f (x ': xs) = f x ': FunctorWrapTypeList f xs
118+
119+type family FunctorWrapTypeListOfLists (f :: * -> *) (xss :: [[*]]) :: [[*]] where
120+ FunctorWrapTypeListOfLists f '[] = '[]
121+ FunctorWrapTypeListOfLists f (xs ': xsTail) = FunctorWrapTypeList f xs ': FunctorWrapTypeListOfLists f xsTail
122+
123+-- | Transform a type-list indexed product of composed functorial values into a type-list indexed product of functorial values where the inner part of the functor
124+-- composition has been moved to the type-list. The values in the product remain the same (up to types representing composition of the functors). E.g.,
125+--
126+-- > (f :.: g) 2 :* (f :.: g) 3.0 :* 'Nil :: NP (f :.: g) '[Int,Double] -> f (g 2) :* f (g 3.0) :* 'Nil :: NP f '[g Int, g Double]
127+npUnCompose :: forall f g xs. NP (f :.: g) xs -> NP f (FunctorWrapTypeList g xs)
128+npUnCompose = go
129+ where
130+ go :: NP (f :.: g) ys -> NP f (FunctorWrapTypeList g ys)
131+ go Nil = Nil
132+ go (fgx :* npTail) = unComp fgx :* go npTail
133+
134+-- | UnCompose all of the 'NP's in an "NS (NP f) xss".
135+nsOfnpUnCompose :: forall f g xss. (SListI2 xss) => NS (NP (f :.: g)) xss -> NS (NP f) (FunctorWrapTypeListOfLists g xss)
136+nsOfnpUnCompose = go sList where
137+ go :: forall yss. (SListI2 yss) => SList yss -> NS (NP (f :.: g)) yss -> NS (NP f) (FunctorWrapTypeListOfLists g yss)
138+ go SNil _ = error "An NS cannot be empty"
139+ go SCons (Z np) = Z (npUnCompose np)
140+ go SCons (S ns') = S (go sList ns')
141+
142+-- | The inverse of 'npUnCompose'. Given a type-list indexed product where all the types in the list are applications of the same functor,
143+-- remove that functor from all the types in the list and put it in the functor parameter of the 'NP'. The values in the product itself remain the same up
144+-- to types representing composition of the functors.
145+npReCompose :: forall f g xs. SListI xs => NP f (FunctorWrapTypeList g xs) -> NP (f :.: g) xs
146+npReCompose = go sList
147+ where
148+ go :: forall ys. SList ys -> NP f (FunctorWrapTypeList g ys) -> NP (f :.: g) ys
149+ go SNil Nil = Nil
150+ go SCons (fgx :* npTail) = Comp fgx :* go sList npTail
151+
152+-- | ReCompose all the 'NP's in an "NS (NP f) xss".
153+nsOfnpReCompose :: forall f g xss. (SListI2 xss) => NS (NP f) (FunctorWrapTypeListOfLists g xss) -> NS (NP (f :.: g)) xss
154+nsOfnpReCompose = go sList
155+ where
156+ go :: forall yss. (SListI2 yss) => SList yss -> NS (NP f) (FunctorWrapTypeListOfLists g yss) -> NS (NP (f :.: g)) yss
157+ go SNil _ = error "NS must be non-empty." -- this shouldn't happen since an NS can't be empty
158+ go SCons (Z np) = Z $ npReCompose np
159+ go SCons (S nsTail) = S $ go sList nsTail
160+
161+-- | Prove that "SListI xs=>(FunctorWrapTypeList f xs)" is also an instance of SListI
162+functorWrappedSListIsSList :: forall f xs. SListI xs => Proxy f -> SList xs -> Dict SListI (FunctorWrapTypeList f xs)
163+functorWrappedSListIsSList _ SNil = Dict
164+functorWrappedSListIsSList pf SCons = goCons (sList :: SList xs)
165+ where
166+ goCons :: forall y ys. SList (y ': ys) -> Dict SListI (FunctorWrapTypeList f (y ': ys))
167+ goCons SCons =
168+ let dict = functorWrappedSListIsSList pf $ (sList :: SList ys)
169+ in withDict dict Dict
170+
171+-- | sequence (in the sense of 'Data.Traversable.sequenceA') a functor f inside an 'NP'
172+-- using a function defined over a 'DM.DMap' indexed by the same type-level-list.
173+-- This is useful in cases where an efficient general solution exists for DMaps.
174+-- This can be done more simply for Applicative f but the efficiency will depend on
175+-- the particular functor and given function over 'DM.DMap'.
176+npSequenceViaDMap :: forall k (f :: * -> *) (g :: * -> *) (xs :: [*]). (Functor f, SListI xs
177+ , k ~ TypeListTag (FunctorWrapTypeList g xs))
178+ =>(DM.DMap k f -> f (DM.DMap k Identity))->NP (f :.: g) xs -> f (NP g xs)
179+npSequenceViaDMap sequenceDMap =
180+ withDict (functorWrappedSListIsSList (Proxy :: Proxy g) (sList :: SList xs)) $
181+ fmap (hmap (runIdentity . unComp) . npReCompose . (\(Just x) -> x) . dMapToNP) . sequenceDMap . npToDMap . npUnCompose
182+-- NB: The (\(Just x)->x) in there is safe!
183+-- dMapToNP has to return Maybe NP since the DMap could be incomplete.
184+-- But since we built this DMap from an NP, we know it's complete and dMapToNp will return a Just.