问题标签 [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.

0 投票
0 回答
167 浏览

haskell - 促进复杂的 GADT

我最近一直在玩弄-XDataKinds,想知道为什么Foo下面不会自动升级:

也就是说,Baz是 的异构列表Foo a,其中a受 约束Bar

有没有办法手动创建这种数据类型的升级版本?我该怎么做呢?可以声明种类吗?我可以制作一个虚拟的 Haskell98 版本Foo,并将其分成一个模块或其他东西吗?理想情况下,我想保留约束上下文,但我认为没有Constraint排序。任何想法都会非常有帮助!

0 投票
0 回答
86 浏览

haskell - 在具有 DataKinds 的 GADT 的种类签名中使用非加糖列表语法

我正在阅读给 Haskell 一个推广http://dreixel.net/research/pdf/ghp.pdf

我遇到了这种语法(如果你使用它就有效{-# LANGUAGE KindSignatures, GADTs, DataKinds, TypeOperators #-}):

检查[]using的信息:info [],告诉我列表的数据类型是:

这让我觉得,这种风格也应该起作用,因为[] a类型构造函数现在被提升为一种类型的构造函数:

但它没有,并给了我这个错误:

0 投票
1 回答
127 浏览

haskell - 在 Haskell 中声明和使用 Kinds

最近我一直在玩 Haskell 的-XDataKinds功能,并且发现自己想要创建一种。

我不确定我的愿望是否能实现,但从 Edward Kmett 的约束包中,似乎有一个声明的种类Constraint(带有 sort BOX),它说是在 中定义的GHC.Prim,但我找不到它。

有没有办法在 Haskell 或 GHC 中手动声明一种?这可能需要手动断言声明的数据类型data是正确的。我的想法是这样的:

0 投票
1 回答
94 浏览

haskell - 不寻常的种类和数据构造函数

我不知道我怎么没有注意到这一点,但是数据构造函数和函数定义都不能使用类型以外的类型*和它的变体* -> *等,因为(->)'s kind 签名,即使在-XPolyKinds.

这是我尝试过的代码:

我得到的错误如下:

为什么我们不应该允许非传统类型的模式匹配?

0 投票
1 回答
296 浏览

haskell - 带有 DataKinds 的 HList,种类不可推广

我有这个代码片段,它使用了大量的 GHC 扩展:

GHC 抱怨说:

为什么我不能晋升HList为一种?我使用 GHC7.8.27.11.

当然,使用内置的'[]作品就好了:

我想使用我自己的HList而不是'[]因为实际HList支持附加并且看起来像这样:

编辑:主要目标是让 GHC 推断

这样我就可以写了

我曾希望为附加类型级别列表添加显式表示可以帮助我实现这一目标。还有其他方法可以说服 GHC 吗?

0 投票
1 回答
564 浏览

haskell - 以组合方式将异构提升类型反射回值

我最近一直在玩-XDataKinds,并想采用类型族的提升结构构建并将其拉回价值水平。我相信这是可能的,因为组合组件非常简单,终端表达式也很简单。

背景

我想降级/反映简单的玫瑰树Strings,它们成为一种类型Tree Symbol(当GHC.TypeLits.Symbol用作类型级字符串时)。这是我的样板代码:

这是一个简单的类型级玫瑰森林,看起来像这个非常详细的图表:

尝试的解决方案

理想情况下,我想遍历这个结构并将 1 对 1 映射回kind的*,但是由于重载而仍然保留(必要的)实例的同时如何异构地执行此操作并不是很明显。

vanila on#haskell建议我使用类型类来绑定两个世界,但这似乎比我想象的要棘手。我的第一次尝试尝试通过实例头约束对类型级模式匹配的内容进行编码,但我的关联类型(用于编码*映射的 -kinded 类型结果)重叠 - 显然实例头在某种程度上被 GHC 忽略了

理想情况下,我还希望列表和树的反射是通用的,这似乎会导致问题 - 这就像使用类型类来组织类型/种类层。

这是我想要的一个非功能示例:

...

这段代码有几处通常是错误的。这是我看到的:

  • 我需要某种形式的前瞻来了解泛型类型级列表反射的更高种类反射的结果 -PostReflection类型函数
  • 我需要即时创建和销毁Proxy。我不确定这目前是否无法编译,但我不相信这些类型会像我期望的那样统一。

但是,这种类型类层次结构感觉像是捕获异构语法的唯一方法,所以这可能仍然是一个开始。对此的任何帮助都将是巨大的!

0 投票
2 回答
771 浏览

haskell - 我可以使用返回由参数编码的类型值的 DataKinds 编写函数吗?

假设我有一个货币类型:

以及存储 int 的 Money 类型,并由给定的 Currency 参数化(Currency 被提升为具有 DataKinds 扩展名的种类)。

是否可以编写一个函数,moneyOf将货币值作为其参数,并返回由货币值的相应类型参数化的货币值?比如moneyOf :: Currency -> Money c,但是我们得到一个编译时保证c是从 Currency 值生成的类型?

0 投票
1 回答
323 浏览

haskell - GADT 中任何“DataKind”的列表

免责声明

GADTs 和 DataKinds 对我来说是未开发的领域,所以我不知道它们的一些限制和功能。

问题

因此,我正在为 JavaScript 代码发射器编写 AST,并且我已经确定了表达式之间的一个边缘情况,即它们可以是引用也可以不是引用。因此,我使用 GADTS 和数据类型来键入 JavaScript 表达式语义的这一方面。ast 看起来像这样。

表达式 AST 的子集

这看起来很好,很花哨,因为赋值表达式要求第一个表达式是引用,如属性表达式 ( "test".shadyProperty) 或引用/标识符。

问题

现在我想添加一个数组文字表达式,在 JavaScript 中,这个列表中的内容并不重要,所以像这样的列表是合法的

然而,在我的 AST 中,这是不合法的,因为列表中有多种类型

什么可以代替???类型?当我想为 JSObject 和 JSFunctionCall 构建一个构造函数时,也会出现类似的问题,因为它们也是表达式。

伊德里斯的灵魂

在伊德里斯???看起来像这样。

潜在的灵魂

包装类型

一种与 Idris 不同的灵魂,会拥有这样的包装器类型

这会使我图书馆的 api 变得粗糙,这不是我想要的。

总之

我正在寻找在 Idris 中找到的等价物,以及对解决方案含义的解释。如果没有等价物,那么下一个最好的解决方案就是我正在寻找的。

0 投票
2 回答
576 浏览

haskell - 如何为 DataKinds 派生类型自动派生 Typeable 实例?

我有一些这样的类型:

我想typeOf在这个函数中使用它们:

这不起作用,因为afindRate 中的类型没有Typeable实例。所以我通过这样做来修复它:

但是,当货币数量增加时,这将成为很多样板。有没有办法指定所有类型的种类Currency都应该派生一个Typeable实例?

编辑:另外,一种让它推断 in Money athe ais的Typeable方法会很好,所以我不需要在(Typeable a) =>任何地方添加。不过那是次要的。

0 投票
1 回答
317 浏览

dynamic - Fortran 动态整数类型

我想编写一段代码,它可以找到我机器的所有可用整数类型并打印所有它们的范围。找到种类并不是困难的部分,使用selected_int_kind我能够迭代所有可用的种类数,直到我得到一个 -1 值,表明编译器不再可以表示整数。

例如,此过程产生了一个可用种类编号的数组 (/ 1 2 4 8 16/)(这是我的 gfortran 编译器的结果)

下一步是使用这个数组来定义 5 种不同的整数,并询问最大可表示的整数是多少。我的想法是使用一个可分配的整数,并且每次都使用其他类型的参数来分配它,比如

但这对我不起作用。有没有人有这方面的经验?我认为可以做到,但我不知道该怎么做。