Haskell类型表示另一种类型的子集

Question

我认为当给定指定类型的参数时,函数永远不会失败.

但是看看这个看似无害的代码:

readInts :: String -> [Int]
readInts = map read . words

它的类型签名过于笼统,事实上,对于任何不是由空格分隔的整数组成的字符串,它都会失败,其类型应为:

readInts :: SpaceSeparatedIntegersString -> [Int]

当您尝试构建SpaceSeparatedIntegersString不符合规定标准的程序时程序失败.

• 实施SpaceSeparatedIntegersString一个明智的想法？

• 如果是我怎样才能实现这样的类型？(我只是问一个一般的想法/提示/推动正确的方向,而不是完整的代码)

• 我是否应该接受String格式化不正确时我的函数会失败(也就是说,我在问题开头的陈述是错误的)？

• 我应该在函数定义中使用保护子句吗？

Answer 1

你的目标是高尚的,但需要非常精确的类型.依赖类型,例如Agda,Coq,Idris和其他语言中提供的类型可以实现您的建议.例如在Coq,

Definition SpaceSeparatedIntegersString: Type :=
   { s: string | spaceSeparatedIntegers s } .
Definition spaceSeparatedIntegers (s: String): Prop := ...

问题在于,无论谁想要构建SpaceSeparatedIntegersString价值,都必须提供相关财产的正式证明.这是可行的,但需要一些关心,时间和数学技能.

在Haskell中,将类型保证移动到输出类型更为常见.我们可以使输出类型更弱,而不是使输入类型更强:

readInts :: String -> Maybe [Int]

这不是那么精确,但可以在不必证明任何事情的情况下使用.

或者,SpaceSeparatedIntegersString通过在模块中声明它而不导出其值构造函数,使其成为不透明类型.

module Foo(SpaceSeparatedIntegersString(), ...)
data SpaceSeparatedIntegersString = S String        -- S is private

这样,模块的用户只能通过模块导出的功能来操作它.需要注意的是,可以制作一堆(导出的)组合器,以保证类型的值SpaceSeparatedIntegersString永远不会包含无效的字符串.例如,

combine :: SpaceSeparatedIntegersString 
        -> SpaceSeparatedIntegersString
        -> SpaceSeparatedIntegersString 
combine (S x) (S y) = S (x ++ " " ++ y)

这并不完全是直截了当的 - 如果你想允许一般的字符串操作,你可能最终会Maybe ...在某些情况下返回.

Answer 2

您可能不应该实施SpaceSeparatedIntegerString。如果您做了一个抽象的数据类型将是最简单的事情。您不应该接受您的函数应该失败，至少不能接受“模式匹配失败”的含义。您应该制作一个返回类似的函数Maybe [Int]。

您不应该实施的原因SpaceSeparatedIntegerString可能是将问题推到了其他地方。您可能是String从某些输入中获取s的，所以在某个地方需要一个函数String -> SpaceSeparatedIntegerString，这同样会失败。在某些时候，除非完全静态指定了唯一的值，否则您需要从结构化的数据转到结构化的数据。

关键是从结构化程度较低的数据到结构化程度更高的数据（或从类型较少的数据到类型较多的数据）实际上总是部分操作。实际上，解析是将结构化程度较低的数据转换为结构化程度较高的数据的过程。你什么应该做，不过，在与你的原则，就是尽可能的实际具体化回收的结构入式系统。所以isValidUri :: String -> Bool是坏的，因为是makeUri :: String -> Maybe String的，但makeUri :: String -> Maybe Uri在那里Uri是可以代表完全有效的URI类型是好的。