问题标签 [gadt]

假设我正在编写一个 DSL，并希望同时支持幻像类型和错误类型的表达式。我的价值类型可能是

我可以使用幻象擦除版本

Valunk现在，我可以通过case删除两者来操作值，VNum甚至VBool以这种方式重新建立我的幻象类型

但这只是感觉就像我正在重新实现Typeable机器。不幸的是，GHC 不会让我推导出一个TypeableforVal

有没有办法绕过这个限制？我很想写

但现在我不得不求助于这样的机器

对于我所有的类型。

如何以尽可能类型安全的方式将 Haskell 函数降低为嵌入式语言。特别是，假设我有一个像

我想将一个函数转换(isSucc :: Int -> Int -> Bool)为它的动态形式和一些类型信息的产品，像这样

这样对于某些apply功能

如果动态类型实际上不匹配，可能会引发一些可能的异常。或者，更明确地说，我想找到makeDynamicFn :: FunType -> SplitFun. 显然，这不是一个合适的 Haskell 类型，而且不太可能有一种方法可以从isSucc自身中提取类型，所以它可能更像是

whereanInt和retBoolhave printf-style 类型。

这样的事情可能吗？有没有办法模拟它？

Sorry for the terrible title. I'm trying to make an instance of Applicative for a Monad wrapping a type that is a Monoid.

This doesn't work; GCHi complains with:

I realise that what I've written above may make no sense. Here is the context: I am trying to use the compos abstraction as described in the paper A pattern for almost compositional functions. Taking this tree (using the GADT version of compos; I've simplified it a lot):

I'm going to write a lot of functions which descend the tree and return a list of say errors or a set of strings whilst also requiring state as it goes down (such as the binding environment), such as:

I think these should all be able to be abstracted away by making composFoldM use compos for the (Monad m, Monoid o) => m o structure. So to use it with the GADT Applicative version of compos found on page 575/576 of the paper. I think I need to make an Applicative instance of this structure. How would I do this? Or am I going down completely the wrong path?

（使用注释更容易复制和粘贴）

是否有可能编写这种会做“正确的事情”的类？也就是说，我如何更改程序以选择正确的实例。

我想我知道一种运行时解决方案，但这不会那么好。

我见过重写规则，这是一个好的解决方案吗？

首先，这是我的代码的最小示例：

我使用 GADT 来避免混合不同类型的 URL。myExportURL各种 URL的功能都是一样的。有没有办法使用这样的东西：

而不是为 GADT 的每个子类型（正确的术语是什么？）重复它？

也欢迎对代码或我试图解决的问题提出任何其他意见。

I have this type and these functions:

The code doesn't typecheck:

But I can't understand why not. Tag a has the context (Show a, Eq a, Ord a, Storable a, Binary a), and getVal ought to preserve this context. Am I doing it wrong, or is this a limitation of the GADTs extension?

This works:

Edit: I changed the example to a minimal example

Edit: Ok, why doesn't this typecheck?

我不得不使用很多扩展来为 Haskell 中的嵌入式语言创建一个安全的表示。在我引入相互函数依赖的某个时刻，类型推断停止了找出类型变量的正确替换。请参见下面的示例：

有趣的是，当我使用 TypeFamily 时Connect它很好：

两种情况下的类型解析有什么区别？

我有以下代码

编译或解释时-Wall给出以下警告：

通常这是可以预料的。通常，即使我可以推断出我的模式将涵盖所有可能的情况，编译器也无法在不运行代码的情况下知道这一点。然而，所提供模式的详尽性由在编译时运行的类型检查器强制执行。添加 GHC 建议的模式会产生编译时错误：

所以我的问题是：GHC 警告是否不能很好地与 GHC 扩展配合使用？他们应该互相了解吗？此功能（考虑到扩展的警告）是否计划在未来版本中发布，或者实现此功能是否存在一些技术限制？

似乎解决方案很简单；编译器可以尝试将假定不匹配的模式添加到函数中，并再次询问类型检查器是否建议的模式类型正确。如果是，那么它确实可以作为缺失模式报告给用户。

假设我想用常数 c、一元函数符号 f 和谓词 P 表示一阶语言的有限模型。我可以将载体表示为列表m，常数表示为 的元素m，函数表示为有序列表的元素对m（可以通过辅助函数应用ap），谓词作为m满足它的元素的列表：

然后我可以在模型上构建特定的模型和操作。细节对我的问题并不重要，只是类型（但我已经包含了定义，因此您可以看到类型约束的来源）：

现在，我想为所有这些模型命名：

最后，我想编写这段代码，将每个名称映射到它命名的模型：

在定义类型的意义上，我尝试了多种方法来使其工作，以便我可以准确地使用 model_of 的这个定义，包括使用幻像类型、GADT 和类型系列——但还没有找到一种方法去做吧。（但话又说回来，我是 Haskell 的新手。）可以做到吗？我该怎么做？

我正在阅读GADT 演练，但被困在其中一个练习上。给定的数据结构是：

练习是实现一个safeTail功能。我希望它的行为类似于tailPrelude 中的功能：

^{（我实际上并没有定义==，但希望我的意思很清楚）}

这可以做到吗？我不完全确定它会是什么类型……也许safeTail :: MarkedList a Safe -> MarkedList a NotSafe吧？