在 Haskell 中模拟路径依赖类型

Question

这是我想做的简化示例。假设您有一对HList：

let hlist = HCons (1, "1") (HCons ("0", 2) (HCons ("0", 1.5) HNil))

现在我想编写一个函数replaceAll，它将用相同类型的第一个“值”替换给定类型的所有“键”。例如，对于上面的HList，我想用"1" 替换所有String 键，这是在String 中找到的String 类型的第一个值@

 replaceAll @String hlist =
    HCons (1, "1") (HCons ("1", 2) (HCons ("1", 1.5) HNil))

这似乎需要依赖路径的类型才能“提取”第一对的类型并能够在第二步中使用它来指导密钥的替换，但我不知道如何将其编码为哈斯克尔。

Answer 1

这是一个证明搜索问题（“在此列表中查找 String 的出现”），因此您可以预期解决方案将涉及类型类 Prolog。我将回答您的问题的一个更简单的版本（即“找到String 的第一次 出现”）并让您弄清楚如何根据您的具体用例进行调整。

由于我们正在进行证明搜索，让我们先写下我们将要搜索的证明对象。

data Contains a as where
    Here :: Contains a (a ': as)
    There :: Contains a as -> Contains a (b ': as)

Contains a as 类型的值是您可以在类型级别列表as 中找到a 的建设性证明。在结构上，Contains 就像一个自然数（将There (There Here) 与S (S Z) 比较）标识a 在列表as 中的位置。要证明a 在as 中，请给出它的索引。

例如，您可以在HList 中的给定位置使用相同类型的新元素replace。

replace :: a -> Contains a as -> HList as -> HList as
replace x Here (HCons y ys) = HCons x ys
replace x (There i) (HCons y ys) = HCons y (replace x i ys)

---

我们想使用类型类 Prolog 在给定列表中搜索a。有两种情况 - 要么您在列表的头部找到 a，要么在尾部的某处。 （如果a 不在as 中，使用contains 将失败并出现“无实例”错误。）理想情况下，我们会这样写：

class CONTAINS a as where
    contains :: Contains a as

instance CONTAINS a (a ': as) where
    contains = Here

instance CONTAINS a as => CONTAINS a (b ': as) where
    contains = There contains  -- recursively call `contains` on the sublist

但这不符合重叠实例规则。在实例搜索期间不检查实例上下文和类型相等性 - 阐述器不会回溯 - 因此这些实例都没有比另一个更具体。

幸运的是，a well-known solution 解决了这个问题。它涉及使用封闭类型族来区分a 和b。你用一个额外的参数定义了一个辅助类CONTAINS'，在这种情况下Bool告诉你a是否可以在as的头部找到。

class CONTAINS' (eq :: Bool) a (as :: [*]) where
    contains' :: Contains a as

然后为eq 为True 或False 的情况定义实例。阐述者可以区分这些实例，因为True 和False 明显不同。请注意，step case 递归调用CONTAINS。

instance CONTAINS' True a (a ': as) where
    contains' = Here

instance CONTAINS a as => CONTAINS' False a (b ': as) where
    contains' = There contains

最后，您根据CONTAINS' 定义您的CONTAINS 实例，并使用==（一个测试其参数是否相等的封闭类型族）的结果来选择一个实例。

instance CONTAINS' (a == b) a (b ': as) => CONTAINS a (b ': as) where
    contains = contains' @(a == b)

（这是布尔类型族为数不多的可接受用途之一。）

现在您可以像使用任何其他课程一样使用CONTAINS。当您尝试实例化a 和as 时，GHC 将尝试在as 中搜索a，contains 方法将返回其索引。

example :: Contains Int '[Bool, Int, Char]
example = contains

-- "no instance for CONTAINS"
failingExample :: Contains String '[Bool, Int, Char]
failingExample = contains

这是一个相当简单的例子，代码已经很乱了。您绝对可以以相同的方式处理您的问题中的示例，但所有人都告诉我，我不相信在这种情况下静态检查值得复杂性。您是否考虑过基于Typeable 的实现？

Answer 2

bug 在当前的 GHC 中打破了这一点。一旦修复被合并，这应该可以正常工作。与此同时，另一个答案可以让你渡过难关。

首先，定义

data Elem :: k -> [k] -> Type where
  Here :: Elem x (x : xs)
  There :: Elem x xs -> Elem x (y : xs)

Elem x xs 告诉您在哪里可以找到xs 中的x。此外，这是一个存在包装器：

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，你可以实现它

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 中提取该类型的值：

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。）

同时，在类型级别上，这个函数可以给你第一个可能的EntryOfVal给定一个值类型和一个列表：

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 分开的原因是因为这些类是可重用的。您可以轻松编写返回 Elems 或 EntryOfVals 的新类型族并将它们具体化。将它们合并到一个整体类中很麻烦，现在您必须每次都重写MElem 的“逻辑”（不是很多），而不是重复使用它。然而，我的方法确实会带来更高的前期成本。但是，所需的代码完全是机械的，因此可以想象一个 TH 库可以为您编写它。我不知道有哪个库可以 处理这个问题，但singletons 计划这样做。

现在，这个函数可以根据EntryOfVal 证明为您提供一个值：

indexHVal :: forall v kvs. EntryOfVal v kvs -> HList kvs -> v
indexHVal (EntryOfVal e) = snd . indexH e

现在 GHC 可以为您做一些思考：

indexHFirstVal :: forall v kvs. MEntryOfVal (FirstEntryOfVal v kvs) =>
                  HList kvs -> v
indexHFirstVal = indexHVal (mEntryOfVal @_ @_ @(FirstEntryOfVal v kvs))

一旦你有了价值，你就需要找到钥匙。出于效率考虑（我认为 O(n) 与 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 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