问题标签 [type-level-computation]

假设我已经用 Haskell 类型对自然数进行了编码，并且我有一种方法可以对它们进行加减运算：

我已经看到了各种创建可变参数函数外观的代码，例如this，它允许以下内容：

我想知道的是我是否可以在此基础上构建一个只接受与类型号实例相对应的参数数量的函数。我想要做的看起来像：

我知道这很愚蠢，可能是在浪费我的时间，但这似乎是周末有趣的事情。

是否可以使用数字参数创建类型？

即，如果我想创建一种具有固定位宽的整数：

这样类型检查器只允许FixedWidth相同类型的 s 相加或相乘，而且还要确定结果的正确精度。

我知道你可以这样做：

并将数字 4 表示为Succ (Succ (Succ (Succ Nil))))，但这非常难看。我还需要弄清楚如何Succ为乘法结果类型附加两个 s。

第一次尝试

很难使这个问题简洁，但提供一个最小的例子，假设我有这种类型：

这种类型让我很高兴地构建了以下异构列表：

但是，唉，当我写下一个Eq实例时，事情就出错了：

啊，所以我们Could not deduce (a1 ~ a)。非常正确; 定义中没有任何内容说x并且y必须是相同的类型。事实上，重点是允许它们不同的可能性。

第二次尝试

让我们Data.Typeable混合起来，如果它们恰好是相同的类型，则只尝试比较两者：

这很不错。如果x和y是相同类型，则使用底层Eq实例。如果它们不同，它只会返回False. 但是，此检查会延迟到运行时，从而nonsense = Val2 True == Val2 "Hello"可以毫无怨言地进行类型检查。

问题

我意识到我在这里与依赖类型调情，但是 Haskell 类型系统是否有可能静态拒绝类似上述内容nonsense，同时允许类似在运行时sensible = Val2 True == Val2 False交回的内容False？

我处理这个问题的次数越多，我就越需要采用HList的一些技术来实现我需要作为类型级函数的操作。但是，我对使用存在主义和 GADT 比较陌生，我很想知道是否可以找到解决方案。所以，如果答案是否定的，我非常感谢讨论这个问题究竟在哪里达到了这些功能的限制，以及推动适当的技术、HList 或其他方式。

在我看来，使haskell 真正好用的大部分是组合符，例如,(.)等。感觉就像我可以在需要时创建新语法一样。flip$ <*>

前段时间我正在做一些事情，如果我可以“翻转”一个类型构造函数，那将非常方便。假设我有一些类型构造函数：

并且我有一个类MyClass需要一个带有 kind 类型构造函数的类型* -> *。自然，我会选择以我可以做到的方式对类型进行编码：

但是假设我无法更改该代码，并假设真正适合MyClass的内容类似于

然后我必须激活XTypeSynonymInstances. 有没有办法创建一个“类型级组合器” Flip，这样我就可以做到：

?? 还是我们在 haskell 中使用的常见运算符的其他类型级别的概括？这甚至有用还是我只是漫无目的？

编辑：

我可以做类似的事情：

但后来我不得不使用数据构造函数Flip, Dot, ... 来进行模式匹配等。值得吗？

兴奋地玩弄无形的自然数，我想知道获得例如 nats 乘积的整数值的最佳方法是什么。

摘自无形nat.scala：

到目前为止，我已经提出了简单的定义

事实上，这种方法需要对等价代码进行一些冗余的实现，例如求和、差异、阶乘等。所以我宁愿能够使用“默认”方法toInt[A <: Nat]。

你会怎么做？是否可以使用内部类型（Prod#Out，，Sum#Out...）？

我有以下使用 ghcs 扩展的固定长度向量的定义GADTs，TypeOperators并且DataKinds：

以及 TypeOperator 的以下定义:+：

为了使我的整个意图库有意义，我需要将类型的固定长度向量函数(Vec n b)->(Vec m b)应用于较长向量的初始部分Vec (n:+k) b。让我们调用那个函数prefixApp。它应该有类型

这是一个示例应用程序，其change2定义如下：

prefixApp应该能够应用于change2任何长度> = 2的向量的前缀，例如

有谁知道如何实施prefixApp？（问题是，必须使用固定长度向量函数类型的一部分来获取正确大小的前缀......）

编辑：Daniel Wagners（非常聪明！）解决方案似乎与 ghc 7.6 的一些候选版本（不是官方版本！）一起使用。恕我直言，它不应该工作，但是，有两个原因：

1. for 的类型声明在上下文中prefixApp缺少一个（用于正确类型检查。VNum mprepend (f b)
2. 更有问题：ghc 7.4.2 不假设 TypeOperator:+在其第一个参数中是单射的（也不是第二个，但这里不是必需的），这会导致类型错误：从类型声明中，我们知道vec必须有type并且类型检查器为定义右侧Vec (n:+k) a的表达式推断出. 但是：类型检查器无法推断出这一点（因为没有单射的保证）。split vecVec (n:+k0) ak ~ k0:+

有谁知道第二个问题的解决方案？我怎样才能在它的第一个论点中声明:+是单射的和/或我怎样才能完全避免遇到这个问题？

我的问题可能最容易以示例的形式解释：

但是，这里的第二个实例被拒绝，因为(+)本身是一个类型族，不能在参数中使用。但似乎没有任何Succ或任何东西通常用于匹配 Nats。

那么，这可以表达吗？如果是这样，如何？

更新。我注意到isZero和中的isEven函数在GHC.TypeLits“破坏类型nats”的标题下。它们是否打算以某种方式在类型级别使用？我怀疑不会……但主要是因为我不知道该怎么做。:)

我一直在自学类型级编程，并想编写一个简单的自然数加法类型函数。我的第一个版本如下：

所以在 GHCi 中我可以这样做：

哪个按预期工作。Z然后我决定通过修改和S类型来尝试 DataKinds 扩展：

Plus 家族现在返回Nat一种：

修改后的代码可以编译，但问题是我现在在测试时遇到错误：

我一直在寻找解决方案，但谷歌让我失望了。是否存在解决方案或者我是否达到了语言的某些限制？

首先，我从一些典型的类型级自然数开始。

所以我想创建一个表示 n 维网格的数据类型。（在评估元胞自动机中发现的内容的概括是 comonadic。）

这个想法是类型U num x是 s 的一num维网格的类型x，它“聚焦”在网格中的特定点上。

所以我想把它做成一个comonad，我注意到我可以做这个潜在有用的功能：

就这个组合器而言，我们现在可以实现一个“维度连接”，将 m 维网格的 n 维网格转换为 (n+m) 维网格。cojoin这在处理将产生网格的结果时会派上用场。

到目前为止，一切都很好。我还注意到该Functor实例可以用ufold.

但是，这会导致类型错误。

但是如果我们制作一些复制意大利面，那么类型错误就会消失。

好吧，我讨厌复制意大利面的味道，所以我的问题是这个。我怎样才能告诉类型系统Plus n Z等于n？问题是：您不能对会导致dimJoin产生类似类型错误的类型族实例进行更改。

我有类，参数化HList和其他类型。如何在其中一种方法中使用mapon HList？

此代码的编译抛出java.lang.AssertionError：

我的目标是这样的结果：