7

我已经学习了 Haskell 大约一年，并提出了一个问题，有才华的编译器作者是否可以添加一个名为“子集”的新功能，以增强 Haskell 的类型系统以捕获许多错误，包括编译阶段的 IOExceptions。我是类型理论的新手，请原谅我的一厢情愿。

我最初的目的不是如何解决问题，而是要知道是否存在相关的解决方案，但由于某些原因，没有将解决方案引入 Haskell。

Haskell 在我心目中几乎是完美的，除了一些小事，我将在以下几行中表达我对 Haskell 未来的愿望。

以下是主要的：

如果我们可以定义一个类型，它只是Int假设 Haskell 允许我们这样做的“子集”，如下所示：

data IntNotZero = Int {except `0`} -- certainly it is not legal in Haskell, but I just assume that Haskell allows us to define a type as a "subset" of an already existing type. I'm novice of Theory of types, and forgive me.

如果函数需要 的参数Int，则 的变量IntNotZero，它只是 的“子集” Int，也可以是函数的参数。但是，如果一个函数需要 a IntNotZero，那么 aInt是非法的。

例如：

div' :: Int -> IntNotZero -> Int
div' = div

aFunction :: Int -> Int -> Int --If we casually write it, then the compiler will complain for type conflict.
aFunction = div'

aFunction2 :: Int -> Int -> Int --we have to distinguish between `Int` and `IntNotZero`.
aFunction2 m n = type n of --An assumed grammar like `case ... of` to separate "subset" from its complement. `case ...of` only works on different patterns.
                   IntNotZero -> m `div` n
                   otherwise  -> m + n

举一个更有用的例子：

data HandleNotClosed = Handle {not closed} --this type infers a Handle not closed

hGetContents' :: HandleNotClosed -> IO String --this function needs a HandleNotClosed and a Handle will make a type conflict.
hGetContents' = hGetContents

wrongMain = do
         ...
         h <- openFile "~/xxx/aa" ReadMode
         ... -- we do many tasks with h and we may casually closed h
         contents <- hGetContents' h --this will raise a type conflict, because h has type of Handle not HandleNotClosed.
         ...

rightMain = do
         ...
         h <- openFile "~/xxx/aa" ReadMode
         ... -- we do many tasks with h and we may casually closed h
         type h of -- the new grammar.
              HandleNotClosed -> do
                                   contents <- hGetContents' h
                                   ...
              otherwise       -> ...

如果我们将普通 IO 与 Exception 组合成一个新的“supset”，那么我们可能会摆脱 IOErrors。

4

4 回答 4

9

你想要的听起来类似于“细化类型”à la Liquid Haskell。这是一个外部工具，允许您通过指定保留类型的附加谓词来“优化”您的 Haskell 类型。要检查这些是否成立，您可以使用SMT 求解器来验证是否满足所有约束。

以下代码片段摘自他们的介绍性博客文章。

例如，您可以编写以下zero类型0：

{-@ zero :: { v : Int | v = 0 } @-}
zero :: Int
zero = 0

您会注意到类型的语法看起来就像数学的集合表示法——您将新类型定义为旧类型的子集。在这种情况下，您定义的Ints 类型等于 0。

您可以使用此系统编写安全分割函数：

{-@ divide :: Int -> { v : Int | v != 0 } -> Int @-}
divide :: Int -> Int -> Int
divide n 0 = error "Cannot divide by 0."
divide n d = n `div` d

当您实际尝试编译该程序时，Liquid Haskell 会发现以 0 作为分母违反了谓词，因此error无法调用 to。此外，当您尝试使用 时divide，它会检查您传入的参数不能为 0。

当然，为了使它有用，您必须能够添加有关函数的后置条件的信息，而不仅仅是前置条件。您可以通过优化函数的结果类型来做到这一点；例如，您可以想象以下类型abs：

{-@ abs :: Int -> { v : Int | 0 <= v } @-}

现在类型系统知道调用的结果abs永远不会是负数，它可以在需要验证您的程序时利用这一事实。

像其他人提到的那样，使用这种类型系统意味着您必须在代码中提供证明。Liquid Haskell 的优势在于它使用 SMT 求解器自动为您生成证明——您只需编写断言。

Liquid Haskell 仍然是一个研究项目，它受到 SMT 求解器可以合理完成的工作的限制。我自己没有使用过它，但它看起来真的很棒，而且似乎正是你想要的。我不确定的一件事是它如何与自定义类型交互，以及IO您可能想要自己研究的东西。

于 2013-06-23T12:22:45.723 回答
7

问题是编译器无法确定某些东西是否属于 type IntNotZero。例如：

