【问题标题】：Haskell Data.Type.Equality "Not in scope: data constructor ‘:~:’"Haskell Data.Type.Equality “不在范围内：数据构造函数‘:~:’”
【发布时间】：2017-03-17 19:59:14
【问题描述】：

我是第一次尝试使用 GADT，我想实现变量替换。当然，我只能在类型相等的情况下进行替换。据我了解，这应该可以使用 Data.Type.Equality 中的 :~: 来实现。但不知何故，编译器根本不希望我使用:~:。为了尝试一下，我编写了以下愚蠢的函数。

lol :: Int -> Int -> Bool
lol a b = case a :~: b of
  Refl -> True
  _    -> False

编译器告诉我：

Not in scope: data constructor ‘:~:’

我尝试了以下方法：

首先，我认为这是安装了错误版本的问题。我看到 :=: 在旧版本中使用。但是 :=: 也没有用。
我将 cabal 文件中的 base 版本显式更改为 4.8.1.0，但仍然没有运气。
我将 Data.Type.Equality 的整个源代码复制到一个名为 TypeEquality 的单独文件中并导入。还是一样的错误信息。
我认为这可能与我需要启用的某些扩展有关。我启用了 Data.Type.Equality 使用的所有扩展，除了 NoImplicitPrelude。还是没有运气。
我将所有内容都复制到了我使用它的同一个文件中。还是一样的错误信息。
我尝试用谷歌搜索其他使用此模块的人。我找不到任何有用的东西。无论如何，这会很好，因为我还不太了解如何使用它。
我寻找“不在范围内”的其他 StackOverflow 问题。我没有查看所有这些，但似乎它总是与大写/小写问题有关，这在我的情况下似乎不是问题。

在尝试了所有我想到的并且在情绪崩溃之前不久，我决定在这里问这个问题。有人知道我的问题可能是什么吗？可能您需要其他信息来诊断它，所以请告诉我我能提供的任何信息。由于是一个很大的项目，我觉得提供完整的源代码没有用...

编辑

好吧，看来我完全误解了 :~: 的工作方式。所以我把这个问题完全改写成我真正需要的：

-- a is a variable symbol used for variable substitution.
-- b is a function symbol used for function substitution.
-- c represents a type of value that is contained.
data Ast a b c where
  BoolConst :: Bool -> Ast a b Bool
  IntConst :: Int -> Ast a b Int
  Var :: Eq a => a -> c -> Ast a b c
  -- Function application for a function with symbol b.
  App :: (Eq b, Eq c) => b -> Ast a b c -> Ast a b Int
  UnOp :: UnaryOperator c d -> Ast a b c -> Ast a b d
  BinOp :: BinaryOperator c d e -> Ast a b c -> Ast a b d -> Ast a b e
  NaryOp :: NaryOperator c -> [Ast a b c] -> Ast a b c
  Ite :: Ast a b Bool -> Ast a b c -> Ast a b c -> Ast a b c

我省略了运算符的定义，但你可以想象。首先：据我了解，实现具有多个参数的函数是不可能的。所以我将 App 实现为只接受一个参数而不是一个列表，并通过以某种方式重复应用它来模拟多个参数。我仍然需要进行一些更改才能使其正常工作，但这不是这里的问题。

现在我想写两个substituteVar 和substituteFunc 函数来替代变量和函数。为简单起见，现在让我们关注substituteVar。我想使用以下签名：

substituteVar :: Eq a => M.Map a (Ast a b c) -> Ast a b d -> Ast a b d

类型参数c和d基本都是作为返回类型使用的。但是我不知道如何处理 Haskell 不“知道”替换 c 的类型是否与遇到的变量 d 的类型相同的问题。所以我想我可以以某种方式使用:~:，但我想我错了。顺便说一句，我目前只需要 Bool 和 Int 类型，但我希望它可以扩展更多（但数量仍然很少）。

我知道可以为变量使用两个构造函数BoolVar 和IntVar。但是虽然这有点难看，但对变量很有效，即使我将它扩展到 5 种类型，对于函数来说也会变得非常混乱。我基本上需要一个类型构造函数，每个参数和返回类型的组合。因此，我认为该解决方案无法扩展，并且感觉应该有更简单的可能性。

【问题讨论】：

你import Data.Type.Equality了吗？
是的，我做到了。无论如何，即使我没有，在我将源代码复制到我想使用它的同一个文件之后，它也应该可以工作。
:~: 是一个类型运算符 - 它对类型进行操作，因此 case a :~: b of ... 没有任何意义，因为 case ... of ... 按条款工作。
哦，好的。然后我完全误解了 :~: 的作用。好的。所以我需要重新考虑一下。
语法是case Refl :: (Int :~: Int) of Refl -> True，但这不是很有用，因为你可以在这里看到Int和Int是一样的！我非常怀疑您是否需要Data.Type.Equality 来做您想做的事情；我认为你应该退后一步，问一个关于你真正想要做什么的问题（你认为Data.Type.Equality 是解决方案的问题）

标签： haskell

【解决方案1】：

好的，这是迄今为止我在 Stackoverflow 上最愚蠢的问题。我想删除它，但也许有一天有人在谷歌上搜索同样的问题并且很高兴看到答案，因此我会回答它。

回答我原来的问题

我完全误解了:~: 运算符。它适用于类型而不是术语，因此我的示例没有意义。

关于我的第二个问题

我没有答案，但我不再需要它了。我喜欢 GADT 的想法，但我试图将它应用到它们非常难以使用的地方。可能一个更有经验的 Haskell 程序员能够在我的上下文中正确使用它们，但我绝不是一个优秀的 Haskell 程序员。所以我将只使用普通的 ADT 并放弃一些类型安全，即编译器不会禁止布尔值等的乘积。但作为交换，我实际上可以让它工作。

此外，完全改变我的问题是一种非常糟糕的风格。小的改编是可以的，但如果方向完全改变，我应该创建一个带有适当标题的单独问题。当前状态对于登陆此页面的每个人来说都是令人困惑的。此外，作为一个具有适当标题的单独问题，我将有更好的机会得到一个好的答案。

【讨论】：