问题标签 [data-kinds]

I have found that I really like combining GADTs with Data Kinds, as it gives me further type safety than before (for most uses, almost as good as Coq, Agda et al.). Sadly, pattern matching fails on the simplest of examples, and I could think of no way to write my functions except for type classes.

Here's an example to explain my sorrow:

We have 2 type classes (one for the theorem, one for a utility operation) and 5 instances - just for a trivial theorem. Ideally, Haskell could look at this function:

And type-check each clause on its own, and per-call decide which cases are possible (thus worth trying to match) and which are not, so when calling trans Le_base Le_base Haskell will notice that only the first case allows for the three variables to be the same, and only attempt matching on the first clause.

GHC 7.6.1 带有用于类型级别编程的新功能，包括数据类型提升。以那里关于类型级自然数和向量的示例为例，我希望能够在依赖于基本算术定律的向量上编写函数。

不幸的是，即使我想要的定律通常很容易通过案例分析和归纳来证明归纳自然，但我怀疑我能否说服类型检查器。举个简单的例子，对下面的朴素 reverse 函数进行类型检查需要证明n + Su Ze ~ Su n.

有什么方法可以提供该证明，还是我现在真的处于成熟的依赖类型领域？

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

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

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

Plus 家族现在返回Nat一种：

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

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

例如，尝试编译以下代码

给出类型错误

我可以看到为什么这不起作用，但是有一些解决方案不需要我手动编写 Eq（和 Ord）实例吗？

所以我最近想出了这个巧妙的想法，希望在严格和懒惰的State转换器模块之间共享代码：

您可以看到，get它们put都可以在严格类型和惰性类型上工作，没有任何重复——没有类型类实例，没有任何东西。但是，即使我涵盖了这两种可能的情况Strictness，但我通常没有 Monad 实例State t s a：

以下工作正常，尽管需要FlexibleContexts：

然后我可以t在Lazyor处实例化Strict并运行结果并得到我期望的结果。但是为什么我必须给出这个背景呢？这是一个概念上的限制，还是一个实际的限制？有什么原因我错过了为什么Monad (State t s a)实际上不成立，还是没有办法说服 GHC 呢？

（旁白：使用上下文Monad (State t s) 不起作用：

Could not deduce (Monad (State t [Bool])) arising from a do statement from the context (Monad (State t s))

这让我更加困惑。前者肯定可以从后者推导出来吗？）

我创建了一个非常简单的示例，说明我在使用 GADT 和 DataKinds 时遇到的问题。我的实际应用程序显然更复杂，但这清楚地抓住了我的情况的本质。我正在尝试创建一个可以返回任何类型为 Test 的值（T1，T2）的函数。有没有办法做到这一点，或者我正在进入依赖类型的领域？这里的问题看起来很相似，但我无法从他们那里找到（或理解）我的问题的答案。我刚刚开始了解这些 GHC 扩展。谢谢。

类似问题 1

类似问题2

----这里是错误---- Test.hs:14:26:

我试图很好地掌握种类、类型和术语（或值，不确定哪个是正确的）以及用于操作它们的 GHC 扩展。我知道我们可以使用 TypeFamilies 来编写带有 Types 的函数，现在我们还可以在某种程度上使用 DataKinds、PolyKinds 等来操作 Kinds。我读过这篇关于Singleton Types 的论文，虽然我还没有完全理解它，但它看起来很有趣。这一切都让我想知道，有没有办法创建一个基于 Term 或 Value 级别的计算来计算返回类型的函数？这是依赖类型实现的吗？

这是我在想的一个例子

- 更新 - - - -

基于这里的大量研究和帮助，我现在很清楚，无论我启用多少扩展，函数的返回类型永远不能基于 Haskell 中值级别的表达式来计算。所以我发布了更多我的实际代码，希望有人能帮助我决定前进的最佳方式。我正在编写一个以圆锥曲线和二次曲面为基本类型的小型库。对这些类型的操作涉及计算它们之间的交集。2个曲面的交点是圆锥曲线的一种类型，包括像点一样的退化（实际上除了圆锥之外还需要另一种类型的曲线，但除了点之外）。确切的曲线返回类型只能由运行时相交曲面的值确定。圆柱体 - 平面相交可以产生无、直线、圆或椭圆。我的第一个计划是像这样使用 ADT 来构造曲线和曲面......

...这是最直接的，并且具有作为一个很好的封闭代数类型的优点，我喜欢。在这种表示中，交集的返回类型很简单，它只是曲线。这种表示的缺点是这些类型的每个函数都必须为每种类型进行模式匹配并处理所有排列，这对我来说似乎很麻烦。Surface-Surface 相交函数将有 16 个图案进行匹配。

下一个选项是保持每个 Surface 和 Curve 类型独立。像这样，

从长远来看，这似乎更灵活，而且很好且细化，但需要包装器 ADT 才能处理来自交集函数的多种返回类型或构建一般“曲线”或“表面”的列表因为他们之间没有任何关系。我可以使用类型类和存在来对它们进行分组，但是我失去了我不喜欢的原始类型。

这些设计中的妥协让我尝试了这个。

...起初我认为这会给我一些神奇的，两全其美的场景，我可以通过“曲线”引用任何曲线类型（如在列表或交集返回类型中）并且还具有完整类型可用（Curve CrvIdx）使用多参数类型类等以粒度样式编写函数。我很快发现这并不像我希望的那样工作得很好，正如这个问题所示。我一直顽固地继续用头撞墙，试图找到一种方法来编写一个函数，该函数可以根据运行时参数的几何属性从我的 GADT 中选择返回类型，现在意识到这不会发生。所以现在的问题是什么是表示这些类型以及它们之间的交互的有效和灵活的方式？谢谢。

假设我在 Haskell 中编写了一些类型级别的程序：

我认为这很有用，我想在我的项目中使用它。所以我把它放在一个模块中。

什么是模块的好分层名称？（参见Haskell 分层模块）

很多数据结构都存在于Data( Data.Text,Data.List等) 中，各种结构化效果的方式都存在于Control诸如Control.MonadorControl.Applicative中。

类型级程序应该放在哪里？ Type? TypeFamily? 达成共识了吗？

我正在尝试为长度索引列表实现一种拉链，它将返回列表中的每个项目与删除该元素的列表配对。例如对于普通列表：

以便

我目前尝试为长度索引列表实现相同的东西：

这感觉应该是相当简单的，但是由于似乎没有任何方法可以向 GHC 传达例如+可交换和关联或零是身份，所以我遇到了很多问题，其中类型检查器 (可以理解）抱怨它无法确定 thata + b ~ b + a或 that a + Zero ~ a。

我是否需要添加某种证明对象（data Refl a b where Refl :: Refl a a等），或者有什么方法可以通过添加更明确的类型签名来完成这项工作？

理解我在问什么需要以下定义：

我想使用这些定义编写一个函数，其工作方式如下：

在哪里

和

基本思想是接受不同形状的输入并根据用于 S 的构造函数和构建 R 时选择的参数产生不同形状的输出。我一直在尝试使用具有数据类型的类来做到这一点，但我得到了种类不匹配错误。我想知道是否有一种直观、干净的方式来编码这种类型的东西。

我目前的尝试如下：

这种方法抱怨 R 的第一个参数应该有 kind Param 但 Param 有 kind *，我不知道如何纠正这个问题。添加约束并使用变量时，我到了这里：

当然，Haskell 拒绝让我使用 Kind 作为约束。我很迷茫，我不知道该去哪里。任何帮助或指导都是无价的。