【问题标题】:Can type constructors be considered as types in functional programming languages?类型构造函数可以被视为函数式编程语言中的类型吗?
【发布时间】:2019-07-04 09:08:29
【问题描述】:

我正在学习 Haskell 编程语言,我有 Scala 和 Java 开发人员的背景。

我正在阅读类型构造函数背后的理论,但我不明白它们是否可以被视为类型。我的意思是,在 Scala 中,您使用关键字 classtrait 来定义类型构造函数。想想List[T],或Option[T]。同样在 Haskell 中,您使用相同的关键字 data,用于定义新类型。

那么,类型构造函数也是类型吗?

【问题讨论】:

    标签: scala haskell types type-theory


    【解决方案1】:

    嗯,类型和类型构造函数有它们自己的演算,它们各自都有种类。例如,如果你在ghci 中使用:k (Maybe Int),你会得到*,现在这是一个正确的类型并且它(通常)有居民。在这种情况下,NothingJust 42 等。* 现在有一个更具描述性的别名 Type

    现在您可以查看Maybe 的构造函数类型,:k Maybe 将为您提供* -> *。使用别名,这是您所期望的 Type -> Type。它需要一个Type构造一个Type。现在,如果您将类型视为一组值,那么一个很好的问题是Maybe 有哪一组值?好吧,没有,因为它不是真正的类型。你可能会尝试类似Just 的东西,但它的类型为a -> Maybe a 和类型Type,而不是Maybe 类型为Type -> Type

    【讨论】:

    • 我很好奇你为什么说Maybe a通常有居民。 Nothing 不是Maybe a 的居民,是否可以选择a
    • 我认为他的意思是一种类型(类似*)通常具有值,Void 是一个(?)例外。
    • @chepner 是对的,这就是我的意思。 Void 然而并不是唯一的例外。例如,(Void,Void) 是一个不同的类型,但也没有居民。
    【解决方案2】:

    让我们看一个类比:函数。在某些数学分支中,函数被称为值构造函数,因为它们就是这样做的:你将一个或多个值放入其中,然后它们会根据这些值构造一个新值。

    类型构造函数是完全一样的,除了在类型层面:你放入一个或多个类型,然后它们构造一个新的类型。从某种意义上说,它们是类型级别的函数。

    现在,按照我们的类比:您所问问题的类比是什么?嗯,就是这样:“值构造函数(即函数)可以被视为函数式编程语言中的值吗?”

    答案是:这取决于编程语言。现在,对于函数式编程语言,几乎所有(如果不是全部)的答案都是“是”。这取决于您对“函数式编程语言”的定义。有些人将函数式编程语言定义为将函数作为值的编程语言,因此根据定义,答案将是微不足道的“是”。但是,有些人将函数式编程语言定义为不允许副作用的编程语言,在这种语言中,函数不一定是值。

    最著名的例子可能是 John Backus 的 FP,来自他的开创性论文 Can Programming Be Liberated from the von Neumann Style? – 函数式风格及其程序代数。在 FP 中,存在“类函数”事物的层次结构。函数只能处理值,函数本身不是值。但是,有一个“函数”的概念,即“函数构造函数”,即它们可以将函数(以及值)作为输入和/或生成函数作为输出,但它们不能将函数作为输入和/或将它们生成为输出。

    因此,FP 可以说是一种函数式编程语言,但它没有函数作为值。

    注意:作为值的函数也称为“一等函数”,将函数作为输入或将函数作为输出返回的函数称为“高阶函数”。

    如果我们看一些类型:

    1   :: Int
    [1] :: List Int
    add :: Int → Int
    map :: (a → b, List a) → b
    

    你可以看到我们可以很容易地说:任何类型中带有箭头的值都是一个函数。任何类型中包含多个箭头的值都是高阶函数。

    同样,这同样适用于类型构造函数,因为除了类型级别之外,它们实际上是相同的东西。在某些语言中,类型构造函数可以是类型,而在某些语言中则不能。例如,在 Java 和 C♯ 中,类型构造函数不是类型。例如,您不能在 C♯ 中有 List<List>。您可以写下 Java 中的 List<List> 类型,但这是一种误导,因为两个 List 的含义不同:第一个 List 是类型构造函数,第二个 List原始类型,所以这实际上不是使用类型构造函数作为类型。

    与我们上面的类型示例等效的是什么?

    Int     :: Type
    List    :: Type ⇒ Type
    →       :: (Type, Type) ⇒ Type
    Functor :: (Type ⇒ Type) ⇒ Type
    

    (注意,我们怎么总是有Type?确实,我们只处理类型,所以我们通常不写Type,而是简单写*,发音为“Type”):

    Int     :: *
    List    :: * ⇒ *
    →       :: (*, *) ⇒ *
    Functor :: (* ⇒ *) ⇒ *
    

    所以,Int 是一个正确的类型,List 是一个类型构造函数,它接受一个类型并产生一个类型,(函数类型构造函数)接受两个类型并返回一个类型(假设只有一元函数,例如使用柯里化或传递元组),而Functor 是一个类型构造函数,它本身接受一个类型构造函数并返回一个类型。

    这些“类型类型”被称为种类。与函数一样,任何带有箭头的东西都是类型构造函数,而任何带有多个箭头的东西都是高级类型构造函数

    和函数一样,有些语言允许更高种类的类型构造函数,而有些则不允许。您在问题中提到的两种语言 Scala 和 Haskell ,但如上所述,Java 和 C♯ 不会。

    但是,当我们查看您的问题时,有一个复杂的问题:

    那么,类型构造函数也是类型吗?

    不是真的,不。至少不是我所知道的任何语言。看,虽然您可以拥有将类型构造函数作为输入和/或将它们作为输出返回的更高种类的类型构造函数,但您不能拥有将类型构造函数作为其类型的表达式或值或变量或参数。您不能有一个接受List 或返回List 的函数。您不能拥有Monad 类型的变量。但是,您可以拥有Int 类型的变量。

    所以,很明显,类型和类型构造函数之间是有区别的。

    【讨论】:

    • 我不同意不能让函数接受List 并返回List。类型同义词和类型族都允许您这样做。
    • Functor 是一个类型构造函数,你说,但 Functor 应该是一个 typeclass,而不是类型构造函数,不是吗?
    • 您对Functor(以及隐含的Monad)的种类不太正确。因为这些是类型类,所以它们应该有一种类型,可以为您提供Constraint(这里特别是(* -> *) -> Constraint)。
    【解决方案3】:

    至少在Haskell中,有一个层次结构,大致可以描述如下。

    术语是运行时存在的东西,例如1'a'(+) 等值。

    每个术语都有一个类型,例如IntCharInt -> Int -> Int

    每个类型都有一个kind,所有类型都有相同的kind,即*

    不过,像[] 这样的类型构造函数有类型* -> *,所以它不是类型。相反,它是从一个类型到一个类型的映射


    还有其他种类,包括(除了** -> *,每个都有一个例子):

    • * -> * -> * (Either)
    • (* -> *) -> * -> *ReaderT,monad 转换器)
    • Constraint (Num Int)
    • * -> ConstraintNum;这是一种类型类)

    【讨论】:

    • 函数是从值到值的映射,但它们仍然是值。我仍然不太清楚这种类比在哪里失效,因为类型构造函数和函数或多或少是同一件事,但由于某种原因,将值映射到值的函数本身就是一个值,但是将类型映射到类型的类型构造函数是不是类型。顺便说一句,我认为 Haskell(至少有一些扩展)也有 sorts,这是下一个级别,即种类的“类型”。
    • 我没有提到排序,因为 1) 通常 Haskell 只有一个隐式排序和 2) 我完全不熟悉让您定义其他排序的扩展。 :) 函数实际上是一种特定类型的映射,从一个 set 到另一个 set定义函数的一种方法是列出(显式或隐式)该域中的每个值映射到函数的codomain中的哪个值。
    猜你喜欢
    • 2017-12-14
    • 2020-03-13
    • 2020-08-07
    • 2018-01-24
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    相关资源
    最近更新 更多