鉴于下面的代码在其中查找类型的特定于类型的信息Data.HashMap，是否可以定义getMapVal2注释中记录的新函数，以构建TypeKey给定类型的参数？

这只是一个玩具代码，用于测试在运行时通过类型特定配置传递Data.HashMap给作用于类型类类型的多态函数。

语境

我正在尝试实现一个与 IBM 的 OLP（线性编程建模语言）松散相似的 EDSL。

代码

Haskell EDSL 代码

EDSL 与 OPL 比较

对应opl码

相关部分

也

问题描述

OPL 使用括号进行数组订阅，我尝试使用以下符号将订阅映射到我的 EDSL

这在以下意义上对应于 OPL：

在前者中， (Id "p" :+ Id "f" :+ Nil) 构造一个 Vector 类型的值，其中包含有关所述向量长度的类型级别信息。根据构造函数:?的定义，可以看到，Iterate(n)[] Double 会展开为[[Double]]。这可以按预期巧妙地工作。然而，反过来使用生成的语法树，我需要对实际值进行模式匹配。

问题：以上行有效，但我不知道如何使用实际数据。如何进行模式匹配？无论如何都可以使用数据吗？通过明显的替换dbl

不起作用。我还尝试建立一个数据系列，但我无法找到一种方法来递归地创建一个包含所有任意嵌套的 Double 列表的系列：

我正在尝试阅读servant库的教程，这是一个类型级的Web DSL。该库广泛使用语言扩展。DataKind

在该教程的早期，我们发现以下行定义了 Web 服务端点：

我不明白在类型签名中包含字符串和数组意味着什么。我也不清楚'前面的勾号（）是什么意思'[JSON]。

所以我的问题归结为字符串和数组的类型/种类是什么，当它变成 WAI 端点时如何解释？

作为旁注，在描述时的一致使用Nat给Vect我们DataKinds留下了一组令人沮丧的有限示例，以便在尝试理解这些内容时查看。我想我已经在不同的地方至少读过这个例子十几次了，但我仍然觉得我不明白发生了什么。

我正在尝试做一些高级类型级编程；该示例是我原始程序的简化版本。

我有（Haskell）类型的表示。在这个例子中，我只介绍了函数类型、基本类型和类型变量。

该表示Type t由一个类型变量参数化，t以允许在类型级别上进行区分。为此，我主要使用 GADT。不同的类型和类型变量通过使用类型级文字来区分，因此KnownSymbol约束和使用Proxys。

我还通过使用 DataKinds 和 KindSignatures 扩展并定义数据类型t来限制类型：TypeKindTypeKind

现在我想实现类型变量的替换，即在一个 type 中用 type 替换每个t等于xtype variable 的变量。替换必须在表示以及类型级别上实现。对于后者，我们需要 TypeFamilies：yt'

类型变量是有趣的部分，因为我们检查符号的相等性x和y类型级别。为此，我们还需要一个（多类）类型族，它允许我们在两个结果之间进行选择：

不幸的是，这还没有编译，这可能是我的问题的第一个指标：

但是，启用 UndecidableInstances 扩展是可行的，因此我们继续定义一个subst在值级别上工作的函数：

这段代码运行良好，除了最后一行产生以下编译错误：

我想问题在于我无法证明两个符号x和y的类型的不等式，并且需要某种类型不等式的见证。这可能吗？还是有其他更好的方法来实现我的目标？我不知道“惯用的”Haskell 类型不等式问题和GADT 可用于证明 GHC 中的类型不等式在多大程度上？已经回答了我的问题。任何帮助，将不胜感激。

人们常说

在“我们可以使用这些术语来执行测试布尔值的真实性的操作”的意义上表示 True 和 False。

但这隐藏了一个重要的警告，因为它似乎只在无类型的 lambda 演算中是正确的。如果我只是将这些值插入haskell，我可以编写一个函数：

它在类型级别区分 tru 和 fls。这么说是多么错误/真实：

