4

我发现自己在我的设计中遇到了相同的模式，我从一个带有几个数据构造函数的类型开始，最终希望能够针对这些数据构造函数进行类型化，从而将它们拆分为自己的类型，然后必须增加在我仍然需要表示多个这些类型（即集合）的情况下，需要使用 Either 或另一个标记联合来降低程序其他部分的冗长性。

我希望有人可以为我指出一种更好的方法来完成我想做的事情。让我从一个简单的例子开始。我正在为一个测试系统建模，您可以在其中拥有最终以测试结束的嵌套测试套件。所以，像这样：

data Node =
    Test { source::string }
    Suite { title::string, children::[Node] }

所以，到目前为止非常简单，本质上是一个花哨的树/叶声明。但是，我很快意识到我希望能够制作专门用于测试的功能。因此，我现在将其拆分为：

data Test = Test { source::string }
data Suite = Suite { title::string, children::[Either Test Suite] }

或者，我可能会推出“自定义”Either（特别是如果示例更复杂并且有超过 2 个选项），例如：

data Node =
   fromTest Test
   fromSuite Suite

所以，已经很不幸了，仅仅为了能够拥有一个Suite可以组合套件或测试的工具，我最终得到了一个奇怪的开销Either类（无论是实际Either的还是自定义的）。如果我使用存在类型类，我可以同时制作Test并Suite派生“Node_”，然后拥有Suite一个上述Nodes 的列表。Coproducts 将允许类似的事情，我基本上会执行相同的Either策略而没有标签的冗长。

现在让我用一个更复杂的例子来扩展。测试的结果可以是 Skipped（测试被禁用）、Success、Failure 或 Omitted（由于先前的失败，测试或套件无法运行）。同样，我最初是这样开始的：

data Result = Success | Omitted | Failure | Skipped
data ResultTree =
    Tree { children::[ResultTree], result::Result } |
    Leaf Result

但我很快意识到我希望能够编写获取特定结果的函数，更重要的是，让类型本身强制执行所有权属性：一个成功的套件必须只有成功或跳过的孩子，失败的孩子可以是任何东西，省略只能自己省略了，等等。所以现在我得到了这样的结果：

data Success = Success { children::[Either Success Skipped] }
data Failure = Failure { children::[AnyResult] }
data Omitted = Omitted { children::[Omitted] }
data Skipped = Skipped { children::[Skipped] }
data AnyResult =
  fromSuccess Success |
  fromFailure Failure |
  fromOmitted Omitted |
  fromSkipped Skipped

同样，我现在有了这些奇怪的“包装器”类型，比如AnyResult，但是，我得到了过去只能从运行时操作中强制执行的东西的类型强制。有没有更好的策略不涉及打开存在类型类之类的功能？

4

2 回答 2

3

读到您的句子，我首先想到的是：“我很快意识到我希望能够编写具有特定结果的函数”是Refinement Types。

它们只允许从类型中获取一些值作为输入，并使这些约束在编译时检查/错误。

有一段来自 HaskellX 2018 的演讲视频，介绍了 LiquidHaskell，它允许在 Haskell 中使用细化类型：

https://skillsmatter.com/skillscasts/11068-keynote-looking-forward-to-niki-vazou-s-keynote-at-haskellx-2018

您必须装饰您的 haskell 函数签名，并安装 LiquidHaskell：

f :: Int -> i : Int {i | i < 3} -> Int将是一个函数，它只能接受Int带有 value的第二个参数< 3，在编译时检查。

你不妨对你的Result类型施加约束。

于 2018-10-24T16:31:52.570 回答
2

我想你可能正在寻找的是GADTswith DataKinds。这使您可以将数据类型中每个构造函数的类型细化为一组特定的可能值。例如：

data TestType = Test | Suite

data Node (t :: TestType) where
  TestNode :: { source :: String } -> Node 'Test
  SuiteNode :: { title :: String, children :: [SomeNode] } -> Node 'Suite

data SomeNode where
  SomeNode :: Node t -> SomeNode

那么当一个函数只对测试起作用时，它可以采用Node 'Test; 在套房上，一个Node 'Suite；在任何一个上，一个多态的Node a. 在 a 上进行模式匹配时Node a，每个case分支都可以访问一个等式约束：

useNode :: Node a -> Foo
useNode node = case node of
  TestNode source ->          {- here it’s known that (a ~ 'Test) -}
  SuiteNode title children -> {- here, (a ~ 'Suite) -}

实际上，如果您采用具体Node 'Test的 ，编译器将不允许该SuiteNode分支，因为它永远无法匹配。

SomeNode是一个包含Node未知类型的存在；如果需要，您可以为此添加额外的类约束。

你可以做类似的事情Result：

data ResultType = Success | Omitted | Failure | Skipped

data Result (t :: ResultType) where
  SuccessResult
    :: [Either (Result 'Success) (Result 'Skipped)]
    -> Result 'Success
  FailureResult
    :: [SomeResult]
    -> Result 'Failure
  OmittedResult
    :: [Result 'Omitted]
    -> Result 'Omitted
  SkippedResult
    :: [Result 'Skipped]
    -> Result 'Skipped

data SomeResult where
  SomeResult :: Result t -> SomeResult

当然，我假设在您的实际代码中有这些类型的更多信息；事实上，它们并不代表太多。当您进行动态计算（例如运行可能产生不同类型结果的测试）时，您可以将其包装在SomeResult.

为了处理动态结果，您可能需要向编译器证明两种类型相等；为此，我指导您使用Data.Type.Equality，它提供了一种类型，当两种类型和相等时，该类型a :~: b由单个构造函数占据；您可以对此进行模式匹配以告知类型检查器有关类型相等性，或使用各种组合器来执行更复杂的证明。Reflab

GADTs与（和ExistentialTypes，不太常见的） is结合使用也很有用RankNTypes，它基本上使您能够将多态函数作为参数传递给其他函数；如果您想普遍使用存在主义，这是必要的：

consumeResult :: SomeResult -> (forall t. Result t -> r) -> r
consumeResult (SomeResult res) k = k res

这是延续传递风格(CPS) 的一个示例，延续在哪里k。

最后一点，这些扩展被广泛使用并且基本上没有争议。当您可以更直接地表达您的意思时，您不必担心选择（大多数）类型系统扩展。

于 2018-10-25T18:05:51.023 回答