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 中对其进行编码。
解决方案
这是一个证明搜索问题(“在此列表中查找出现的String
”),因此您可以预期该解决方案将涉及类型类 Prolog。我将回答您的问题的一个更简单的版本(即“找到第一个出现的String
”),并让您弄清楚如何针对您的确切用例进行调整。
由于我们正在进行证明搜索,让我们首先写下我们将要搜索的证明对象。
data Contains a as where
Here :: Contains a (a ': as)
There :: Contains a as -> Contains a (b ': as)
type 的值是您可以在 type-level listContains a as
中找到的建设性证明。在结构上,就像一个自然数(与 比较)标识列表中的位置。为了证明那是在你给它的索引。a
as
Contains
There (There Here)
S (S Z)
a
as
a
as
例如,您可以replace
在一个给定位置的HList
元素与一个相同类型的新元素。
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)
a
我们想使用类型类 Prolog 在给定列表中搜索一个。有两种情况——要么你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
区分b
。CONTAINS'
你定义了一个带有额外参数的辅助类,在这种情况下,一个Bool
告诉你是否a
可以在as
.
class CONTAINS' (eq :: Bool) a (as :: [*]) where
contains' :: Contains a as
eq
然后为isTrue
或的情况定义实例False
。阐述者可以区分这些实例,因为True
和False
明显不同。请注意,步骤案例递归调用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 将尝试搜索a
inside as
,并且该contains
方法将返回其索引。
example :: Contains Int '[Bool, Int, Char]
example = contains
-- "no instance for CONTAINS"
failingExample :: Contains String '[Bool, Int, Char]
failingExample = contains
这是一个相当简单的例子,代码已经很乱了。您绝对可以以相同的方式处理您的问题中的示例,但所有人都告诉我,我不相信在这种情况下静态检查值得复杂性。您是否考虑过基于 的实现Typeable
?
推荐阅读
- javascript - 比较两个 JavaScript 对象/数组值
- javascript - 如何从嵌套钩子函数访问数据属性?
- wcf - WCF:找不到 X.509 证书
- arrays - 动态数组不接受在 1x2 中重新调整尺寸(2x2 和 2x1 有效)
- python - 如何将充满数字字符串的csv文件读取到numpy数组中
- python - 如何快速向数据框插入一行?
- flutter - 当我从 FLUTTER 的下拉列表中更新数据时出错?
- c# - 当我使用 .NET Core HttpClient 时,Google FCM 给了我 BadRequest
- c - 函数位于目标文件之一中,但链接器未链接它们
- javascript - 当 api 的加载变量为 false 时反应更新视图