问题标签 [gadt]

我正在阅读一篇关于 Haskell 以及 HList 是如何实现的研究论文，并想知道所描述的技术何时可以确定，何时不能确定类型检查器。此外，因为您可以使用 GADT 做类似的事情，所以我想知道 GADT 类型检查是否总是可确定的。

如果你有引用，我会更喜欢引用，这样我就可以阅读/理解解释。

谢谢！

代码：

我希望Const a包含一个 show 类型的值，以便我以后可以打印它。所以在 C# 中我会写：

我怎么能在 Haskell 中做到这一点？

如何使用广义代数数据类型？

haskell wikibook中给出的示例太短，无法让我深入了解 GADT 的真正可能性。

我开始在 Haskell Wiki 中阅读有关 GADT 的内容，但对理解它感到不太自在。您是否会为 Haskell 初学者推荐特定的书籍章节或解释 GADT 的博客文章？

假设我们定义了一个 GADT 来比较类型：

那么是否可以使用以下类型签名声明函数eqt ：

...这样如果typeOf x == typeOf y ---则eqt xy评估为Just Witness ，否则为Nothing？

函数eqt可以将普通的多态数据结构提升为 GADT。

给定一种简单的语言，说

那么是否可以将其转换为类型化表示：

我尝试了各种方法，例如：

这不起作用，我收到以下错误消息：

约束中的模棱两可的类型变量 'a'：
'Typeable a'
源于在 ... 使用 'e2t'
可能的修复：添加一个类型签名来修复这些类型变量

但是，如果我确实喜欢这样

它编译。

在回答问题并提出使用 GADT 的建议时，评论中出现了一些关于性能的问题。这个问题涉及一个类型类PlotValue：

我的回答建议使用 GADT Input：

但我想，细节无关紧要。

我想知道性能的两个方面：

时间：模式匹配是否会产生任何运行时成本，例如

超出匹配两个Maybe值的正常成本？

空间Input：一个类型的值携带多少存储开销？我的猜测是，它PlotValue为每个类型的值Input（每个“指针”？）都携带两个字典，这意味着 a[Input]在内存使用方面比使用(Just Double, Just Double)or 效率低得多，或者更好，(# #Double, #Double #)如果你存储value正常或未打包元组中的结果。

所以，虽然我喜欢 GADT 给我的表现力，但我从来没有过多地考虑过性能方面。谁能告诉我更多关于这一点（以及我可能不知道的任何其他隐藏成本）？

我编写了以下 Haskell 程序来解释基本数学。除了数学运算符之外，我还想添加比较和布尔运算符。我的问题是我应该如何用可以处理or的Int东西替换出现的.IntBool

我考虑将Token类型扩展为具有三种类型的运算符，它们仅在函数的类型（(Int -> Int -> Int)、、(Int -> Int -> Bool)和）上有所不同(Bool -> Bool -> Bool)，但这似乎会导致在类型声明和模式匹配。有没有办法用类型类来做到这一点？

我有一个定义为（缩写）的 GADT，

编译器正确地抱怨它不能为 R 派生 Show。在这种情况下，我们知道 (Either ab) 属于 Show 类，但如果 b 属于 Show 类，我们不知道这是真的。错误信息是，

似乎需要能够限定存在类型，例如对存在类型 b 说“Show b => Show (D (Either ab))”，或者升级含义“(Show a, Show b) = > Show (Either ab)" 所以它是双向的。

非常感谢！

（请随意清理标题或描述。）

我有一个很像这样的 GADT：

它包装了各种输入原语，但最后一个构造函数也允许一个 Functor 实例：

顺便说一句，这种类型的要点是支持：

我想要做的是在这种类型上定义明显的 Eq 实例，例如：

问题是第三种情况，它失败了，因为此时 x 和 y 不一定具有相同的类型。我明白那个。在我自己的代码中，我可以进行长时间的解决，但感觉应该有一种方法可以直接定义 Eq。在我看来，解决方案类似于“不断钻取 F 构造函数，直到你点击 M 或 T，然后如果它们是相同的构造函数（即 M 或 T ）且类型相同，则进行相等比较”，但我'不知道我怎么能写出来。