• 在 STLC中tru，fls是一些提升'Boolean类型的价值级别见证，它有类型'True和'False
• 在 STLC 中（强制）类型值(tru :: ∀ t . t → t → t)并(fls :: ∀ t . t → t → t)表示 True 和 False（并且在未类型化中，通常情况下）

编辑：我现在意识到感谢@Daniel Wagner 的回答，我在我的问题中考虑的是二阶 Lambda 微积分而不是 STLC。

我一直在努力在 Haskell 中构建自己的外交模拟器来弄湿我的脚。

我相信我已经对什么是订单提出了一个不错的定义：

对于那些不熟悉游戏的人，命令以“保持伦敦舰队”、“移动伦敦英吉利海峡舰队”、“支援英吉利海峡舰队北大西洋中大西洋舰队”或“护航舰队英吉利海峡军队”的形式写成伦敦布雷斯特”等。

现在，将 Unit 定义为data Unit = Fleet | Army (deriving Eq, Show)，我得到了Not in scope: type constructor or class 'Fleet'关于 Order 定义的错误。

为什么是这样？

我应该如何编写单位或命令的定义（或者我应该做一些不同的事情），以允许我要求 Convoy 的第一个参数是舰队，第三个参数是陆军？

我对这个问题的处理方法“甚至没有错”吗？

我是否应该在我的验证功能中处理这个问题（因为据我所知，没有办法通过 Haskell 仅指定有效订单。它具有表现力但不具有表现力）？

我已经尝试过使用“DataKinds”，但这对我没有任何帮助（尽管错误后记建议这样做，但 Haskell 错误后记再次提出了很多建议，所以我怀疑我需要过多注意它）。

我最近开始搞乱DataKinds，以便为算术提供编译时科学单位。我或多或少想出了一种方法来做我想做的事，但我觉得它可能会更干净。

我需要可能为负数（m^-1）的整数，所以我决定使用整数而不是自然数。但事实证明，当你这样做时，:k 5它会给你GHC.Types.Nat带来不符合我需求的东西。我最终改为制作自己的自定义代数整数类型。以及定义与它一起使用的加法和减法类型系列。

但这一切似乎都非常间接，似乎没有充分的理由我不能直接使用所有现有函数在编译时在类型族中操作数据。

基本上我希望基本上自动生成以下内容：

这可能吗，如果没有，那为什么不呢？

还有一种简单的方法可以从类型中获取运行时值吗？特别是在为所有这些类型编写Show实例时，我基本上只想引入表示单元组合的幻像类型并将其转换为字符串。我现在能想到的所有方法似乎都非常冗长。

假设我们有一个类型构造函数 f，它通过一个 DataKinds-promoted 对来接受两种类型。

然后我可以实现一个函数，forward就像量词一样：curryforall

但是，反向功能是有问题的：

GHC 8.0.1 给出错误消息：

从概念上讲，它似乎是一个有效的程序。有没有另一种方法来实现这个功能？或者这是 GHC 的已知限制？

我有这个异构列表，它的类型反映了它包含的值的类型。我可以通过检查包含的每种类型是否满足约束来将所有元素转换为字符串：

我想做的是通过类型级关联列表指定一些额外的信息，该列表由 HList 中的类型索引。就像是：

现在，可以清楚地看到 if(Keys keyMap)是非空的，然后keyMap，但 GHC 很难弄清楚这一点：

我怎样才能重写它以便 GHC 可以解决问题？

我正在为消息队列编写一个库。队列可以是Direct或Topic。Direct队列有一个静态绑定键，而Topic队列可以有动态键。

我想编写一个publish仅适用于Direct队列的函数。这有效：

这需要两个单独的构造函数

但是当我去写发布时，我需要匹配一个额外的模式，这应该是不可能的

有没有更好的方法来模拟这个问题，这样我就不需要模式匹配了？Direct队列应始终具有该Text元数据，并且Topic队列应始终具有该[Text]元数据。有没有更好的方法在类型和值级别上执行此操作？