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

Question

我对Haskell很新,如果这是一个基本问题,或者基于不稳定理解的问题,那就很抱歉

类型级编程对我来说是一个很有意思的想法.我认为我得到了基本的前提,但我觉得还有另一面对我来说是模糊的.我认为这个想法是使用类型将逻辑和计算带入编译时而不是运行时.通过这种方式,您可以将通常的运行时逻辑/状态/数据转换为静态逻辑,例如集合的大小.

所以我得到了例如你可以有类型级自然数,并对这些自然数进行类型级算术,所有这些计算和类型安全性在编译时进行.

但这种算术在运行时意味着什么呢？特别是因为Haskell具有完全类型的擦除.所以举个例子

• 如果我连接两个类型级别列表,那么类型级别安全性是否意味着在运行时该连接的行为或性能？或者类型级编程方面只在编译时有意义,当程序员正在努力解决代码并将事物放在一起时？
• 或者,如果我有两个类型级别编号,然后将它们相乘,那么这在运行时意味着什么？如果这些大数字操作在编译时很慢,那么它们是否在运行时瞬间完成？
• 或者,如果我们实现了类型级别的RSA然后使用它,那在运行时甚至意味着什么呢？

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

Answer 1

正如你所说，Haskell [没有奇怪的扩展] 具有完整的类型擦除。因此，这意味着纯粹在类型级别计算的任何内容都会在运行时被删除。

但是，为了做有用的事情，您可以将类型级别的内容与值级别的内容连接起来以提供有用的属性。

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

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

• 要求调用者始终提供相同维度的向量，如果不满足该要求，则愉快地返回乱码。（即，忽略该问题。）
• 在运行时执行显式检查，Nothing如果维度不匹配，则抛出异常或返回或类似的情况。

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

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

它实际上与编译器所做的普通检查相同，以确保您不会尝试将整数乘以字符串或其他内容。这些类型在运行前全部被删除，但代码不会崩溃。

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

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