如何为 GADT 编写遍历？答案

【问题标题】：How to write Traversal for GADT?如何为 GADT 编写遍历？
【发布时间】：2017-11-21 17:46:07
【问题描述】：

是否可以为 GADT 编写 Traversal？我有：

{-# LANGUAGE TypeInType, GADTs, TypeFamilies, RankNTypes #-}

module GADT where

import Data.Kind

data Tag = TagA | TagB

data family Tagged (tag :: Tag)

data Foo (tag :: Maybe Tag) where
    Foo       :: Int -> Foo Nothing
    FooTagged :: Int -> Tagged tag -> Foo (Just tag)

我想为Tagged tag 字段编写遍历。我试过了：

type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s

tagged :: forall mt t. Traversal' (Foo mt) (Tagged t)
tagged _  foo@(Foo         _) = pure foo
tagged fn foo@(FooTagged i t) = fmap (\t' -> FooTagged i t') (fn t)

但它失败了：

* Could not deduce: tag ~ t
      from the context: mt ~ 'Just tag
        bound by a pattern with constructor:
                   FooTagged :: forall (tag :: Tag).
                                Int -> Tagged tag -> Foo ('Just tag),
                 in an equation for `tagged'
        at gadt.hs:19:16-28
      `tag' is a rigid type variable bound by
        a pattern with constructor:
          FooTagged :: forall (tag :: Tag).
                       Int -> Tagged tag -> Foo ('Just tag),
        in an equation for `tagged'
        at gadt.hs:19:16-28
      `t' is a rigid type variable bound by
        the type signature for:
          tagged :: forall (mt :: Maybe Tag) (t :: Tag).
                    Traversal' (Foo mt) (Tagged t)
        at gadt.hs:17:1-53
      Expected type: Tagged t
        Actual type: Tagged tag
    * In the first argument of `fn', namely `t'
      In the second argument of `fmap', namely `(fn t)'
      In the expression: fmap (\ t' -> FooTagged i t') (fn t)
    * Relevant bindings include
        t :: Tagged tag (bound at gadt.hs:19:28)
        fn :: Tagged t -> f (Tagged t) (bound at gadt.hs:19:8)
        tagged :: (Tagged t -> f (Tagged t)) -> Foo mt -> f (Foo mt)
          (bound at gadt.hs:18:1)
   |
19 | tagged fn foo@(FooTagged i t) = fmap (\t' -> FooTagged i t') (fn t)
   |                                                                  ^

如果没有unsafeCoerce，我如何在FooTagged 的情况下证明mt ~ Just t？

更新：

使用类型族来指定遍历的焦点似乎有效：

type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s

type family TaggedType (m :: Maybe Tag) :: Type where
    TaggedType ('Just a) = Tagged a
    TaggedType 'Nothing  = ()

tagged :: forall mt. Traversal' (Foo mt) (TaggedType mt)
tagged _  foo@(Foo         _) = pure foo
tagged fn foo@(FooTagged i t) = fmap (\t' -> FooTagged i t') (fn t)

还有其他解决方案吗？

更新 2：

它可能应该是TaggedType 'Nothing = Void，而不是最后一个子句中的TaggedType 'Nothing = ()。

【问题讨论】：

为什么要保留mt ~ Just t？ forall mt t. Traversal' (Foo mt) (Tagged t) 类型表示这些事情完全是随意的。
@gallais 我应该如何重写tagged 类型如果我想mt ~ Just t 保持FooTagged 的情况？
注意：data family Tagged (tag :: Tag) 不是一个很有用的声明； Tagged 的实例必须是单个 data instance Tagged x where .. 或 data instance Tagged TagA where .. 和 data instance Tagged TagB where .. 中的一个或两个（通常，只有索引是封闭类型的数据系列没有用处）。

标签： haskell haskell-lens gadt

【解决方案1】：

这与AllowAmbiguousTypes 一起编译。不过，我对这段代码有点怀疑，因为我无法清楚地看到它是如何使用的。

type family FromMaybe (t :: Tag) (x :: Maybe Tag) :: Tag where
  FromMaybe _ (Just tag) = tag
  FromMaybe t _          = t  

tagged :: forall mt t. Traversal' (Foo mt) (Tagged (FromMaybe t mt))
tagged _  foo@(Foo         _) = pure foo
tagged fn foo@(FooTagged i t) = fmap (\t' -> FooTagged i t') (fn t)

【讨论】：