问题标签 [data-kinds]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
haskell - 具有更高种类的功能？
假设定义了以下数据类型：
必须有三个独立的函数，getX，getY和getZ？在我看来，可能有一个函数定义如下：
显然这不是有效的标准 Haskell，但是 GHC 有很多扩展，看起来他们可能有解决方案（、、、RankNTypes等ExistentialQuantification）DataKinds。除了避免少量键入的简单原因之外，还有避免记录解决方案产生的命名空间污染的好处。我想这实际上只是一个比使用这样的类型类更隐含的解决方案：
然而，定义泛型函数似乎比类型类更有用，因为它是隐式定义的，这意味着它可以在更多地方使用，就像使用($)or一样(.)。所以我的问题分为三个部分：有没有办法做到这一点，这是一个好主意，如果没有，什么是更好的方法？
haskell - 亲切的降级（相对于亲切的晋升）
DataKinds扩展将“值”（即构造函数）提升为类型。比如True和False变成不同种类的那种Bool。
我想做的是相反的，即将类型降级为值。具有此签名的函数会很好：
我实际上可以这样做，例如Bool：
但是，我必须为我想降级为它的值的任何类型编写实例。有没有更好的方法来做这不涉及这么多样板？
haskell - 无法将种类 '*' 与 'Nat' 匹配
我正在尝试创建一种保证字符串长度小于 N 个字符的类型。
这给出了错误：
我不明白这个错误。为什么它不起作用？我已经使用几乎完全相同的代码在其他地方获取 n 的 natVal 并且它可以工作。
有一个更好的方法吗？
haskell - 在数据类型的每个值上实例化的类型类
是否可以指定数据种类的每个成员都满足类型类，从而隐含类约束？例如
基本上a是一个AB，所以我们确定它有一个实例Foo。我觉得不太可能——从哪里得到Foo字典？- 但我在我的日子里看到了一些魔法。
haskell - 理解 HList 的这个定义
我对 Haskell 比较陌生，我正在尝试理解HList的定义之一。
我有几个具体问题：
我看到的
'[]and语法是什么？(x ': xs)它几乎看起来像是对可变参数类型参数的模式匹配，但我以前从未见过这种语法，也不熟悉 Haskell 中的可变参数类型参数。我猜这是GHC 的 Type Families 的一部分，但我在链接页面上看不到任何关于此的内容，而且在 Google 中搜索语法相当困难。除了避免装箱之外，使用
newtype带有元组的声明（而不是带有两个字段的声明）还有什么意义？dataHCons1
haskell - 带有 DataKinds 的 FromJSON 实例
尝试使用 TypeLits 对数据类型进行 JSON 反序列化，但遇到以下问题：
在以下示例中，在FromJSON实例中一般允许Nat的正确语法如何：
haskell - 嵌套类型级编程
我正在尝试使用 DataKinds 进行类型级编程，但是当我将其中一个结构嵌套在另一个结构中时遇到了困难。
一旦我添加了 ClassUpper 的最后一个实例，我就会得到一个错误。
我知道这'C ~ 'C表明类型相等，但我不明白根本问题是什么，更不用说解决方案或解决方法了。
我不明白什么，解决这个问题的最佳方法是什么？
haskell - 使用 DataKinds 时无法在 GHCI 中指定类型签名
因此，当我尝试在使用DataKinds. 我有以下代码：
此代码按预期编译。如果我SomeData在 ghci 中构造并且不指定类型，它可以正常工作：
但是，如果我尝试指定类型，则会出错：
似乎 ghci 没有解释这句话。我使用stack ghci. 有没有人遇到过这个？提前感谢您的帮助。
haskell - 如何使用 kind :: '[SomeDataKind] 处理递归 GADT
我认为这是我做过的最深入的 Haskell 类型系统扩展，我遇到了一个我无法弄清楚的错误。提前为篇幅道歉，这是我可以创建的最短示例，它仍然说明了我遇到的问题。我有一个递归 GADT，它的种类是提升列表，如下所示：
GADT 定义
问题
我想要做的是遍历数据并执行一些操作，例如将Just Char找到的第一个传播到顶部。
烦人的缺失功能 - 下一节需要
现在，因为显然没有对 GADT 的记录语法支持（https://ghc.haskell.org/trac/ghc/ticket/2595），您需要手动编写它们，所以它们是：
测试数据
所以，我想做的事情。从顶部向下走结构，直到找到一个值为Just. 所以给定以下初始值：
预期结果
我想要这样的东西：
以前的尝试
我试了几次，首先是一个常规功能：
这给出了错误：
我还尝试了一个类型类并尝试在结构上进行匹配：
这会导致错误：
我也尝试过匹配的组合，SomeData '[]但SomeData '[p]无济于事。
我希望我遗漏了一些简单的东西，但我还没有在任何地方找到关于如何处理这样的结构的文档，而且我对 Haskell 类型系统的理解有限，反正现在:)。再一次，很抱歉这篇长文，任何帮助将不胜感激:)
haskell - Haskell GADTs - 为黎曼几何制作类型安全的张量类型
我想使用 GADT 在 Haskell 中对张量演算进行类型安全的实现，所以规则是：
- 张量是具有“楼上”或“楼下”的不定值的 n 维度量，例如：
- 是没有定值的张量（标量），
是具有一个“楼上”索引
的张量，是具有一堆 ' 的张量楼上和楼下的猥亵 您可以添加相同类型的张量，这意味着它们具有相同的 indecies 签名。第一个张量的第 0 个索引与第二个张量的第 0 个索引的类型相同（楼上或楼下），依此类推...
~~~~ 好的
~~~~ 不好您可以将张量相乘并获得更大的张量，并将这些不定值连接起来：
所以我希望 Haskell 的类型检查器不允许我编写不遵循这些规则的代码，否则它不会编译。
这是我使用 GADT 的尝试：
但我得到：
问题是什么？