GADT的Traversal怎么写？

Question

是否可以为 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 = ()。

Answer 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)

GADT的Traversal怎么写？

How to write Traversal for GADT?

haskell

haskell-lens

gadt