函数不仅仅有类型：它们是类型。和种类。和排序。帮助破碎的心灵重新整合起来

发布于 2025-01-01 15:16:54 字数 1261 浏览 4 评论 0原文

我正在做我平常的“睡前阅读LYAH的一章”例行公事，感觉我的大脑随着每个代码示例而扩展。此时我确信我理解了 Haskell 的核心优势，现在只需要理解标准库和类型类，这样我就可以开始编写真正的软件了。

因此，我正在阅读有关应用函子的章节，突然这本书声称函数不仅有类型，它们是类型，并且可以被视为类型（例如，通过使它们类型类的实例）。 (->) 是一个像其他类型构造函数一样的类型构造函数。

我的心再次大吃一惊，我立即从床上跳起来，启动电脑，打开GHCi，发现了以下内容：

Prelude> :k (->)
(->) :: ?? -> ? -> *

这到底是什么意思？
如果 (->) 是类型构造函数，那么值构造函数是什么？我可以猜测，但不知道如何在传统的 data (->) ... = ... | 中定义它... | ... 格式。使用任何其他类型构造函数即可轻松完成此操作：data Either ab = Left a |对b。我怀疑我无法以这种形式表达它与极其奇怪的类型签名有关。
我刚刚偶然发现了什么？更高类型的类型具有类似 * -> 的类型签名*-> *。想想看... (->) 也出现在实物签名中！这是否意味着它不仅是一个类型构造函数，而且还是一个类构造函数？这与类型签名中的问号有关吗？

我在某处读过（希望我能再次找到它，谷歌失败了）关于能够通过从值到值的类型，到类型的种类，到种类的种类，到其他种类的东西来任意扩展类型系统，到其他的东西或其他的东西，直到永远。这是否反映在 (->) 的签名中？因为我也遇到了 Lambda 立方体的概念和构造演算，但没有花时间真正研究它们，如果我没记错的话，可以定义采用类型和返回类型、采用值和返回值的函数，采用类型和返回值，以及采用返回类型的值。

如果我必须猜测一个接受值并返回类型的函数的类型签名，我可能会这样表达：

a -> ?

或者可能

a -> *

虽然我看不到为什么第二个例子不能轻易解释的基本不可变原因作为从 a 类型的值到 * 类型的值的函数，其中 * 只是字符串或其他内容的类型同义词。

第一个例子更好地表达了一个函数，其类型超越了我心目中的类型签名：“一个函数接受类型 a 的值并返回无法表达为类型的东西。”

原文

I was doing my usual "Read a chapter of LYAH before bed" routine, feeling like my brain was expanding with every code sample. At this point I was convinced that I understood the core awesomeness of Haskell, and now just had to understand the standard libraries and type classes so that I could start writing real software.

So I was reading the chapter about applicative functors when all of a sudden the book claimed that functions don't merely have types, they are types, and can be treated as such (For example, by making them instances of type classes). (->) is a type constructor like any other.

My mind was blown yet again, and I immediately jumped out of bed, booted up the computer, went to GHCi and discovered the following:

Prelude> :k (->)
(->) :: ?? -> ? -> *

What on earth does it mean?
If (->) is a type constructor, what are the value constructors? I can take a guess, but would have no idea how define it in traditional data (->) ... = ... | ... | ... format. It's easy enough to do this with any other type constructor: data Either a b = Left a | Right b. I suspect my inability to express it in this form is related to the extremly weird type signature.
What have I just stumbled upon? Higher kinded types have kind signatures like * -> * -> *. Come to think of it... (->) appears in kind signatures too! Does this mean that not only is it a type constructor, but also a kind constructor? Is this related to the question marks in the type signature?

I have read somewhere (wish I could find it again, Google fails me) about being able to extend type systems arbitrarily by going from Values, to Types of Values, to Kinds of Types, to Sorts of Kinds, to something else of Sorts, to something else of something elses, and so on forever. Is this reflected in the kind signature for (->)? Because I've also run into the notion of the Lambda cube and the calculus of constructions without taking the time to really investigate them, and if I remember correctly it is possible to define functions that take types and return types, take values and return values, take types and return values, and take values which return types.

If I had to take a guess at the type signature for a function which takes a value and returns a type, I would probably express it like this:

a -> ?

or possibly

a -> *

Although I see no fundamental immutable reason why the second example couldn't easily be interpreted as a function from a value of type a to a value of type *, where * is just a type synonym for string or something.

