问题标签 [data-kinds]

让我定义一个长度受限的列表。IE

然后我想从普通列表中初始化这个列表（例如任意长度的输入字符串）。我可以这样做吗？是否可以像这样编写函数（或类）？

或者这是否仅适用于编译时已知长度的结构？

使用DataKindsand KindSignatures，我可以执行以下操作：

当然，Haskell 在运行时删除了这种类型。我可以通过分离构造函数来保留这些信息：

然后当我进行模式匹配时，我也得到了类型。但现在我已经用完了所需的构造函数数量，我怀疑这将是一场维护噩梦。

我想做这样的事情：

然后我可以进行模式匹配DWrap以确定类型：

这应该没问题，因为一旦我们匹配T1我们就知道t然后我们知道我们是开始传递给的正确类型g。

当然，如果我只想忽略我喜欢的类型：

无论哪种方式，完整性检查都应该确保我不会做任何愚蠢的事情。

除了这种方法行不通。首先，因为t不是普通类型的 kind *，它是 kind T。其次T1甚至不是 type 'T1，它是 type 的成员T，就像等一样T2，T3所以这是区分类型的无用方法。

为了尝试解决第一个问题，我可以更改t为Proxy t：

现在这个data定义可以编译了，但是这对于区分类型是毫无用处的，因为Proxy只有一个构造函数。

我可以这样做：

然后这个：

然后我可以这样匹配：

这应该可以完成工作，但我必须写出data TConstructor，这几乎是data T. 无论如何我可以避免这个额外的样板并仍然实现我想要做的事情吗？

考虑以下代码

我试图说服 gchi:kind! forall x . C x => F x 解决2. 但看起来我只能在=>. 有没有办法解决这个问题？特别是我得到

编辑：将其包装在代理中似乎不起作用：

我正在尝试对一个类型级别的图进行编码，该图对边的构造有一些限制（通过类型类），但是当我尝试为构造图取别名时遇到了“类型中的非法约束”错误。是什么导致了这个问题？如果它不可行，是否有另一种方法来编码图形结构，以便它可以按类型构建并折叠以产生图形的值级表示？

编辑：渴望

我希望能够将图形的构造限制在任何两个操作的input和output节点上。

为了清楚起见，让我们以众所周知的长度索引向量为例。

Anoperation将采用input某种形状，并可能将其长度更改为output. 两者之间的优势operations需要确保第一个的输出与第二个的输入兼容——对于某些实例定义的兼容性概念来说。（下面，这些约束被省略了；应用程序需要在编译时对约束进行依赖类型验证和类型计算。）

为了定义一个S可以与现有操作（T等）一起使用的新操作，只需添加数据类型S、实现S _ 和必要的约束S作为实例的功能类型类的Edge。

要点在这里

在使用模板haskell 的haskell 项目中，我试图生成一个具有类型注释作为幻像类型的表达式。

一个简单的例子是这样的DataKinds情况KindSignatures：

我怎样才能写一个函数，像genType这样

提升只是提升保存编译时间Foo值的变量？我不知道使用类型数据构造函数中的哪个构造函数 来制作数据种类。

有什么想法吗？谢谢！

我正在解析一些输入，对此我有类似的东西：

然后我有我的解析功能：

所以，我现在有兴趣写一些看起来像这样的东西：

有什么方法可以让类型有意义吗？

我正在处理货币和货币操作。我希望操作是类型安全的，但我还需要将不同的货币一起存储在一个集合中，以便我可以搜索它们。

这两个目标似乎发生了冲突。

我可以使用选项类型来实现它，但在操作中我没有获得类型安全：

或者我可以为每种货币使用一种类型，但我不能轻松地创建和处理它们的汇率。

我现在是怎么做的

我目前的解决方案是货币作为不同类型和货币期权类型之间的同构，希望在程序的不同部分中拥有两全其美的优势。但这是一团糟。

我怎样才能在某些函数中具有类型安全性以及在其他函数中具有相同类型值的便利性？. 看起来像是一份工作，DataKinds但我看不出它有什么帮助。

请记住，我在编码时没有所有数据。它将从 API 中获取。

我正在研究单例类型可以在多大程度上模拟依赖类型并且我遇到了一个问题。我复制错误的最小代码是：

错误信息是：

预期种类 'SBool b'，但 ''SFalse' 有种类 'SBool 'False'</p>

什么样的f？

我写过：(* -> *) -> * -> * 这是正确的吗？c是具体类型*。a是一种接受类型并产生类型的类型。而这两个都是参数f？我的论证正确吗？

什么是种类T？

f有两种具体类型作为参数 (String和Int)。 g有一个参数 ( Bool) 这两个都是 的参数T。所以我有：(*->*->*)->(*->*)->*。这个对吗？谢谢