f :: Int -> IntNotZero
f x = someExtremlyComplexComputation

编译器必须证明它someExtremlyComplexComputation不会产生零结果，这通常是不可能的。

解决此问题的一种方法是在普通 Haskell 中创建一个模块，该模块隐藏表示IntNotZero并仅发布智能构造函数，例如

module MyMod (IntNotZero(), intNotZero) where

newtype IntNotZero = IntNotZero Int

intNotZero :: Int -> IntNotZero
intNotZero 0 = error "Zero argument"
intNotZero x = IntNotZero x

-- etc

明显的缺点是仅在运行时检查约束。

有比 Haskell 更复杂的系统使用Dependent types。这些是依赖于值的类型，它们允许你表达你想要的。不幸的是，这些系统相当复杂，而且没有普及。如果您对此主题感兴趣，我建议您阅读Adam Chlipala 的Certified Programming with Dependent Types。

于 2013-06-23T08:49:30.697 回答
1

我们有类型，我们有价值观。类型是一组（无限）值。String是一种类型，所有可能的字符串值都是String集合的一部分。现在，关于类型和值的最重要区别在于 - 类型与编译时间有关，而值在运行时可用。

如果我们看你的第一个例子，它讨论了一个新类型，它是 Int 类型的子类型（或子集），这样“Int 的值不能为零”，这意味着你想要定义一个设置一些限制的类型值 BUT 类型是编译时间，值是运行时事物 - 编译时事物不能限制运行时事物，因为运行时事物还没有编译时事物消耗。

类似地，句柄值是一个运行时的东西，只有在运行时你才能知道它是否关闭，并且你有函数来检查句柄是否关闭。IO 是关于运行时的，你不能使用类型系统来摆脱 IOErrors。

对于运行时故障建模，您可以使用数据类型，例如Maybe或Either表示该函数可能无法执行应执行的操作，并且由于这些数据类型实现了仿函数、moands 和其他计算模式，您可以轻松地组合它们。

类型系统更像是一种结构化/设计工具，它使事情更加明确和清晰，让你更多地思考你的设计，但它不能做应该做的功能。

这部电影是：类型化的 Lambda 演算。Lambda 担任主角，键入配角 :)

于 2013-06-23T08:45:23.717 回答
1

为了扩展@augustss 的评论，很有可能使用依赖类型的语言。Haskell 不是完全依赖类型的，但它足够接近依赖类型可以“伪造”。

人们今天不常用依赖类型有几个原因

  1. 它们仍然是非常重要的研究课题
  2. 它们使类型推断复杂化和削弱
  3. 在某些情况下它们更难使用
  4. 它们可能导致类型检查花费更长的时间甚至无法终止，并且
  5. 创建生产依赖类型的编译器更加困难。

也就是说，依赖类型的支持者发现您正在寻找的错误减少非常站得住脚。他们还期望更好的安全性和更快的编译二进制文件。最后，依赖类型系统可以用作数学的“证明系统”。对于一个非常当前的示例，请考虑“同伦类型理论”Agda 代码，它正式证明了依赖类型数学的一个新领域的许多断言。

要体验依赖类型，您可以阅读/探索 Pierce 的Software Foundations或 Chlipala 的Certified Programming with Dependent Types。

对于依赖类型，您可能会引入这样的类型

div :: Int -> (x :: Int) -> (Inequal x 0) -> Int

其中第二个参数引入了类型对参数实际值的依赖性，第三个参数要求证明. 有了这样的证明（只要没有人作弊并用作该证明），就有可能确信除以第二个参数永远不会不确定。x /= 0undefined

挑战来自创建（自动或手动）作为第三个参数传入的值。对于这样一个简单的例子，它可能并不太难，但是可以对很难生成甚至不可能生成的证明的需求进行编码。

作为另一个优势的示例，请考虑

fold1 :: (f :: a -> a -> a) -> Associative f -> [a] -> a

忽略第二个参数，这只是一个常规折叠。第二个论点可以是关联的证明，f因此允许我们使用具有对数复杂度而不是线性的树状合并算法。但是，为了“证明” Associative，我们需要将应用和关联理论嵌入到我们的类型中，并有能力在其中创建证明。

存在更简单的不变量，例如普遍流行Vec的“固定长度向量”类型。这些是列表的长度（一个值）包含在类型中的列表，允许我们拥有一些不错的东西，例如

(++) :: Vec n a -> Vec m a -> Vec (n + m) a

其中，如果我们的类型系统中有一些好的加法理论（或者，更一般地说，magmas、monoids 和 groups），那么创建我们的结果类型并不难，它包含有关Vecs 长度交互方式的信息级联。

于 2013-06-24T00:34:25.347 回答