【问题标题】:What does it mean that the semantics (of Haskell) are affected by the inferred types (of return type polymorphism)?(Haskell 的)语义受到(返回类型多态的)推断类型的影响是什么意思?
【发布时间】:2014-06-10 13:35:05
【问题描述】:

Here the commentator writes:

最后,只要有足够的宏魔法,就可以做到这一点……但现在可能比在 Clojure 上实现 Haskell 风格的类型系统更省力。类型化的 Clojure 可能是一个很好的模型,除非它被显式设计,因此 Clojure 的语义不会受到推断类型的影响。这正是返回类型多态中发生的情况,因此在 Typed Clojure 中显然是不可能的。

我的问题是 - 语义(Haskell)受到推断类型(返回类型多态性)的影响是什么意思?

【问题讨论】:

  • 如果语义不受影响,那么即使没有类型检查器/推理器,类型正确的程序也可以运行。由于情况并非如此,如果不指定类型以及 Haskell(语言)如何知道类型,您实际上无法判断 Haskell 程序会做什么。尽管通常它们都是相同的机制,并且要么是推理器,要么是句法注释。

标签: haskell types clojure polymorphism clojure-core.typed


【解决方案1】:

考虑read 函数,它具有(ad-hoc)多态返回值:

read :: (Read a) => String -> a

实施并不那么重要。唯一重要的部分是实现依赖于在编译时选择的Read 的实例,并且推断可能会导致为对read 的相同调用选择不同的类型。

addFive :: Int -> Int
addFive x = x + 5

main :: IO ()
main = do
    print (addFive (read "11"))
    putStrLn (read "11")

使用相同的参数两次调用read。 Haskell 需要引用透明性,所以它必须两次产生相同的结果,对吧?嗯,不完全是。推断的返回类型很重要。在print 行中,推断的返回类型是Int。在putStrLn 行中,推断的返回类型是String。而且因为它是 ad-hoc 多态的,所以语义会随着类型变量的变化而变化。

print 行将打印出 16。putStrLn 行将崩溃,因为"11" 不是read 将成功解码为String 的输入。

因为类型变量只出现在返回类型中,所以在调用函数时没有该类型的值。没有办法在运行时调度值的类型来确定要使用的 Read 的哪个实例。弄清楚它的唯一方法是在编译时知道类型。所以 Typed Clojure 不能这样做——这意味着语义依赖于编译时类型。

编辑地址评论

我不知道它是否应该给你留下深刻印象。但是由于您的陈述(2)在所有可能的方面都是错误的,这表明即使理解这个例子也明显缺乏基础。我想我必须一直回到 Haskell 中类型变量 的含义 来解释这一点。

Haskell 中的类型变量表示由调用者选择的未知但具体的类型。 Read a => String -> a 类型并不意味着函数根据其输入为其返回值选择一个类型。这意味着该函数根据它输出的类型选择它的工作方式。

也许read 是一个不好的例子,因为它的不同行为只有在由于输入错误而引发异常时才会显得特别不同。对于没有使用 Haskell 类型系统经验的人来说,很容易将其与运行时强制转换异常之类的东西混为一谈,即使它完全不同。

你的说法(2)是完全错误的。该程序不会崩溃,因为read 返回一个Int,其中代码预期为String,并且发生了类似ClassCastException 的情况。程序崩溃是因为read 在编译时根据其返回类型选择了一个解析器来解析String 文字,但给出的输入不是有效的String 文字。 (相比之下,"\"11\"" 是有效的 String 文字,因为它被引用了。)

粗体部分是重要部分。 read 函数根据返回类型选择在编译时要使用的解析器。这既是一种非常强大的技术,也是 Typed Clojure 无法做到的。

