haskell - 类型级编程在运行时意味着什么？

Question

我对 Haskell 很陌生，如果这是一个基本问题，或者一个建立在摇摇欲坠的理解基础上的问题，我很抱歉

类型级编程对我来说是一个迷人的想法。我想我明白了基本前提，但我觉得它的另一面对我来说是模糊的。我知道这个想法是使用类型将逻辑和计算带入编译时而不是运行时。通过这种方式，您可以将通常的运行时逻辑/状态/数据转换为静态逻辑，例如集合的大小。

所以我知道，例如，你可以拥有类型级别的自然数，并对这些自然数进行类型级别的算术运算，所有这些计算和类型安全都在编译时进行。

但是这样的算术在运行时意味着什么？特别是因为 Haskell 具有完整的类型删除功能。所以例如

如果我连接两个类型级别的列表，那么类型级别的安全性是否暗示了该连接在运行时的行为或性能？或者类型级编程方面是否仅在编译时才有意义，当程序员正在处理代码并将事物放在一起时？

或者如果我有两个类型级别的数字，然后将它们相乘，这在运行时意味着什么？如果这些对大数的操作在编译时很慢，它们在运行时是瞬时的吗？

或者如果我们 implemented type level RSA然后使用它，这在运行时甚至意味着什么？

它纯粹是一个编译时安全/一致性工具吗？或者类型级编程是否也为我们购买了运行时的任何东西？逻辑和算术是“在编译时支付”还是仅仅“在编译时保证”(如果这甚至有意义的话)？

Answer 1

正如您所说的那样，Haskell [没有奇怪的扩展]具有完整的类型删除。所以这意味着任何纯粹在类型级别计算的东西都会在运行时被删除。

然而，为了做有用的东西，你将类型级别的东西与你的值(value)级别的东西连接起来，以提供有用的属性。

例如，假设您要编写一个函数，该函数接受一对列表，将它们视为数学向量，并与它们执行向量点积。现在点积仅在相同大小的向量对上定义。因此，如果向量的大小不匹配，您将无法返回合理的答案。

如果没有类型级编程，您的选择是:

要求调用者始终提供相同维度的向量，如果不满足该要求，则愉快地返回乱码。 (即，忽略问题。)

在运行时执行显式检查，并抛出异常或返回 Nothing如果尺寸不匹配或类似。

使用类型级编程，您可以做到如果维度不匹配，则代码无法编译!所以这意味着在运行时你不需要关心不匹配的维度，因为......好吧，如果你的代码正在运行，那么维度就不会不匹配。

此时类型已全部删除，但您仍然可以保证您的代码不会崩溃/返回乱码，因为编译器已经检查过不会发生这种情况。

这实际上与编译器进行的普通检查相同，以确保您不会尝试将整数乘以字符串或其他东西。这些类型在运行前都被删除了，但代码并没有崩溃。

当然，要进行点积，我们只需要检查两个数字是否相等。我们还不需要任何算术。但应该清楚的是，要检查向量的维度是否匹配，我们需要知道向量的维度。这意味着任何改变向量维度的操作都需要进行编译时计算，因此编译器可以知道结果大小并检查它是否满足要求。

你也可以做更复杂的事情。我在某个地方看到了一个库，它可以让您定义客户端/服务器通信协议(protocol)，但是因为它将协议(protocol)编码为极其复杂的类型签名[编译器自动推断]，它可以静态证明客户端和服务器实现完全相同的协议(protocol)(即，服务器没有处理客户端可以发送的消息之一的错误)。类型在运行时被删除，但我们仍然知道有线协议(protocol)不会出错。