Haskell在编译时可以捕获哪些类型的类型错误,而Java无法捕获?[已关闭]静态类型不变性类型推断结论类型转换更强大的类型
我刚刚开始学习Haskell,并不断看到对其强大类型系统的引用。我看到许多实例中,推理比Java更强大,但也暗示它可以在编译时捕获更多错误,因为它具有优越的类型系统。所以,我想知道是否有可能解释Haskell在编译时可以捕获哪些类型的错误,而Java无法捕获。
我刚刚开始学习Haskell,并不断看到对其强大类型系统的引用。我看到许多实例中,推理比Java更强大,但也暗示它可以在编译时捕获更多错误,因为它具有优越的类型系统。所以,我想知道是否有可能解释Haskell在编译时可以捕获哪些类型的错误,而Java无法捕获。
说Haskell的类型系统可以捕获比Java更多的错误,这有点误导。让我们稍微解开一下。
Java和Haskell都是静态类型语言。我的意思是,它们在编译时就知道语言中给定表达式的类型。对于Java和Haskell来说,这有许多优点,即它允许编译器检查表达式是否“sane”,以获得一些合理的sane定义。
是的,Java允许某些“混合类型”表达式,例如,有些人可能会认为这是不安全或不好的,但这是一个主观的选择。最后,它只是Java语言提供的一个功能,无论好坏。"abc" + 2
要了解Haskell代码如何被认为比Java(或C,C++等)代码更不容易出错,您必须考虑语言不变性的类型系统。在纯(正常)Haskell代码中,没有副作用。也就是说,程序中的任何值,一旦创建,就可能永远不会改变。当我们计算某些东西时,我们正在从旧结果创建新结果,但我们不会修改旧值。事实证明,从安全的角度来看,这具有一些非常方便的后果。当我们编写代码时,我们可以确定程序中任何地方的任何其他内容都不会影响我们的功能。事实证明,副作用是许多编程错误的原因。例如,C 中的一个共享指针在一个函数中释放,然后在另一个函数中访问,从而导致崩溃。或者在 Java 中设置为 null 的变量,
String foo = "bar";
foo = null;
Char c = foo.charAt(0); # Error!
这在正常的Haskell代码中是不可能发生的,因为一旦定义,就无法改变。这意味着它不能设置为 。foo
null
现在,您可能想知道类型系统如何参与所有这些,这毕竟是您所询问的。好吧,尽管不变性很好,但事实证明,在没有任何突变的情况下,你能做的有趣的工作很少。从文件中读取?突变。写入磁盘?突变。与网络服务器通信?突变。那么我们该怎么办呢?为了解决这个问题,Haskell使用其类型系统来封装一种类型中的突变,称为IO Monad。例如,从文件中读取,可以使用此功能,
readFile :: FilePath -> IO String
请注意,结果的类型不是字符串
,而是 。通俗地说,这意味着结果将IO(副作用)引入程序。在一个格式良好的程序中,IO将只发生在IO monad内部,从而使我们能够非常清楚地看到哪里可能发生副作用。此属性由类型系统强制执行。其他类型只能在程序的功能内产生其结果,即副作用。因此,现在我们已经非常整洁,很好地隔离了程序受控部分的危险副作用。当你得到的结果时,任何事情都可能发生,但至少这不会在任何地方发生,只在函数中,并且只能作为类型的结果。IO String
IO a
main
IO String
main
IO a
现在需要明确的是,您可以在代码中的任何位置创建值。您甚至可以在函数外部操作它们,但在函数体中要求结果之前,实际上不会进行任何操作。例如IO a
main
main
strReplicate :: IO String
strReplicate =
readFile "somefile that doesn't exist" >>= return . concat . replicate 2
此函数从文件中读取输入,复制该输入并将复制的输入追加到原始输入的末尾。因此,如果文件包含字符,这将创建一个包含 内容 。您可以在代码中的任何位置调用此函数,但 Haskell 实际上只会在函数中找到表达式时才尝试读取该文件,因为它是 .这样abc
String
abcabc
main
IO
Monad
main :: IO ()
main =
strReplicate >>=
putStrLn
这几乎肯定会失败,因为您请求的文件可能不存在,但它只会在这里失败。您只需要担心副作用,而不是像许多其他语言那样在代码中无处不在。
总的来说,IO和Monads都比我在这里介绍的要多得多,但这可能超出了你的问题范围。
现在还有一个方面。类型推断
Haskell使用非常高级的类型推理系统,它允许您编写静态类型的代码,而无需编写类型注释,例如在Java中。GHC可以推断出几乎任何表达的类型,甚至是非常复杂的表达式。String foo
这对我们的安全讨论意味着,无论在程序中使用实例的任何地方,类型系统都将确保它不能用于产生意外的副作用。你不能把它扔到一个,然后只要你想要的地方/时间得到结果。您必须在 main
函数中显式引入副作用。IO a
String
类型推理系统还具有一些其他不错的属性。通常人们喜欢脚本语言,因为他们不必像在Java或C中那样为类型编写所有样板。这是因为脚本语言是动态类型的,或者表达式的类型仅在解释器运行表达式时才计算。这使得这些语言可以说更容易出错,因为在运行代码之前,您将不知道是否有错误的表达式。例如,你可以在Python中说这样的话。
def foo(x,y):
return x + y
这样做的问题是,它可以是任何东西。所以这很好,x
y
foo(1,2) -> 3
但这会导致错误,
foo(1,[]) -> Error
我们现在有办法检查它是否无效,直到它被运行。
了解所有静态类型语言都没有这个问题非常重要,包括Java。从这个意义上说,Haskell并不比Java更安全。Haskell和Java都可以保护你免受这种类型的错误,但是在Haskell中,你不必为了安全而编写所有类型,它们的类型系统可以推断类型。通常,在 Haskell 中注释函数的类型被认为是一种很好的做法,即使您不必这样做。但是,在函数体中,您很少需要指定类型(有一些奇怪的边缘情况, 您将这样做)。
希望这有助于阐明Haskell如何保证您的安全。关于Java,你可能会说在Java中,你必须与类型系统一起工作才能编写代码,但在Haskell中,类型系统适合你。
一个区别是Java允许动态类型转换,例如(下面是愚蠢的例子):
class A { ... }
static String needsA(A a) { ... }
Object o = new A();
needsA((A) o);
类型强制转换可能导致运行时类型错误,这可以被视为类型不安全的原因。当然,任何优秀的Java程序员都会将强制转换视为最后的手段,而是依靠类型系统来确保类型安全。
在Haskell中,(大致)没有子类型,因此没有类型转换。最接近转换的特征是(不经常使用的)库,如下所示Data.Typeable
foo :: Typeable t => t -> String
foo x = case cast x :: A of -- here x is of type t
Just y -> needsA y -- here y is of type A
Nothing -> "x was not an A"
大致对应于
String foo(Object x) {
if (x instanceof A) {
A y = (A) x;
return needsA(y);
} else {
return "x was not an A";
}
}
Haskell和Java之间的主要区别在于,在Java中,我们有单独的运行时类型检查()和cast()。如果检查不能确保强制转换成功,这可能会导致运行时错误。instanceof
(A)
我记得在引入泛型之前,强制转换是Java中的一个大问题,因为例如,使用集合迫使你执行大量的转换。有了泛型,Java类型系统得到了极大的改进,现在在Java中强制转换应该不那么常见,因为它们不太常用。
回想一下,泛型类型在运行时在Java中被擦除,因此代码如
if (x instanceof ArrayList<Integer>) {
ArrayList<Integer> y = (ArrayList<Integer>) x;
}
不起作用。由于我们无法检查 的参数,因此无法完全执行检查。也因为这个擦除,如果我没记错的话,即使转换是不同的,也可以成功,只是以后导致运行时类型错误,即使转换没有出现在代码中。ArrayList
x
ArrayList<String>
Haskell 机器不会在运行时擦除类型。Data.Typeable
Haskell GADT 和(Coq、Agda 等)依赖类型扩展了传统的静态类型检查,以便在编译时对代码强制实施更强大的属性。
例如,考虑Haskell函数。下面是一个示例:zip
zip (+) [1,2,3] [10,20,30] = [1+10,2+20,3+30] = [11,22,33]
这以“逐点”方式适用于两个列表。它的定义是:(+)
-- for the sake of illustration, let's use lists of integers here
zip :: (Int -> Int -> Int) -> [Int] -> [Int] -> [Int]
zip f [] _ = []
zip f _ [] = []
zip f (x:xs) (y:ys) = f x y : zip xs ys
但是,如果我们传递不同长度的列表,会发生什么情况?
zip (+) [1,2,3] [10,20,30,40,50,60,70] = [1+10,2+20,3+30] = [11,22,33]
一个被默默截断的时间越长。这可能是一个意外的行为。可以将 zip 重新定义为:
zip :: (Int -> Int -> Int) -> [Int] -> [Int] -> [Int]
zip f [] [] = []
zip f (x:xs) (y:ys) = f x y : zip xs ys
zip f _ _ = error "zip: uneven lenghts"
但是引发运行时错误只是稍微好一点。我们需要的是,在编译时强制要求列表的长度相同。
data Z -- zero
data S n -- successor
-- the type S (S (S Z)) is used to represent the number 3 at the type level
-- List n a is a list of a having exactly length n
data List n a where
Nil :: List Z a
Cons :: a -> List n a -> List (S n) a
-- The two arguments of zip are required to have the same length n.
-- The result is long n elements as well.
zip' :: (Int -> Int -> Int) -> List n Int -> List n Int -> List n Int
zip' f Nil Nil = Nil
zip' f (Cons x xs) (Cons y ys) = Cons (f x y) (zip' f xs ys)
请注意,编译器能够推断出这一点,并且具有相同的长度,因此递归调用在静态上是良好的类型。xs
ys
在Java中,您可以使用相同的技巧对类型中的列表长度进行编码:
class Z {}
class S<N> {}
class List<N,A> { ... }
static <A> List<Z,A> nil() {...}
static <A,N> List<S<N>,A> cons(A x, List<N,A> list) {...}
static <N,A> List<N,A> zip(List<N,A> list1, List<N,A> list2) {
...
}
但是,据我所知,代码无法访问两个列表的尾部,并将它们用作相同类型的两个变量,其中直观地 。直观地说,访问两个尾巴会丢失类型信息,因为我们不再知道它们的长度是偶数。要执行递归调用,需要强制转换。zip
List<M,A>
M
N-1
当然,可以以不同的方式重写代码并使用更传统的方法,例如使用迭代器。诚然,上面我只是试图以直接的方式在Java中转换Haskell函数,这是编写Java的错误方法(就像通过直接翻译Java代码来编码Haskell一样)。尽管如此,我还是用这个愚蠢的例子来展示Haskell GADT如何在没有不安全的强制转换的情况下表达一些需要在Java中强制转换的代码。list1