The first example better expresses a function whose type transcends a type signature in my mind: "a function which takes a value of type a and returns something which cannot be expressed as a type."

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

じее 2025-01-08 15:16:54

你的问题触及了很多有趣的点，所以我
恐怕这将是一个很长的答案:)

类似 (->)

(->) 的类型是 * -> *-> *，如果我们忽略 Boxity GHC
插入。但是没有循环发生，-> 中的
(->) 的种类是种类箭头，而不是功能箭头。确实，为了
区分它们，箭头可以写成 (=>)，然后
(->) 的类型是 * =>; * => *。

我们可以将 (->) 视为类型构造函数，或者更确切地说是一种类型
操作员。类似地，(=>) 可以被视为种类运算符，并且
正如您在问题中所建议的，我们需要上升一个“级别”。我们
稍后在超越类型部分中返回这一点，但首先：

在依赖类型语言中情况如何。

您询问类型签名将如何查找采用
值并返回一个类型。这在 Haskell 中是不可能做到的：
函数不能返回类型！您可以使用以下命令模拟此行为
键入类和类型族，但让我们进行更改以进行说明
语言到依赖类型语言
Agda。这是一个
与 Haskell 语法相似的语言，其中将类型混合在一起
价值观是第二天性。

为了有一些东西可以使用，我们定义了一个自然的数据类型
数字，为了方便一元表示，如
皮亚诺算术。
数据类型写在
GADT 风格：

data Nat : Set where
    Zero : Nat
    Succ : Nat -> Nat

Set 相当于 Haskell 中的 *，所有（小）类型的“类型” ,
比如自然数。这告诉我们 Nat 的类型是
Set，而在 Haskell 中，Nat 没有类型，但它有
一种，即*。在 Agda 中没有种类，但一切都有
一种类型。

我们现在可以编写一个接受值并返回类型的函数。
下面是一个函数，它接受一个自然数 n 和一个类型，
并迭代应用于此的 List 构造函数 n
类型。（在 Agda 中，[a] 通常写作 List a）

listOfLists : Nat -> Set -> Set
listOfLists Zero     a = a
listOfLists (Succ n) a = List (listOfLists n a)

一些示例：

listOfLists Zero               Bool = Bool
listOfLists (Succ Zero)        Bool = List Bool
listOfLists (Succ (Succ Zero)) Bool = List (List Bool)

我们现在可以创建一个在 上运行的 map 函数列表列表。
我们需要取一个自然数，即迭代次数
列表构造函数。基本情况是当数字为
0，那么 listOfList 只是身份，我们应用该函数。
另一种是空列表，返回空列表。
步骤案例是一个有点移动，涉及：我们将 mapN 应用于头部
列表的，但这少了一层嵌套，并且 mapN
到列表的其余部分。

mapN : {a b : Set} -> (a -> b) -> (n : Nat) ->
       listOfLists n a -> listOfLists n b
mapN f Zero     x         = f x
mapN f (Succ n) []        = []
mapN f (Succ n) (x :: xs) = mapN f n x :: mapN f (Succ n) xs

在 mapN 类型中，Nat 参数被命名为 n，因此其余部分
类型可以取决于它。这是一个类型的例子
取决于一个值。

<子>
作为旁注，这里还有两个其他命名变量，
即第一个参数 a 和 b，类型为 Set。类型
变量在 Haskell 中是隐式普遍量化的，但是
这里我们需要把它们拼出来，并指定它们的类型，即
设置。括号的作用是让它们在视图中不可见
定义，因为它们总是可以从其他参数中推断出来。

集合是抽象的

你问(->)的构造函数是什么。需要指出的一件事
是 Set （以及 Haskell 中的 *）是抽象的：你不能
模式匹配就可以了。所以这是非法的 Agda：

cheating : Set -> Bool
cheating Nat = True
cheating _   = False

同样，您可以在类型构造函数上模拟模式匹配
Haskell 使用类型族，给出了一个典型的例子
布伦特·约吉的博客。
我们可以在 Agda 中定义 -> 吗？因为我们可以返回类型
函数，我们可以定义一个自己的 -> 版本，如下所示：（

_=>_ : Set -> Set -> Set
a => b = a -> b

中缀运算符写作 _=>_ 而不是 (=>)< /代码>）这个定义的内容很少，并且与做一个非常相似 Haskell 中的类型同义词：

type Fun a b = a -> b

超越种类：海龟一路向下

