Here is a simplified example of what I want to do. Let's say you have a HList of pairs:
let hlist = HCons (1, "1") (HCons ("0", 2) (HCons ("0", 1.5) HNil))
Now I want to write a function replaceAll which will replace all the "keys" of a given type with the first "value" of the same type. For example, with the HList above I would like to replace all the String keys with "1" which is the first value of type String found in the HList
replaceAll @String hlist =
HCons (1, "1") (HCons ("1", 2) (HCons ("1", 1.5) HNil))
This seems to require path-dependent types in order to "extract" the type of the first pair and being able to use it to direct the replacement of keys in a second step but I don't know how to encode this in Haskell.
A bug breaks this in current GHCs. Once the fix is merged in, this should work fine. In the meantime, the other answer can tide you over.
First, define
data Elem :: k -> [k] -> Type where
Here :: Elem x (x : xs)
There :: Elem x xs -> Elem x (y : xs)
An Elem x xs tells you where to find an x in an xs. Also, here's an existential wrapper:
data EntryOfVal v kvs = forall k. EntryOfVal (Elem (k, v) kvs)
-- to be clear, this is the type constructor (,) :: Type -> Type -> Type
type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type where
EntryOfValKey ('EntryOfVal (_ :: Elem (k, v) kvs)) = k
type family GetEntryOfVal (eov :: EntryOfVal v kvs) :: Elem (EntryOfValKey eov, v) kvs where
GetEntryOfVal ('EntryOfVal e) = e
If you have an Elem at the type level, you may materialize it
class MElem (e :: Elem (x :: k) xs) where
mElem :: Elem x xs
instance MElem Here where
mElem = Here
instance MElem e => MElem (There e) where
mElem = There (mElem @_ @_ @_ @e)
Similarly, you may materialize an EntryOfVal
type MEntryOfVal eov = MElem (GetEntryOfVal eov) -- can be a proper constraint synonym
mEntryOfVal :: forall v kvs (eov :: EntryOfVal v kvs).
MEntryOfVal eov =>
EntryOfVal v kvs
mEntryOfVal = EntryOfVal (mElem @_ @_ @_ @(GetEntryOfVal eov))
If a type is an element of a list of types, then you may extract a value of that type from an HList of that list of types:
indexH :: Elem t ts -> HList ts -> t
indexH Here (HCons x _) = x
indexH (There i) (HCons _ xs) = indexH i xs
(I feel the need to point out how fundamentally important indexH is to HList. For one, HList ts is isomorphic to its indexer forall t. Elem t ts -> t. Also, indexH has a dual, injS :: Elem t ts -> t -> Sum ts for suitable Sum.)
Meanwhile, up on the type level, this function can give you the first possible EntryOfVal given a value type and a list:
type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs where
FirstEntryOfVal v ((k, v) : _) = 'EntryOfVal Here
FirstEntryOfVal v (_ : kvs) = 'EntryOfVal (There (GetEntryOfVal (FirstEntryOfVal v kvs)))
The reason for separating the materialization classes from FirstEntryOfVal is because the classes are reusable. You can easily write new type families that return Elems or EntryOfVals and materialize them. Merging them together into one monolithic class is messy, and now you have to rewrite the "logic" (not that there is much) of MElem every time instead of reusing it. My approach does, however, give a higher up-front cost. However, the code required is entirely mechanical, so it is conceivable that a TH library could write it for you. I don't know a library that can handle this, but singletons plans to.
Now, this function can get you a value given a EntryOfVal proof:
indexHVal :: forall v kvs. EntryOfVal v kvs -> HList kvs -> v
indexHVal (EntryOfVal e) = snd . indexH e
And now GHC can do some thinking for you:
indexHFirstVal :: forall v kvs. MEntryOfVal (FirstEntryOfVal v kvs) =>
HList kvs -> v
indexHFirstVal = indexHVal (mEntryOfVal @_ @_ @(FirstEntryOfVal v kvs))
Once you have the value, you need to find the keys. For efficiency (O(n) vs. O(n^2), I think) reasons and for my sanity, we won't make a mirror of EntryOfVal, but use a slightly different type. I'll just give the boilerplate without explanation, now
-- for maximal reuse:
-- data All :: (k -> Type) -> [k] -> Type
-- where an All f xs contains an f x for every x in xs
-- plus a suitable data type to recover EntriesOfKey from All
-- not done here mostly because All f xs's materialization
-- depends on f's, so we'd need more machinery to generically
-- do that
-- in an environment where the infrastructure already exists
-- (e.g. in singletons, where our materializers decompose as a
-- composition of SingI materialization and SingKind demotion)
-- using All would be feasible
data EntriesOfKey :: Type -> [Type] -> Type where
Nowhere :: EntriesOfKey k '[]
HereAndThere :: EntriesOfKey k kvs -> EntriesOfKey k ((k, v) : kvs)
JustThere :: EntriesOfKey k kvs -> EntriesOfKey k (kv : kvs)
class MEntriesOfKey (esk :: EntriesOfKey k kvs) where
mEntriesOfKey :: EntriesOfKey k kvs
instance MEntriesOfKey Nowhere where
mEntriesOfKey = Nowhere
instance MEntriesOfKey e => MEntriesOfKey (HereAndThere e) where
mEntriesOfKey = HereAndThere (mEntriesOfKey @_ @_ @e)
instance MEntriesOfKey e => MEntriesOfKey (JustThere e) where
mEntriesOfKey = JustThere (mEntriesOfKey @_ @_ @e)
The logic:
type family AllEntriesOfKey (k :: Type) (kvs :: [Type]) :: EntriesOfKey k kvs where
AllEntriesOfKey _ '[] = Nowhere
AllEntriesOfKey k ((k, _) : kvs) = HereAndThere (AllEntriesOfKey k kvs)
AllEntriesOfKey k (_ : kvs) = JustThere (AllEntriesOfKey k kvs)
The actual value manipulation
updateHKeys :: EntriesOfKey k kvs -> (k -> k) -> HList kvs -> HList kvs
updateHKeys Nowhere f HNil = HNil
updateHKeys (HereAndThere is) f (HCons (k, v) kvs) = HCons (f k, v) (updateHKeys is f kvs)
updateHKeys (JustThere is) f (HCons kv kvs) = HCons kv (updateHKeys is f kvs)
Get GHC to think some more
updateHAllKeys :: forall k kvs. MEntriesOfKey (AllEntriesOfKey k kvs) =>
(k -> k) -> HList kvs -> HList kvs
updateHAllKeys = updateHKeys (mEntriesOfKey @_ @_ @(AllEntriesOfKey k kvs))
All together now:
replaceAll :: forall t kvs.
(MEntryOfVal (FirstEntryOfVal t kvs), MEntriesOfKey (AllEntriesOfKey t kvs)) =>
HList kvs -> HList kvs
replaceAll xs = updateHAllKeys (const $ indexHFirstVal @t xs) xs