类型构造函数可以被视为函数式编程语言中的类型吗？

Question

我正在接近Haskell编程语言,我有Scala和Java开发人员的背景.

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

那么类型构造函数也是类型吗？

Answer 1

嗯,类型和类型构造函数有自己的微积分,它们各有各种.如果您使用:k (Maybe Int)的ghci,例如,你会得到*,现在这是一个正确的类型和它(通常)的居民.在这种情况下Nothing,Just 42等等*现在具有更具描述性的别名Type.

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

Answer 2

让我们看一个类比:函数.在数学的某些分支中,函数被称为值构造函数,因为这就是它们的作用:将一个或多个值放入其中,并从中构造一个新值.

类型构造函数完全相同,除了类型级别:您放入一个或多个类型,并且它们构造一个新类型.在某种意义上,它们是类型级别的函数.

现在,按照我们的比喻:你问的问题的类比是什么？嗯,就是这样:"可以将值构造函数(即函数)视为函数式编程语言中的值吗？"

答案是:它取决于编程语言.现在,对于函数式编程语言,几乎所有(如果不是全部)它们的答案都是"是".这取决于您对"函数式编程语言"的定义.有些人将函数式编程语言定义为具有值函数的编程语言,因此根据定义,答案将简单地为"是".但是,有些人将函数式编程语言定义为不允许副作用的编程语言,而在这种语言中,函数不一定是值.

最着名的例子可能是约翰巴克斯的FP,来自他的开创性论文Can Programming From the von Neumann Style？- 功能风格及其程序代数.在FP中,存在"类似功能"事物的层次结构.函数只能处理值,函数本身不是值.但是,有一个"功能"的概念是"函数构造函数",即它们可以将函数(以及值)作为输入和/或生成函数作为输出,但它们不能将函数作为输入和/或将它们生成为输出.

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

注意:作为值的函数也称为"第一类函数",将函数作为输入或将它们作为输出返回的函数称为"高阶函数".

如果我们看一些类型:

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

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

同样,这同样适用于类型构造函数,因为它们在类型级别上实际上是相同的.在某些语言中,类型构造函数可以是类型,有些则不能.例如,在Java和C♯中,类型构造函数不是类型.例如,你不能拥有List<List>C♯.你可以在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是一个类型构造函数,它采用一种类型并生成一个类型,?(函数类型构造函数)采用两种类型并返回一个类型(假设只有一元函数,例如使用currying或传递元组),并且Functor是一个类型构造函数,它本身采用类型构造函数并返回一个类型.

这些"类型 - 类型"被称为种类.与函数一样,带箭头的任何东西都是一个类型构造函数,任何带有多个箭头的东西都是一个更高级的类型构造函数.

和函数一样,某些语言允许使用更高级的类型构造函数,而某些语言则不允许.这两种语言在你的问题,斯卡拉和Haskell提做,但如上所述,Java和C♯没有.

但是,当我们查看您的问题时,会出现问题:

那么类型构造函数也是类型吗？

不是,不是.至少不是我所知道的任何语言.请参阅,虽然您可以使用类型构造函数作为输入的高级类型构造函数和/或将它们作为输出返回,但您不能拥有表达式或值或变量或具有类型构造函数作为其类型的参数.你不能拥有一个带List或返回的函数List.你不能有一个类型的变量Monad.但是,你可以有一个类型的变量Int.

所以,显然,类型和类型构造函数之间存在差异.