【问题标题】:What is a higher kinded type in Scala?Scala 中的高级类型是什么?
【发布时间】:2011-09-08 22:57:55
【问题描述】:

您可以在网上找到以下内容:

  1. 高级类型 == 类型构造函数?

    class AClass[T]{...} // For example, class List[T]
    

    有人说这是一种高级类型,因为它 对符合定义的类型进行抽象。

    高级类型是接受其他类型并构造新类型的类型

    这些虽然也称为类型构造函数。 (例如,Programming in Scala)。

  2. 高级类型 == 类型构造函数,它以类型构造函数作为类型参数?

    在论文Generics of a Higher Kind,你可以阅读

    ... 抽象于类型之上的类型 抽象于类型之上的类型 ('高级类型') ..."

    这表明

    class XClass[M[T]]{...} // or
    
    trait YTrait[N[_]]{...} // e.g. trait Functor[F[_]]
    

    是更高种类的类型。

因此,考虑到这一点,很难区分类型构造函数更高种类的类型以类型构造函数为类型参数的类型构造函数 em>,因此上面的问题。

【问题讨论】:

  • 添加了 Landei 的 Functor 作为示例。

标签: scala generics types higher-kinded-types type-constructor


【解决方案1】:

让我通过一些消歧来弥补开始的一些混乱。我喜欢用价值水平的类比来解释这一点,因为人们往往更熟悉它。

类型构造函数是一种可以应用于类型参数以“构造”类型的类型。

值构造函数是可以应用于值参数以“构造”值的值。

值构造函数通常称为“函数”或“方法”。这些“构造函数”也被称为“多态”(因为它们可用于构造不同“形状”的“东西”)或“抽象”(因为它们抽象出不同多态实例之间的差异)。

在抽象/多态的上下文中,一阶是指抽象的“一次性使用”:您对一个类型进行一次抽象,但该类型本身不能对任何东西进行抽象。 Java 5 泛型是一阶的。

上述抽象特征的一阶解释是:

类型构造函数是一种类型,您可以将其应用于正确的类型参数以“构造”正确的类型。

值构造函数是一个值,您可以将其应用于正确的值参数以“构造”正确的值。

为了强调不涉及抽象(我猜你可以称之为“零阶”,但我没有看到它在任何地方使用过),例如值1或类型String,我们通常会说一些是一个“正确的”值或类型。

正确的值是“立即可用的”,因为它不等待参数(它不抽象它们)。将它们视为您可以轻松打印/检查的值(序列化函数是作弊!)。

正确的类型是对值进行分类的类型(包括值构造函数),类型构造函数不会对任何值进行分类(它们首先需要应用于正确的类型参数以产生正确的类型)。要实例化一个类型,有必要(但不充分)它是一个正确的类型。 (它可能是一个抽象类,或者您无权访问的类。)

“高阶”只是一个通用术语,表示重复使用多态性/抽象。对于多态类型和值来说,这意味着同样的事情。具体来说,高阶抽象抽象了一些抽象的东西。对于类型,术语“higher-kinded”是更一般的“higher-order”的特殊用途版本。

因此,我们表征的高阶版本变为:

类型构造函数是一种可以应用于类型参数(正确类型或类型构造函数)以“构造”正确类型(构造函数)的类型。

值构造函数是可以应用于值参数(正确值或值构造函数)以“构造”正确值(构造函数)的值。

因此,“高阶”仅仅意味着当您说“对 X 进行抽象”时,您是认真的!被抽象出来的X 并没有失去它自己的“抽象权”:它可以抽象它想要的一切。 (顺便说一下,我在这里使用动词“抽象”来表示:省略对值或类型的定义不重要的东西,以便抽象的用户可以改变/提供它作为参数.)

以下是一些正确、一阶和高阶值和类型的示例(灵感来自 Lutz 通过电子邮件提出的问题):

                   proper    first-order           higher-order

values             10        (x: Int) => x         (f: (Int => Int)) => f(10)
types (classes)    String    List                  Functor
types              String    ({type λ[x] = x})#λ   ({type λ[F[x]] = F[String]})#λ

使用的类被定义为:

class String
class List[T]
class Functor[F[_]]

为了避免通过定义类的间接性,您需要以某种方式表达匿名类型函数,这些函数在 Scala 中无法直接表达,但是您可以使用结构类型而没有太多的语法开销( 样式是由于 @ 987654321@afaik):

在一些支持匿名类型函数的假设未来版本的 Scala 中,您可以将示例中的最后一行缩短为:

types (informally) String    [x] => x              [F[x]] => F[String]) // I repeat, this is not valid Scala, and might never be

(就个人而言,我很遗憾曾经谈论过“高级类型”,它们毕竟只是类型!当您绝对需要消除歧义时,我建议说诸如“类型构造函数参数”,“类型构造函数成员”或“类型构造函数别名”,以强调您不是在谈论正确的类型。)

