haskell - 如何在 GADT 中使用受限约束？

Question

我有以下代码，我希望这不能通过类型检查:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

import Control.Lens

data GADT e a where
  One :: Greet e => String -> GADT e String
  Two :: Increment e => Int -> GADT e Int

class Greet a where
  _Greet :: Prism' a String

class Increment a where
  _Increment :: Prism' a Int

instance Greet (Either String Int) where
  _Greet = _Left

instance Increment (Either String Int) where
  _Increment = _Right

run :: GADT e a -> Either String Int
run = go
  where
  go (One x) = review _Greet x
  go (Two x) = review _Greet "Hello"

这个想法是 GADT 中的每个条目都有一个相关的错误，我正在使用 Prism 对其进行建模。进入一些更大的结构。当我“解释”这个 GADT 时，我为 e 提供了一个具体类型。具有所有这些 Prism 的实例s。但是，对于每个单独的情况，我不希望能够使用未在构造函数的关联上下文中声明的实例。

上面的代码应该是一个错误，因为当我在 Two 上进行模式匹配时我应该知道我只能使用 Increment e ，但我使用的是 Greet .我明白为什么会这样 - Either String Int有 Greet 的实例，所以一切都检查出来了。

我不确定解决此问题的最佳方法是什么。也许我可以使用 Data.Constraint 的蕴涵，或者也许有更高等级类型的技巧。

有任何想法吗？

Answer 1

问题是您正在修复最终结果类型，因此实例存在并且类型检查器可以找到它。

尝试类似:

run :: GADT e a -> e

现在结果类型无法选择 review 的实例参数化强制执行您的不变量。