在Haskell中模拟与路径相关的类型 [英] Simulate a path-dependent type in Haskell

问题描述

这是我要执行的操作的简化示例.假设您有一个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 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.

现在，在提供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中模拟与路径相关的类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！