haskell - 类型别名混淆的 RankNTypes

标签 haskell types functional-programming higher-rank-types

<分区>

我正在尝试了解类型约束如何与类型别名一起使用。首先,假设我有下一个类型别名:

type NumList a = Num a => [a]

我有下一个功能:

addFirst :: a -> NumList a -> NumList
addFirst x (y:_) = x + y

此函数失败并出现下一个错误:

Type.hs:9:13: error:
    • No instance for (Num a) arising from a pattern
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            addFirst :: a -> NumList a -> a
    • In the pattern: y : _
      In an equation for ‘addFirst’: ad

这是显而易见的。此问题已在此处描述:

Understanding a rank 2 type alias with a class constraint

而且我理解为什么我们需要 {-# LANGUAGE RankNTypes #-} 来使此类类型别名起作用,以及为什么前面的示例不起作用。但我不明白的是为什么下一个示例可以正常编译(在 ghc 8 上):

prepend :: a -> NumList a -> NumList a
prepend = (:)

当然,如果我尝试传递错误的值,它会在 ghci 中失败:

λ: prepend 1 []
[1]
λ: prepend "xx" []

<interactive>:3:1: error:
    • No instance for (Num [Char]) arising from a use of ‘prepend’
    • When instantiating ‘it’, initially inferred to have
      this overly-general type:
        NumList [Char]
      NB: This instantiation can be caused by the monomorphism restriction.

似乎类型类型检查在运行时延迟了:(

此外,一些简单且看似相同的代码无法编译:

first :: NumList a -> a
first = head

并产生下一个错误:

Type.hs:12:9: error:
    • No instance for (Num a)
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            first :: NumList a -> a
    • In the expression: head
      In an equation for ‘first’: first = head

有人能解释一下这是怎么回事吗?我希望在函数类型检查与否方面保持一致。

最佳答案

Seems like type type checking delayed at runtime :(

不是真的。这里可能有点令人惊讶,因为您在加载文件后 在 ghci 中遇到了类型错误。然而,可以这样解释:文件本身非常好,但这并不意味着所有您可以使用其中定义的函数构建的表达式都是类型正确的。

高阶多态性与它无关。例如,(+) 是在前奏中定义的,但如果您尝试在 ghci 中计算 2 + "argh",您也会遇到类型错误:

No instance for (Num [Char]) arising from a use of ‘+’
In the expression: 2 + "argh"
In an equation for ‘it’: it = 2 + "argh"

现在,让我们看看首先的问题是什么:它声称给定一个NumList a,它可以产生一个a,不问的问题。但是我们知道如何凭空构建NumList a!事实上,Num a 约束意味着 0 是一个 a 并使 [0] 成为完全有效的 NumList a.这意味着如果 first 被接受,那么所有类型将被居住:

first :: NumList a -> a
first = head

elt :: a
elt = first [0]

特别是Void会太:

argh :: Void
argh = elt

确实啊!

关于haskell - 类型别名混淆的 RankNTypes,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/40252867/

相关文章:

scala - Mixin 类型约束仍然可以编译

haskell - 使用 `a0' 引起的模糊类型变量 `it'

algorithm - 什么是尾递归?

haskell - 使用foldl with++ 时约束错误中的非类型变量参数

c++ - 确定传递给模板函数的变量类型

haskell - 在没有 `Conkin.Traversable` 的情况下将值更改为 `unsafeCoerce` 中的索引

delphi - 如何在 Delphi 中声明自定义类型?

r - 如何从函数内生成条件图

haskell - 返回该宽度和高度的网格中每个可能坐标的列表

Haskell:GHCi 将 Ctrl-Y 视为 Ctrl-Z