问题描述
这是我要执行的操作的简化示例.假设您有一个HList
对:
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))
现在,我想编写一个函数replaceAll
,该函数将给定类型的所有键"替换为相同类型的第一个值".例如,使用上面的HList
,我想将所有String
键替换为"1"
,这是在HList
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.
推荐答案
一个 bug 在当前的GHC中打破了这一点.一旦修复程序被合并,这应该可以正常工作.同时,另一个答案可以帮助您解决问题.
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.
首先,定义
data Elem :: k -> [k] -> Type where
Here :: Elem x (x : xs)
There :: Elem x xs -> Elem x (y : xs)
Elem x xs
告诉您在xs
中的哪里可以找到x
.另外,这是一个存在性包装器:
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
如果您在类型级别上有Elem
,则可以实现它
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)
类似地,您可以实现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))
如果类型是类型列表的元素,则可以从该类型列表的HList
中提取该类型的值:
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
(我觉得有必要指出indexH
对HList
的根本重要性.例如,HList ts
对它的索引器forall t. Elem t ts -> t
是同构的.而且,indexH
具有对偶的injS :: Elem t ts -> t -> Sum ts
适用于Sum
.)
(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
.)
同时,在类型级别上,此函数可以为您提供第一个可能的EntryOfVal
给定值类型和列表:
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)))
将实现类与FirstEntryOfVal
分开的原因是,这些类是可重用的.您可以轻松地编写返回Elem
或EntryOfVal
并实现它们的新类型族.将它们合并为一个整体类是很麻烦的,现在您必须每次重写MElem
的逻辑"(不是很多),而不是重新使用它.但是,我的方法确实带来了较高的前期成本.但是,所需的代码完全是机械的,因此可以想象TH库可以为您编写代码.我不知道可以处理的库,但singletons
计划要处理.
The reason for separating the materialization classes from FirstEntryOfVal
is because the classes are reusable. You can easily write new type families that return Elem
s or EntryOfVal
s 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.
现在,在提供EntryOfVal
证明的情况下,此函数可以为您提供一个值:
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
现在GHC可以为您做一些思考:
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))
一旦有了值,就需要找到键.出于效率(我认为O(n)vs. O(n ^ 2))的原因以及我的理智,我们不会创建EntryOfVal
的镜像,而是使用稍有不同的类型.我现在不做解释就给样板
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)
逻辑:
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)
实际值操作
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)
让GHC思考更多
updateHAllKeys :: forall k kvs. MEntriesOfKey (AllEntriesOfKey k kvs) =>
(k -> k) -> HList kvs -> HList kvs
updateHAllKeys = updateHKeys (mEntriesOfKey @_ @_ @(AllEntriesOfKey k kvs))
现在在一起:
replaceAll :: forall t kvs.
(MEntryOfVal (FirstEntryOfVal t kvs), MEntriesOfKey (AllEntriesOfKey t kvs)) =>
HList kvs -> HList kvs
replaceAll xs = updateHAllKeys (const $ indexHFirstVal @t xs) xs
这篇关于在Haskell中模拟与路径相关的类型的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!