haskell - 如何为GADT实现棱镜？

我有这样的GADT数据类型:

data TValue = TInt | TBool

data Value (t :: TValue) where
    I :: Int  -> Value 'TInt
    B :: Bool -> Value 'TBool

我想在此数据类型上具有用于模式匹配的棱镜。为了简化起见，我使用数据棱镜方法。所以以前我有这样的事情:

data ValuePrism (tag :: TValue) a = ValuePrism
    { matchValue :: forall t . Value t -> Maybe a
    , buildValue :: a -> Value tag
    }

boolPrism :: ValuePrism 'TBool Bool
boolPrism = ValuePrism matchBool B
  where
    matchBool :: Value t -> Maybe Bool
    matchBool (B b) = Just b
    matchBool _     = Nothing

我想将此用例放入棱镜界面。我可以通过以下方式指定类型:

data Prism s t a b = Prism
    { preview :: s -> Either t a
    , review  :: b -> t
    }

type ValuePrism (tag :: TValue) a =
    forall t . Prism (Value t) (Value tag) a a

但是我无法编写根据旧接口创建ValuePrism的函数:

mkValuePrism :: (forall t . Value t -> Maybe a)
             -> (a -> Value tag)
             -> ValuePrism tag a
mkValuePrism = =<< (ツ) >>=

有什么方法可以为GADT创建棱镜吗？

最佳答案

您需要更改ValuePrism的第二个定义。

您的第一个ValuePrism 'TBool Bool不包含Bool -> Value 'TInt类型的函数，但是您的第二个ValuePrism 'TBool Bool包含(通过将forall'd t专门化为'TInt并调用review)。这样的功能可以从头开始，但是一定是我所说的“不合理”。您可以定义

type ValuePrism tag a = Prism (Value tag) (Value tag) a a

代替;然后，您会发现翻译变得容易得多。

关于haskell - 如何为GADT实现棱镜？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/50948583/