我可以为选定的对象附加一个唯一的、运行时确定的标记吗

Question

考虑类型B及其子类型A，由谓词P确定。一个例子是B的自然数和A的素数，一些素性测试是P。实现这样的A的智能构造函数很简单，定义为newtype或Tagged。

现在假设子类型谓词在编译时还没有完全确定。例如，让P是由IO输入确定的集合中的成员：运算符输入整数多项式的系数，我们得到一个谓词，该谓词验证给定的数字是该多项式在某个索引处的值。

我能确保每个多项式以及为其验证的值都以一种使它们彼此兼容且与任何其他多项式不兼容的方式进行标记吗我需要的操作之一是在值和它们的索引之间进行转换，我想键入保护它们以避免混淆。

这就是我想象的样子：

polynomial :: [Integer] -> Polynomial unique
toValue   :: Integer -> Polynomial unique -> Value unique
fromValue :: Integer -> Polynomial unique -> Maybe (Index unique)
toValue'   :: Index unique -> Value unique
fromValue' :: Value unique -> Index unique

重点是获得后两个总函数。

但是我不知道如何定义这个polynomial函数。它从哪里得到unique类型？

Answer 1

要以类似ST的方式进行操作，您需要一个函数库来操作Value s和Polynomial s类型，然后拥有一个类型如下的函数：

withPolynomial :: (forall s . Polynomial s -> Integer) -> [Integer] -> Integer

这将把[Integer]转换为Polynomial s，并将其传递给变元函数。然后，这个函数将执行它想要的任何操作，在适当的情况下使用函数库。任何Value s值都保证不会从封闭的withPolynomial应用程序中泄漏，因此它们不会混淆。然而，这也将阻止您存储多项式及其值，以便在未来的计算中使用。