正如上面所承诺的，Agda 中的所有内容都有一个类型，但是然后
_=>_ 的类型必须有一个类型！这触及你的观点
关于类别，可以说是集合（类别）之上的一层。
在 Agda 中，这称为 Set1：

FunType : Set1
FunType = Set -> Set -> Set

事实上，它们有一个完整的层次结构！集合的类型是
“小”类型：haskell 中的数据类型。但是我们有Set1，
Set2、Set3 等等。 Set1 是提到的类型的类型
设置。这种层次结构是为了避免像吉拉德那样的不一致
悖论。

正如您在问题中注意到的， -> 用于类型和种类
Haskell，函数空间使用相同的符号
Agda 中的级别。这必须被视为内置类型运算符，
构造函数是 lambda 抽象（或函数
定义）。这种类型的层次结构类似于中的设置
System F omega 等
信息可以在后面的章节中找到
Pierce 的类型和编程语言。

纯类型系统

在 Agda 中，类型可以依赖于值，函数可以返回类型，
如上所示，我们还有一个层次结构
类型。对 lambda 不同系统的系统研究
在 Pure Type Systems 中对演算进行了更详细的研究。一个好的
参考是
带有类型的 Lambda 演算，作者：Barendregt，
其中第 96 页介绍了 PTS，第 99 页及以后的许多示例。
您还可以在那里阅读有关 lambda 立方体的更多信息。

You touch so many interesting points in your question, so I am
afraid this is going to be a long answer :)

Kind of (->)

The kind of (->) is * -> * -> *, if we disregard the boxity GHC
inserts. But there is no circularity going on, the ->s in the
kind of (->) are kind arrows, not function arrows. Indeed, to
distinguish them kind arrows could be written as (=>), and then
the kind of (->) is * => * => *.

We can regard (->) as a type constructor, or maybe rather a type
operator. Similarly, (=>) could be seen as a kind operator, and
as you suggest in your question we need to go one 'level' up. We
return to this later in the section Beyond Kinds, but first:

How the situation looks in a dependently typed language

You ask how the type signature would look for a function that takes a
value and returns a type. This is impossible to do in Haskell:
functions cannot return types! You can simulate this behaviour using
type classes and type families, but let us for illustration change
language to the dependently typed language
Agda. This is a
language with similar syntax as Haskell where juggling types together
with values is second nature.

To have something to work with, we define a data type of natural
numbers, for convenience in unary representation as in
Peano Arithmetic.
Data types are written in
GADT style:

data Nat : Set where
    Zero : Nat
    Succ : Nat -> Nat

Set is equivalent to * in Haskell, the "type" of all (small) types,
such as Natural numbers. This tells us that the type of Nat is
Set, whereas in Haskell, Nat would not have a type, it would have
a kind, namely *. In Agda there are no kinds, but everything has
a type.

We can now write a function that takes a value and returns a type.
Below is a the function which takes a natural number n and a type,
and makes iterates the List constructor n applied to this
type. (In Agda, [a] is usually written List a)

listOfLists : Nat -> Set -> Set
listOfLists Zero     a = a
listOfLists (Succ n) a = List (listOfLists n a)

Some examples:

listOfLists Zero               Bool = Bool
listOfLists (Succ Zero)        Bool = List Bool
listOfLists (Succ (Succ Zero)) Bool = List (List Bool)

We can now make a map function that operates on listsOfLists.
We need to take a natural number that is the number of iterations
of the list constructor. The base cases are when the number is
Zero, then listOfList is just the identity and we apply the function.
The other is the empty list, and the empty list is returned.
The step case is a bit move involving: we apply mapN to the head
of the list, but this has one layer less of nesting, and mapN
to the rest of the list.

mapN : {a b : Set} -> (a -> b) -> (n : Nat) ->
       listOfLists n a -> listOfLists n b
mapN f Zero     x         = f x
mapN f (Succ n) []        = []
mapN f (Succ n) (x :: xs) = mapN f n x :: mapN f (Succ n) xs

In the type of mapN, the Nat argument is named n, so the rest of
the type can depend on it. So this is an example of a type that
depends on a value.

_{As a side note, there are also two other named variables here,
namely the first arguments, a and b, of type Set. Type
variables are implicitly universally quantified in Haskell, but
here we need to spell them out, and specify their type, namely
Set. The brackets are there to make them invisible in the
definition, as they are always inferable from the other arguments.}

Set is abstract

You ask what the constructors of (->) are. One thing to point out
is that Set (as well as * in Haskell) is abstract: you cannot
pattern match on it. So this is illegal Agda:

