haskell - 在Haskell中模拟与路径相关的类型

这是我要做什么的简化示例。假设您有一个HList对：let hlist = HCons (1, "1") (HCons ("0", 2) (HCons ("0", 1.5) HNil))现在，我想编写一个函数replaceAll，它将用相同类型的第一个“值”替换给定类型的所有“键”。例如，使用上面的HList，我想用String替换所有"1"键，这是在String中找到的HList类型的第一个值 replaceAll @String hlist = HCons (1, "1") (HCons ("1", 2) (HCons ("1", 1.5) HNil))这似乎需要依赖于路径的类型，以便“提取”第一对的类型，并能够在第二步中使用它来指导密钥的替换，但是我不知道如何在Haskell中对其进行编码。 最佳答案 bug在当前GHC中打破了这一点。修复程序合并后，就可以正常工作。同时，其他答案也可以帮您解决。首先，定义data Elem :: k -> [k] -> Type where Here :: Elem x (x : xs) There :: Elem x xs -> Elem x (y : xs)Elem x xs告诉您在x中的哪里可以找到xs。另外，这是一个存在性包装器：data EntryOfVal v kvs = forall k. EntryOfVal (Elem (k, v) kvs)-- to be clear, this is the type constructor (,) :: Type -> Type -> Typetype family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type where EntryOfValKey ('EntryOfVal (_ :: Elem (k, v) kvs)) = ktype family GetEntryOfVal (eov :: EntryOfVal v kvs) :: Elem (EntryOfValKey eov, v) kvs where GetEntryOfVal ('EntryOfVal e) = e如果在类型级别具有Elem，则可以实现它class MElem (e :: Elem (x :: k) xs) where mElem :: Elem x xsinstance MElem Here where mElem = Hereinstance MElem e => MElem (There e) where mElem = There (mElem @_ @_ @_ @e)同样，您可以实现EntryOfValtype MEntryOfVal eov = MElem (GetEntryOfVal eov) -- can be a proper constraint synonymmEntryOfVal :: forall v kvs (eov :: EntryOfVal v kvs). MEntryOfVal eov => EntryOfVal v kvsmEntryOfVal = EntryOfVal (mElem @_ @_ @_ @(GetEntryOfVal eov))如果类型是类型列表的元素，则可以从该类型列表的HList中提取该类型的值：indexH :: Elem t ts -> HList ts -> tindexH Here (HCons x _) = xindexH (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：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)))将实现类与EntryOfVal分开的原因是，这些类是可重用的。您可以轻松地编写返回FirstEntryOfVal或Elem并实现它们的新类型族。将它们合并到一个整体类中是很麻烦的，现在您必须每次都重写EntryOfVal的“逻辑”（不是很多），而不是重新使用它。但是，我的方法确实带来了较高的前期成本。但是，所需的代码完全是机械的，因此可以想象TH库可以为您编写代码。我不知道一个可以处理此问题的库，但是MElem计划这样做。现在，给定singletons证明，此函数可以为您提供一个值：indexHVal :: forall v kvs. EntryOfVal v kvs -> HList kvs -> vindexHVal (EntryOfVal e) = snd . indexH e现在，GHC可以为您做一些思考：indexHFirstVal :: forall v kvs. MEntryOfVal (FirstEntryOfVal v kvs) => HList kvs -> vindexHFirstVal = indexHVal (mEntryOfVal @_ @_ @(FirstEntryOfVal v kvs))一旦有了值，就需要找到键。出于效率（我认为O（n）vs.O（n ^ 2））的原因以及我的理智，我们不会制作EntryOfVal的镜像，而是使用稍有不同的类型。我现在不做解释就给样板-- 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 feasibledata 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 kvsinstance MEntriesOfKey Nowhere where mEntriesOfKey = Nowhereinstance 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 kvsupdateHKeys Nowhere f HNil = HNilupdateHKeys (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 kvsupdateHAllKeys = updateHKeys (mEntriesOfKey @_ @_ @(AllEntriesOfKey k kvs))现在都在一起了：replaceAll :: forall t kvs. (MEntryOfVal (FirstEntryOfVal t kvs), MEntriesOfKey (AllEntriesOfKey t kvs)) => HList kvs -> HList kvsreplaceAll xs = updateHAllKeys (const $ indexHFirstVal @t xs) xs