ps:更复杂的是,“多态”在另一种意义上是模棱两可的,因为多态类型有时意味着一个普遍量化的类型,例如Forall T, T => T,这是一个正确的类型,因为它对多态值进行分类(在Scala,这个值可以写成结构类型{def apply[T](x: T): T = x})

【讨论】:

【解决方案2】:

(此答案试图通过一些图形和历史信息来装饰 Adriaan Moors 的答案。)

自 2.5 以来,高级类型是 Scala 的一部分。

  • 在 Scala 之前,就像 Java 一样,直到现在, 不允许使用类型构造函数 (Java 中的“泛型”)用作 类型构造函数的类型参数。例如

     trait Monad [M[_]]
    

    不可能。

    在 Scala 2.5 中,类型系统通过分类能力得到了扩展 更高级别的类型(称为类型构造函数多态)。这些 分类称为种类。

    (图片来源于Generics of a Higher Kind

    结果是,可以使用类型构造函数(例如List) 就像类型构造函数的类型参数位置中的其他类型一样 自 Scala 2.5 以来,它们成为一流的类型。 (类似于 Scala 中的一等值函数)。

    在支持更高种类的类型系统的上下文中,我们可以 区分正确类型IntList[Int] 等类型与List 等一阶类型和更高类型的类型(如FunctorMonad) (对类型进行抽象的类型对类型进行抽象)。

    Java 的类型系统不支持种类,因此没有类型 属于“高级”。

    所以这必须在支持类型系统的背景下才能看到。

  • 在 Scala 中,您经常会看到类型构造函数的示例,例如

     trait Iterable[A, Container[_]]
    

    标题为“高级类型”,例如在Scala for generic programmers, section 4.3

    这有时会产生误导,因为许多人将Container 称为更高种类的类型 而不是Iterable,但更准确的是,

    这里使用Container作为更高种类(高阶)类型的类型构造函数参数Iterable

【讨论】:

    【解决方案3】:

    IntChar 等普通类型的kind 的实例是值,是*。像Maybe 这样的一元类型构造函数是* -> *;像Either 这样的二进制类型构造函数有(curried) 种类* -> * -> *,等等。您可以将MaybeEither 等类型视为类型级函数:它们采用一种或多种类型,并返回一个类型。

    一个函数是 higher-order 如果它的 order 大于 1,其中 order 是(非正式地)函数箭头向左的嵌套深度:

    • 订单 0:1 :: Int
    • 订单1:chr :: Int -> Char
    • 订单 2:fix :: (a -> a) -> amap :: (a -> b) -> [a] -> [b]
    • 订单 3:((A -> B) -> C) -> D
    • 订单 4:(((A -> B) -> C) -> D) -> E

    所以,长话短说,higher-kinded 类型只是一个类型级别的高阶函数,它抽象 类型构造函数:

    • 订单 0:Int :: *
    • 订单 1:Maybe :: * -> *
    • 顺序 2:Functor :: (* -> *) -> Constraint—higher-kinded:将一元类型构造函数转换为类型类约束

    【讨论】:

    • 好的,我明白了,那么在 Scala 中,( * ⇒ * ) ⇒ * 和 ( * ⇒ * ) ⇒ ( * ⇒ * ) 的例子是什么? Landei 函子属于第一类还是第二类?
    • @lutz:它属于第一类:Functor 从类型构造函数 F 生成正确的类型(好吧,特征,但相同的想法)Functor[F[_]]
    • @Jon:非常有见地的帖子,谢谢。类型转换器(* => *) => (* => *)可以用Scala表示吗?如果没有,用任何其他语言?
    • @JonPurdy * ⇒ * ⇒ * 与柯里化的比较非常有帮助。谢谢!
    • (* ⇒ *) ⇒ (* ⇒ *) 也可以拼写为(* ⇒ *) ⇒ * ⇒ *。它可以用 Scala 表示,如Foo[F[_], T]。这种类型(在 Haskell 中)newtype Twice f a = Twice (f (f a))(例如,Twice Maybe IntMaybe (Maybe Int)Twice [] Char[[Char]])或更有趣的类型,例如免费的 monad data Free f a = Pure a | Free (f (Free f a))
    【解决方案4】:

    我想说:一个更高种类的类型抽象一个类型构造函数。例如。考虑

    trait Functor [F[_]] {
       def map[A,B] (fn: A=>B)(fa: F[A]): F[B]
    }
    

    这里的Functor 是一个“更高种类的类型”(如"Generics of a Higher Kind" paper 中使用的那样)。它不是像 List 那样的具体(“一阶”)类型构造函数(仅抽象出适当的类型)。它抽象了所有一元(“一阶”)类型构造函数(用F[_] 表示)。

    或者换一种说法:在 Java 中,我们有明确的类型构造函数(例如 List<T>),但是我们没有“更高种类的类型”,因为我们不能对它们进行抽象(例如我们不能写上面定义的Functor接口——至少不是directly)。

    术语“高阶(类型构造器)多态性”用于描述支持“更高种类的类型”的系统。

    【讨论】:

    • 这是我的想法,但这似乎与 Jon 的回答相矛盾,其中“具体类型构造函数”已经是“更高种类的类型”。
    • 是的。根据乔恩的回答(据我所知)Java 中的List<T> 将是一元类型构造函数,因为它显然具有* -> * 类型。 Jon 的回答中缺少的是,您必须能够抽象出“整个事物”(而不仅仅是 Java 中的第二个 *)才能将其称为更高种类的类型。
    • @Landai:第 4.3 节中的论文Scala for generic programmers 建议特征 Iterable[A, Container[_]] 是一种更高种类的类型(尽管不清楚是指 Iterator 还是 Container)另一方面vero690 在第 2.3.1 节中使用术语 higher-kinded type constructor 来表示 ( * -> * ) -> * (类型运算符参数化为高阶类型构造函数) 看起来类似于 Iterator 或您的 Functor 特征。
    • 这可能是正确的,但我认为我们开始在这里分裂头发。关于高阶类型的重要一点是,不仅涉及类型构造函数(一种类型构造函数多态性),而且我们能够抽象出该类型构造函数的具体类型(高阶类型构造函数多态性)。我们能够不受限制地抽象出我们想要的任何东西(关于类型和类型构造函数),这使得命名该功能的所有可能版本变得不那么有趣了。它伤害了我的大脑。
    • 一般来说,在这里区分定义和引用很重要。 def succ(x: Int) = x+1 的定义引入了“值构造函数”(关于我的意思,请参阅我的其他答案)succ(没有人会将此值称为 succ(x: Int))。以此类推,Functor 是您的答案中定义的(实际上是更高种类的)类型。同样,您不应该将其称为Functor[F[_]]F 是什么?_ 是什么?它们不在范围内!不幸的是,存在主义的语法糖通过使F[_] 变短而使这里的水域变得混乱对于F[T forSome {type T}])
    【解决方案5】:

    Scala REPL 提供了:kind 命令

    scala> :help kind
    
    :kind [-v] <type>
    Displays the kind of a given type.
    

    例如,

    scala> trait Foo[A]
    trait Foo
    
    scala> trait Bar[F[_]]
    trait Bar
    
    scala> :kind -v Foo
    Foo's kind is F[A]
    * -> *
    This is a type constructor: a 1st-order-kinded type.
    
    scala> :kind -v Foo[Int]
    Foo[Int]'s kind is A
    *
    This is a proper type.
    
    scala> :kind -v Bar
    Bar's kind is X[F[A]]
    (* -> *) -> *
    This is a type constructor that takes type constructor(s): a higher-kinded type.
    
    scala> :kind -v Bar[Foo]
    Bar[Foo]'s kind is A
    *
    This is a proper type.
    

    :help 提供了清晰的定义,因此我认为值得将其完整发布在这里 (Scala 2.13.2)

    scala> :help kind
    
    :kind [-v] <type>
    Displays the kind of a given type.
    
        -v      Displays verbose info.
    
    "Kind" is a word used to classify types and type constructors
    according to their level of abstractness.
    
    Concrete, fully specified types such as `Int` and `Option[Int]`
    are called "proper types" and denoted as `A` using Scala
    notation, or with the `*` symbol.
    
        scala> :kind Option[Int]
        Option[Int]'s kind is A
    
    In the above, `Option` is an example of a first-order type
    constructor, which is denoted as `F[A]` using Scala notation, or
    * -> * using the star notation. `:kind` also includes variance
    information in its output, so if we ask for the kind of `Option`,
    we actually see `F[+A]`:
    
        scala> :k -v Option
        Option's kind is F[+A]
        * -(+)-> *
        This is a type constructor: a 1st-order-kinded type.
    
    When you have more complicated types, `:kind` can be used to find
    out what you need to pass in.
    
        scala> trait ~>[-F1[_], +F2[_]] {}
        scala> :kind ~>
        ~>'s kind is X[-F1[A1],+F2[A2]]
    
    This shows that `~>` accepts something of `F[A]` kind, such as
    `List` or `Vector`. It's an example of a type constructor that
    abstracts over type constructors, also known as a higher-order
    type constructor or a higher-kinded type.
    

    【讨论】:

      猜你喜欢
      • 2013-02-24
      • 1970-01-01
      • 1970-01-01
      • 2017-09-12
      • 2015-03-08
      • 2023-03-30
      • 2013-09-15
      • 1970-01-01
      • 1970-01-01
      相关资源
      最近更新 更多