是否有可能通过向Haskell添加一个新功能(我称之为"子类型系统")来在Haskell中编写的程序中找到大多数错误？

Question

我已经学习了大约一年的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,则a 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

你想要的听起来像液体Haskell的 "精炼类型" .这是一个外部工具,允许您通过指定保留类型的其他谓词来"优化"您的Haskell类型.要检查这些是否成立,请使用SMT求解器验证是否已满足所有约束.

以下代码段摘自其介绍性博客文章.

例如,你可以写的类型zero是0:

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

您会注意到类型的语法看起来就像数学的集合表示法 - 您将新类型定义为旧的类型.在这种情况下,您将定义Int等于0 的s 类型.

您可以使用此系统编写安全除法功能:

{-@ 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- 您可能想要自己查看的内容.

Answer 2

问题是编译器无法确定某些内容是否类型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

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

使用Dependent类型的系统比Haskell更复杂.这些是依赖于值的类型,它们允许您表达您想要的内容.不幸的是,这些系统相当复杂并且不太普遍.如果您对该主题感兴趣,我建议您阅读Adam Chlipala的" 依赖类型认证编程".