在Haskell中，“更高级的类型” *真的*类型？或者他们只是表示*具体*类型的集合，而不是更多？ [英] In Haskell, are "higher-kinded types" *really* types? Or do they merely denote collections of *concrete* types and nothing more?

问题描述

Paramametrically多态函数

考虑以下函数：

  f :: a  - > Int 
fx =（1 :: Int）
  

我们可以说< c $ c> f 是 a - > Int ，因此 f 是一个更高金额类型。

以下哪一种是最准确的方法来考虑 f ？

1. 实际上 f 类型 a - > INT 。但是，它可以用作 f :: Int - > Int ，作为 f :: Double - >



2. 从字面上看， f 不是 a - > INT 。事实上，这只是一种简短的说法，表示存在一个 的 的 c $ c> f :: Int - > Int ， f :: Double - > Double 等等;而且，每个）
   

高价类型

同样，我们可以考虑下面的类型声明：

  data也许a =只是|没有什么
  

然后问两个视图中的哪一个更正确：

1. 没有单类型可能;的确，只有一个具体类型的家族（ Maybe Int ， Maybe String 等），仅此而已。 / p>




2. 事实上 单个类型也许。这种类型是较高的类型。当我们说它是一个类型时，我们的意思是（不是（1）的简写）。恰巧我们也可以写 Maybe Int ， Maybe Double 等等来生成 distinct 类型（恰好是具体的）。但是，在一天结束时（即）：可能，可能是Int 和也许String 表示三个不同的类型，其中两个是具体的，其中一个是更高级的。

>



问题摘要





在Haskell中，更高级的类型真的是类型吗？或者只有具体类型是真实类型，当我们谈到更高类型时，我们只是表示一个具体类型的家庭。而且，paramametrically多态函数表示单一类型的功能，或者仅表示具体类型的集合函数

解决方案

这并不完全清楚您想问什么，以及实际的区别是什么？ 1和2在这两种情况下，但从基本的数学角度来看：





f 实际上有类型 f :: forall aa-> int





对于基于Haskell的类型化lambda演算函数来说，这是一个完全合法的类型。它可以是这样的：



  f =λa：Type.λx：a。（body for f）
  

您如何获得 Double-> Int ？您 将它应用于 Double 类型：



  f Double =（λa：Type.λx：a。（body for f））Double => λx：Double。（body for f | a = Double）
  

Haskell执行两个操作（类型抽象和尽管可以在类型签名中用 XExplicitForAll GHC扩展明确指出 forall 部分，并使用类型签名显式地创建 Double-> Int f 的实例：

  f_double :: Double  - > Int 
 f_double = f 
  

更高固定类型





考虑一个简单的类型：



  data示例= IntVal Int | NoVal 
  

（是，它是也许是Int ）。



也许是一个类型构造函数，就像 IntVal 是一个 data 构造函数。这是完全一样的，只有'高一级'，在 Maybe 被应用于 Type 的意义上，很像 IntVal 应用于 Int 。





lambda微积分，也许有类型：



 可能：Type->类型
  

Haskell不允许您从类型构造函数中获取类型，但可以让您获得 （这只是类型的类型的一个奇特名称）：



 ：k也许
也许:: *  - > * 
  

不，也许不是 type ：您不能拥有类型为 Maybe 的对象。 可能是（几乎）从类型到类型的函数，如 IntVal 是从值到值的函数。 p>



我们将 Maybe 应用于 String 的结果称为 Maybe String ，就像我们将 IntVal 应用于 4 as IntVal 4 。




Paramametrically polymorphic functions

Consider the following function:

f :: a -> Int
f x = (1 :: Int)

We might say that the type of f is a -> Int, and that f therefore is of a "higher-kinded" type.

Which of the following is the most accurate way to think about f?

1. There is in fact a single f of type a -> Int. It can be used, however, as an f :: Int -> Int, as an f :: Double -> Int, and so forth.

2. Literally speaking, the type of f is NOT a -> Int. Indeed, that is just a shorthand way of saying that there is a family of functions f whose type is concrete (i.e., there is an f :: Int -> Int, an f :: Double -> Double, and so forth; moreover, each of these functions is distinct from each other).

Higher Kinded Types

Similarly, we can consider the following type declaration:

data Maybe a = Just a | Nothing

And ask which of the two views is more correct:

1. There is no single type Maybe; indeed, there is merely a family of concrete types (Maybe Int, Maybe String, etc) and nothing more.

2. There is in fact a single type Maybe. This type is a higher-kinded type. When we say that it is a "type" we mean it literally (not as a shorthand for (1)). It just so happens that we can also write Maybe Int, Maybe Double, and so forth to generate distinct types (which happen to be concrete). But, at the end of the day (i.e.): Maybe, Maybe Int, and Maybe String denote three distinct types, two of which are concrete and one of which is higher-kinded.

Question Summary

In Haskell, are "higher-kinded types" really types? Or are only concrete types "the real types", and when we speak of "higher-kinded types" we are merely denoting a family of concrete types. Moreover, do paramametrically polymorphic functions denote functions of a single type, or do they merely denote a collection functions of concrete types (and nothing more)?

解决方案

It's not entirely clear what you want to ask, and what is the practical difference between 1 and 2 in both cases, but from underlying math perspective:

Paramametrically Polymorphic Functions

f actually has type f :: forall a.a->int

It is a perfectly legal type for a function in typed lambda calculus, which is Haskell based on. It can be something like:

f = λa:Type.λx:a.(body for f)

How do you get Double->Int from it? You apply it to Double type:

f Double = (λa:Type.λx:a.(body for f)) Double => λx:Double.(body for f|a=Double)

Haskell does both operations (type abstraction and type application) behind the scene, although it is possible to explicitly state forall part in the type signature with XExplicitForAll GHC extension, and explicitly make a Double->Int instance of f with type signature:

f_double :: Double -> Int
f_double = f

Higher Kinded Types

Consider a simple type:

data Example = IntVal Int | NoVal

(Yes, it is Maybe Int).

Maybe is a type constructor, just like IntVal is a data constructor. It is exactly the same thing, only 'one level higher', in the sense that Maybe is applied to Type, much like IntVal is applied to Int.

In lambda calculus, Maybe has type:

Maybe : Type->Type

Haskell doesn't allow you to get a type from type constructor, but allows you to get a kind (which is just a fancy name for type of type):

:k Maybe
Maybe :: * -> *

So no, Maybe is not a type: you can't have an object with the type Maybe. Maybe is (almost) a function from types to types, like IntVal is a function from values to values.

We call the result of applying Maybe to String as Maybe String, like we call the result of applying IntVal to 4 as IntVal 4.

这篇关于在Haskell中，“更高级的类型” *真的*类型？或者他们只是表示*具体*类型的集合，而不是更多？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！