【讨论】:

  • 在这里帮帮我。您是说(1)打印行使读取函数返回整数(2)第二个读取行也将返回一个整数(3)这将在运行时崩溃而不是编译时(4)这不会发生在 Clojure core.typed 中。嗯,原谅我,我应该对此印象深刻吗?有什么我想念的吗?
  • @hawkeye 你误解得很彻底。我怀疑这是因为对 Haskell 中的多态性的含义存在一些基本的误解。我已添加到答案中以填写其中一些详细信息。
  • @hawkeye (1) addFive 的类型意味着 read 返回一个 Int,并且 (2) 它是 putStrLn 的类型使得 read 返回一个字符串,不是 int。 read "11" 必须是字符串,但 11 不是有效字符串 - 字符串必须包含在 "s 中 - 您需要 read "\"11\"" - 包含要读取的字符串的字符串。 (3) read 的变体将结果包装在 Maybe 中(这样您就不会在运行时崩溃),这更适合现实生活中使用 - 这只是一个玩具示例,表明完全不同的 @根据需要的返回类型使用 987654359@。
  • @hawkeye 您不应该对崩溃印象深刻,您应该了解read 的语义取决于从上下文确定的推断类型(在编译时,而不是运行时)。 read 是(返回类型)多态的,因此read "11" 的不同推断类型(第一种情况下的Int 和第二种情况下的String)导致使用不同的语义,在一种情况下返回11::Int并在第二种情况下拒绝无效的字符串11。
  • 值得强调的是read 不是一个函数,它是一个相关函数家族!但是,read :: String -> Int 是一个字面量函数
【解决方案2】:

查看这种区别的一种方法是检查 System F。它与 Haskell 非常相似,只是所有多态性都是使用“type lambdas”显式引入的。典型的符号是类型 lambda 在类型声明中显示为“forall”量化(我将写为 \/),在值中显示为“big lambdas”(我将写为 /\)。

因此,例如,id 变为

id :: \/ a . a -> a
id = /\ type -> \x -> x

所以我们必须显式传递实例化变量a 的类型才能使用id。您可能会看到它被用作

> id Int 3
3 :: Int

那么,这与返回类型多态性有什么关系?嗯,Haskell 的类型推断器(Hindley-Milner)系统可以被认为本质上生活在 System F 之上,自动围绕类型进行管道传输。为此,它限制了 System F 的很多灵活性,但我们暂时忽略它。

您必须记住的是,类型推断器会在运行时之前确定类型变量应该被实例化为什么。或者,更清楚地说,在运行时所有类型的 lambdas 都被消除了。这就是允许编译时/运行时阶段区分的原因,也是允许类型擦除的原因。


Haskell 扩展了 Hindley-Milner 以允许一种有界多态性。类型

\/ a . C a => a

表示 lambda 类型只能由以C 为界的类型来实现。 Haskell 然后求解关于这些边界的方程以确定插入到任何位置的正确类型。

这就是我们得到返回类型多态性的地方。当我们推断必须传递给特定类型 lambda 的类型时,我们使用有关函数输入和输出的信息

f :: a -> b
e :: a

f e :: b

如果函数的返回类型可以约束类型变量,那么它会。这将使推理器选择正确的 System F 变体。然后,在运行时,所有的 lambda 类型都消失了,只剩下与所需返回类型匹配的确切的、无类型的代码。

【讨论】:

  • 只是为了澄清 - 正如我在系统 F 中所理解的那样 - 有类型 lambdas 和 value lambdas。类型 lambdas 在编译时运行(并且在运行时之前被消除)并且在运行时值 lambdas 运行。那是对的吗?如果是这样 - 我们可以考虑类似于 lambda 类型的宏的编译时部分吗?
  • 宏可以实现它们(它们可以控制阶段),但只有当宏实际上是在对类型系统进行编程时,它们才会真正确实实现它们。我想这就是 Typed Clojure 的运作方式。
猜你喜欢
  • 2020-07-03
  • 1970-01-01
  • 1970-01-01
  • 2018-11-05
  • 2017-12-03
  • 2015-01-03
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
相关资源
最近更新 更多