Haskell-非法多态类型? [英] Haskell - Illegal Polymorphic type?

问题描述

为什么会编译这种类型的单一用法，但是将其放入列表会失败?

Why does the single usage of this type compile, but putting it into a list fails?

ft1  :: (Foldable t, Num a) => t a -> a
ft1   =   (F.foldl (+)  0)

fTest :: [(Foldable t, Num a) => t a -> a ]
fTest = [ F.foldl (+)  0 ]

后者给出了错误:

folding.hs:80:10:
    Illegal polymorphic or qualified type:
      (Foldable t, Num a) => t a -> a
    Perhaps you intended to use ImpredicativeTypes
    In the type signature for `fTest':
      fTest :: [(Foldable t, Num a) => t a -> a]

相似地，尝试命名它失败(不同):

Simliarly, trying to name it fails (differently):

type Ftst t a = (Foldable t, Num a) => t a -> a

folding.hs:80:1:
    Illegal polymorphic or qualified type:
      (Foldable t, Num a) => t a -> a
    Perhaps you intended to use RankNTypes or Rank2Types
    In the type declaration for `Ftst'

推荐答案

对Haskell的类型系统进行此限制是为了简化类型推断和检查.使用谓词等级1类型(见下文)的类型推断是可以确定的，并且具有相对简单的实现.等级2类型的类型推断是可以决定的，但相当复杂，以至于我不知道任何使用等级2类型推断的语言.对于等级3及更高级别的类型，类型推断是无法确定的.强制性类型也使事情复杂化.GHC曾经有一个实现，它允许使用强制性类型进行类型检查(以及一些非常有限的推断)，但是它是如此复杂，以至于后来被淘汰了.(目前，GHC仍接受某些仅使用强制性类型进行类型检查的值，但我认为这不被视为稳定"功能.)

This restriction on Haskell's type system is in place to simplify type inference and checking. Type inference with predicative rank-1 types (see below) is decidable and has a relatively simple implementation. Type inference with rank-2 types is decidable but quite complicated, to the point that I don't know any language with an implementation of rank-2 type inference. Type inference for types of rank 3 and above is flat-out undecidable. Impredicative types also complicate things considerably; GHC used to have an implementation which allowed type-checking (and some very limited inference) with impredicative types, but it was so complicated that it was ripped out later. (Some values which only typecheck with impredicative types are still accepted by GHC at the moment, but I think this is not considered a "stable" feature.)

快速定义:等级1类型具有所有的量化和类约束，因此所有等级1类型都具有以下形式

Quick definitions: rank-1 types have all quantification and class constraints "outside" the type, so all rank-1 types are of the form

forall a_1 ... a_m. (C_1, ..., C_n) => t

Rank-2类型允许函数参数具有rank-1类型.一般而言，n级类型允许函数参数具有(n-1)级类型.

Rank-2 types allow function arguments to have rank-1 types; and in general rank n types allow function arguments to have rank (n-1) types.

谓语性回答了可以用什么类型代替类型变量的问题.如果只能替换单态类型(尽管可能使用类型变量！)，则您处于谓词系统中；否则，您将处于谓词系统中.强制性类型使您可以将多态类型替换为类型变量.通过扩展，谓词系统中的参数数据类型只能接受单态类型作为参数.因此，例如，您的示例将 [] 类型的构造函数应用于类型为 forall的类型.(可折叠的t，数字a)＝>t a->试图将构造函数应用于多态类型，因此仅在强制性系统中有效.

Predicativity answers the question of what types can be substituted for type variables. If only monomorphic types (though potentially with type variables!) can be substituted, you are in a predicative system; impredicative types allow you to substitute a polymorphic type for a type variable. By extension, parametric data types in predicative systems can only accept monomorphic types as arguments. Thus, for example, your example which applies the [] type constructor to the type forall t a. (Foldable t, Num a) => t a -> a is trying to apply a constructor to a polymorphic type, hence is only valid in an impredicative system.

这篇关于Haskell-非法多态类型?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！