我有以下代码,我希望这不能通过类型检查:
{-# 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
的蕴涵,或者也许有更高等级类型的技巧。有任何想法吗?
最佳答案
问题是您正在修复最终结果类型,因此实例存在并且类型检查器可以找到它。
尝试类似:
run :: GADT e a -> e
现在结果类型无法选择
review
的实例参数化强制执行您的不变量。
关于haskell - 如何在 GADT 中使用受限约束?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/23365220/