我对Haskell很陌生，很抱歉，如果这是一个基本问题，或者是一个基于不稳定理解的问题
类型级编程对我来说是一个迷人的想法。我想我明白了基本的前提，但我觉得它的另一面对我来说是模糊的。我知道这个想法是使用类型将逻辑和计算引入编译时而不是运行时。通过这种方式，您可以将通常的运行时逻辑/状态/数据转换为静态逻辑，例如集合的大小。
因此，我得到例如，您可以拥有类型级别的自然数，并对这些自然数进行类型级别的算术，所有这些计算和类型安全都在编译时进行。
但是这样的算术在运行时意味着什么？特别是因为Haskell具有完整的类型擦除功能。所以例如
- 如果我连接两个类型级别列表，那么类型级别安全性是否暗示了该串联在运行时的行为或性能？还是类型级编程方面仅在编译时有意义，当程序员正在处理代码并将事情放在一起时？
- 或者，如果我有两个类型级别编号，然后将它们相乘，这在运行时意味着什么？如果这些对大量数据的操作在编译时很慢，那么它们在运行时是瞬时的吗？
- 或者，如果我们实现了类型级 RSA 然后使用它，这在运行时意味着什么？
它纯粹是一个编译时安全/一致性工具吗？ 还是类型级编程也为我们提供了运行时的东西？逻辑和算术是"在编译时付费"还是仅仅"在编译时保证"(如果这甚至有意义(？
正如您正确所说，Haskell[没有奇怪的扩展名]具有完整的类型擦除功能。因此，这意味着纯粹在类型级别计算的任何内容都会在运行时擦除。
但是，要做有用的事情，你需要将类型级的东西与值级的东西联系起来，以提供有用的属性。
例如，假设您要编写一个函数，该函数采用一对列表，将它们视为数学向量，并用它们执行向量点积。现在，点积仅在相同大小的向量对上定义。因此，如果向量的大小不匹配，则无法返回合理的答案。
如果没有类型级编程，您的选项是：
要求- 调用方始终提供相同维度的向量，如果不满足该要求，则愉快地返回乱码。(即忽略问题。
- 在运行时执行显式检查，如果维度不匹配，则引发异常或返回
Nothing或类似内容。
使用类型级编程，您可以做到如果维度不匹配，代码就不会编译！所以这意味着在运行时你不需要关心不匹配的维度，因为......好吧，如果您的代码正在运行，那么维度就不会不匹配。
此时这些类型已被全部删除，但您仍然可以保证您的代码不会崩溃/返回乱码，因为编译器已检查这不会发生。
这实际上与编译器所做的普通检查相同，以确保您不会尝试将整数乘以字符串或其他东西。这些类型都在运行时之前被擦除，但代码不会崩溃。
当然，要做点积，我们只需要检查两个数字是否相等。我们还不需要任何算术。但应该清楚的是，要检查向量的维度是否匹配，我们需要知道向量的维度。这意味着任何改变向量维度的操作都需要进行编译时计算，因此编译器可以知道结果大小并检查它是否满足要求。
你也可以做更复杂的事情。我在某处看到一个库，它允许你定义客户端/服务器通信协议，但由于它将协议编码为非常复杂的类型签名[编译器自动推断]，它可以静态证明客户端和服务器实现完全相同的协议(即，服务器不处理客户端可以发送的消息之一没有错误(。这些类型在运行时被擦除，但我们仍然知道有线协议不会出错。