exception - 是否可以通过向 Haskell 添加一个新功能(我称之为 "subtype system")来发现用 Haskell 编写的程序中的大部分错误？

Question

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

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

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

以下是主要的:

如果我们可以定义一个类型，它只是 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 的“子集” , 也可以是函数的参数。但是，如果函数需要 IntNotZero ，然后是 Int是非法的。

例如:

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。

Answer 1

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

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

例如，您可以编写 zero 的类型。是 0 :

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

您会注意到类型的语法看起来就像数学的集合表示法——您将新类型定义为旧类型的子集。在本例中，您定义了 Int 的类型。 s 等于 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不可能发生。此外，当您尝试使用 divide ，它会检查你传入的参数不能为0。

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

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

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

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

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