问题标签 [gadt]

为模糊的标题道歉，这里有一些上下文：http ://themonadreader.files.wordpress.com/2013/08/issue221.pdf

上一期的 GADTs 文章介绍了 Nat 类型和 NatSing 类型，用于各种类型级别的列表函数（concat、!!、head、repeat 等）。对于其中一些函数，有必要创建类型族以在 Nat 类型上定义 + 和 <。

无论如何，为了方便调用者，我编写了一个函数“list”，它将普通[a]转换为 。List n a这需要列表的长度作为输入，就像repeat（来自链接的文章）：

使用辅助函数会很好toNatSing :: Int -> NatSing n，所以上面可以写成

是否可以编写这样的函数toNatSing？我一直在与类型搏斗，但还没有想出任何东西。

非常感谢！

我正在尝试使用 Haskell 来了解 GADT 的概念，并尝试遵循 Peano Number 场景，

但是，我发现当我使用-fwarn-incomplete-patterns标志 (GHC-7.6.3) 编译它时，即使已满足所有可能的模式，它也会给我以下警告：

但是，当我为其中任何一种模式添加匹配项时，如下所示：

编译器（正确）给了我以下错误：

有没有办法编写这个函数或数据类型而不添加testFunc _ _ = undefined一行，这基本上使warn-incomplete-patterns标志对这个函数无用，并且用多余的丑陋垃圾使我的代码混乱？

给定一个GADT由幻像变量索引的索引，我可以使用独立派生来创建一些简单的实例

这似乎在 GHCi 中完美运行

但是，当我尝试编译时，会收到警告。

这似乎是 GADT 派生代码的一个错误位（re: Haskell Inaccessible code bug? and https://ghc.haskell.org/trac/ghc/ticket/8128）但因为它似乎有正确的行为我'我想知道

1. -fno-warn-*我可以用一些标志关闭这些警告吗？并且，如果可能的话
2. 这样做有什么问题的副作用吗？

我已经定义了一个可以包含任何东西的通用数据类型（嗯，当前的实现不是完全任何东西）！

这是（完整代码）：

我可以在控制台中使用它：

好吧，我有它，但我需要以某种方式处理它。例如，让我们定义转换函数（函数定义，添加到前面的代码）：

还有问题！之前代码中的fromAny定义不正确！而且我不知道如何使它正确。我在 GHCi 中得到错误：

我也尝试了其他一些给出错误的方法。

我对此有相当糟糕的解决方案：通过showAnyT定义必要的函数并读取（替换以前的函数定义）：

是的，这是工作。我可以玩它：

但我认为这很糟糕，因为它使用字符串进行转换。

你能帮我找到整洁和好的解决方案吗？

这只是一个测试，所以我不太担心，但我有以下定义：

我收到“type _ aVL =”的错误：

该怎么办？

我想完成这样的事情，但我不能完全理解语法。

Here is the code where I'm having an issue:

So I want to extend Tup to be defined over arbitrarily many arguments, same with sum. But a formulation involving lists would constrain the the final Term to one type of a:

I could just get rid of the a and do something like:

But then I lose the very things I'm trying to express.

So how do I express some polymorphic Term without loss of expressiveness?

一般问题

我有一对数据类型，它们是表示同一事物的两种不同方式，一种在 String 中记录变量名，而另一种在 Int 中记录变量名。目前，它们都已定义。但是，我只想描述第一种表示，而第二种表示将由某种关系生成。

具体例子

具体来说，第一个是 STLC 术语全域的用户定义版本，而第二个是同一事物的 de Bruijn 索引版本：

已经在Termand上定义了一个关系TermIn：

请注意，由于原始名称Term存储在 中，因此到和返回TermIn之间存在一对一的映射。TermTermIn

重述问题

现在您可以看到涉及多少样板，我想使用我定义的一些优雅的抽象Term和类型输出的一些函数来摆脱它TermIn。只是为了提供更多上下文，我正在为不同的 lambda 演算公式创建许多这样的外部和 de Bruijn 表示对，并且一对一的关系适用于所有这些。

我在我的程序中编译了以下代码：

由于构造函数的参数数量Foo可能很多，我想使用记录语法编写代码，但我不知道如何使用 GADT 语法来做到这一点（GHC 不推荐使用数据类型上下文，所以我试图避免它们） ：

我需要像上面那样在没有记录语法的情况下限制ain的构造函数。Foo我怎样才能做到这一点？

AFAIK 没有办法在 Haskell 中做异构数组或扩展数据类型。然而，它似乎可以通过使用嵌套对轻松实现（就像 CONS 一样）。

例如

可以像这样使用嵌套对编写；

这样访问器对于 Point2D 和 Point3D 来说是通用的

这种技术也可以用来扩展这样的记录

ETC ...

这是一个好主意吗？如果是这样，为什么 Haskell 中没有对此类东西的内置支持？这是 GADT 的目的吗？