haskell - 如何为 GADT 实现棱镜？

Question

我有这样的 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

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

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

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

Answer 1

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

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

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

相反；然后你会发现翻译更容易。