cheating : Set -> Bool
cheating Nat = True
cheating _   = False

Again, you can simulate pattern matching on types constructors in
Haskell using type families, one canoical example is given on
Brent Yorgey's blog.
Can we define -> in the Agda? Since we can return types from
functions, we can define an own version of -> as follows:

_=>_ : Set -> Set -> Set
a => b = a -> b

(infix operators are written _=>_ rather than (=>)) This
definition has very little content, and is very similar to doing a
type synonym in Haskell:

type Fun a b = a -> b

Beyond kinds: Turtles all the way down

As promised above, everything in Agda has a type, but then
the type of _=>_ must have a type! This touches your point
about sorts, which is, so to speak, one layer above Set (the kinds).
In Agda this is called Set1:

FunType : Set1
FunType = Set -> Set -> Set

And in fact, there is a whole hierarchy of them! Set is the type of
"small" types: data types in haskell. But then we have Set1,
Set2, Set3, and so on. Set1 is the type of types which mentions
Set. This hierarchy is to avoid inconsistencies such as Girard's
paradox.

As noticed in your question, -> is used for types and kinds in
Haskell, and the same notation is used for function space at all
levels in Agda. This must be regarded as a built in type operator,
and the constructors are lambda abstraction (or function
definitions). This hierarchy of types is similar to the setting in
System F omega, and more
information can be found in the later chapters of
Pierce's Types and Programming Languages.

Pure type systems

In Agda, types can depend on values, and functions can return types,
as illustrated above, and we also had an hierarchy of
types. Systematic investigation of different systems of the lambda
calculi is investigated in more detail in Pure Type Systems. A good
reference is
Lambda Calculi with Types by Barendregt,
where PTS are introduced on page 96, and many examples on page 99 and onwards.
You can also read more about the lambda cube there.

回复收藏 0 原文

陈独秀 2025-01-08 15:16:54

首先，<代码>?? -> ？ -> * kind 是 GHC 特定的扩展。 ? 和 ?? 只是用来处理未装箱的类型，其行为与 * 不同（它必须装箱，到目前为止据我所知）。所以 ?? 可以是任何普通类型或未装箱类型（例如 Int#）； ? 可以是其中任何一个，也可以是未装箱的元组。这里有更多信息： Haskell 奇怪的种类：(->) 的种类是 ?? -> ？ -> *

我认为函数不能返回未装箱的类型，因为函数是惰性的。由于惰性值要么是一个值，要么是一个 thunk，因此必须将其装箱。 Boxed 只是意味着它是一个指针而不仅仅是一个值：就像 Java 中的 Integer() 与 int 一样。

由于您可能不会在 LYAH 级别的代码中使用未装箱的类型，因此您可以想象 -> 的类型只是 * ->; *-> *。

由于 ? 和 ?? 基本上只是 * 的更通用版本，因此它们与排序或类似内容没有任何关系。

但是，由于 -> 只是一个类型构造函数，因此您实际上可以部分应用它；例如，(->) e 是 Functor 和 Monad 的实例。弄清楚如何编写这些实例是一个很好的思维拓展练习。

就值构造函数而言，它们只能是 lambda (\ x ->) 或函数声明。由于函数对于语言来说是如此基础，因此它们有自己的语法。

回复收藏 0 原文

~没有更多了~

关于作者

夏雨凉

暂无简介

文章

27 人气

关注发私信

友情链接

文江博客

函数不仅仅有类型：它们是类型。和种类。和排序。帮助破碎的心灵重新整合起来

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

评论（2）

类似 (->)

在依赖类型语言中情况如何。

集合是抽象的

超越种类：海龟一路向下

纯类型系统

Kind of (->)

How the situation looks in a dependently typed language

Set is abstract

Beyond kinds: Turtles all the way down

Pure type systems

关于作者

相关话题

热门标签

推荐作者

櫻之舞

弥枳

m2429

寻找一个思念的角度

野却迷人

我怀念的。

友情链接

函数不仅仅有类型：它们是类型。和种类。和排序。帮助破碎的心灵重新整合起来

如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

评论（2）

类似 (->)

在依赖类型语言中情况如何。

集合是抽象的

超越种类：海龟一路向下

纯类型系统

Kind of (->)

How the situation looks in a dependently typed language

Set is abstract

Beyond kinds: Turtles all the way down

Pure type systems

关于作者

相关话题

热门标签

推荐作者

櫻之舞

弥枳

m2429

寻找一个思念的角度

野却迷人

我怀念的。

友情链接

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。