haskell - 你能在 Haskell 类型签名中组合参数化类型吗？

Question

我一直在尝试编写一个自定义光学数据结构来概括透镜、棱镜和遍历。我的数据结构如下所示:

data Optic m a b = Optic { view :: a -> m b
                         , over :: a -> (b -> b) -> a
                         }

我想编写一个包含两个 Optics 的函数，optic1::Optic m a b 和 optic2::Optic n b c 以生成包含 view::的 Optic a -> m (n c) 和 over::a -> (c -> c) -> a。

在我看来，这个组合的 Optic 的类型应该是 Optic (m n) a c，但这不起作用——GHC 会提示 m 有一个太多的类型参数，而 n 也有一个很少。

这是我对 compose 函数的非编译实现:

compose :: Optic m a b -> Optic n b c -> (m b -> (b -> n c) -> m (n c)) -> Optic (m n) a c
compose optic1 optic2 glue = Optic { view = viewCompose (view optic1) (view optic2) glue
                                   , over = overCompose (over optic1) (over optic2)
                                   }

viewCompose :: (a -> m b) -> (b -> n c) -> (m b -> (b -> n c) -> m (n c)) -> a -> m (n c)
viewCompose view1 view2 glue x = glue (view1 x) view2

overCompose :: (a -> (b -> b) -> a) -> (b -> (c -> c) -> b) -> a -> (c -> c) -> a
overCompose over1 over2 x f = over1 x (\y -> over2 y f)

GHC 错误信息是:

optic.hs:7:83: error:
    • Expecting one fewer argument to ‘m n’
      Expected kind ‘* -> *’, but ‘m n’ has kind ‘*’
    • In the first argument of ‘Optic’, namely ‘m n’
      In the type signature:
        compose :: Optic m a b
                   -> Optic n b c -> (m b -> (b -> n c) -> m (n c)) -> Optic (m n) a c

optic.hs:7:85: error:
    • Expecting one more argument to ‘n’
      Expected a type, but ‘n’ has kind ‘* -> *’
    • In the first argument of ‘m’, namely ‘n’
      In the first argument of ‘Optic’, namely ‘m n’
      In the type signature:
        compose :: Optic m a b
                   -> Optic n b c -> (m b -> (b -> n c) -> m (n c)) -> Optic (m n) a c

如果我创建一个 Optic Maybe Int Int 类型的 optic，GHC 会理解第一个类型参数的类型是 * -> * 并且不会提示参数不足.但我不知道如何将类型组合在一起以创建另一种类型 * -> *。

是否有任何方式(有或没有语言扩展)来表达类似的东西:

Optic (forall t. m (n t)) a c

Answer 1

根据@chi 的评论，Haskell 不直接支持类型级别的 lambda。因此，虽然存在一个名为 Maybe 的类型 * -> * ，它直接表示类型级别的 lambda \a ~> Maybe a , 没有对应的类型直接表示类型级 lambda \a ~> Maybe (Maybe a).

这意味着给定您为字段 view 定义的类型:

view :: a -> m b

不可能为任何类型的 m 找到满足以下条件的光学 Optic m a b:

view :: a -> Maybe (Maybe b)  -- impossible

您必须为这些类型使用一些 编码。从 Data.Functor.Compose 导入的 Compose 新类型是一种替代方法。它的定义是:

newtype Compose m n a = Compose (m (n a))

它基本上将没有直接 Haskell 表示的类型 lambda \a ~> m (n a) 包装成类型 lambda \a ~> (Compose m n) a 其直接的 Haskell 表示很简单 Compose m n : * -> *。

缺点是它会在您的类型中引入不均匀性——会有“普通”光学器件，如 Optic Maybe Int Int，然后是“复合”光学器件，如 Optic (Compose Maybe Maybe) Int Int。在大多数情况下，您可以使用 coerce 来解决这个不便。

使用 Compose 新类型的 compose 的适当定义类似于:

type Glue m n b c = m b -> (b -> n c) -> m (n c)

compose :: Optic m a b -> Optic n b c -> Glue m n b c -> Optic (Compose m n) a c
compose optic1 optic2 glue
  = Optic { view = viewCompose (view optic1) (view optic2) glue
          , over = overCompose (over optic1) (over optic2)
          }
  where
    viewCompose view1 view2 glue x = Compose $ glue (view1 x) view2
    overCompose over1 over2 x f = over1 x (\y -> over2 y f)

对于典型的基于可能的光学器件:

_Left :: Optic Maybe (Either a b) a
_Left = Optic v o
  where v (Left x) = Just x
        v (Right _) = Nothing
        o (Left x) f = Left (f x)
        o (Right y) _ = Right y

合成的光学器件可能看起来像:

_Left2 = compose _Left _Left (flip fmap)

直接使用它会引入一个Compose包装器:

> view _Left2 (Left (Left "xxx"))
Compose (Just (Just "xxx"))

但您可以强制结果以避免显式解包，如果有多个嵌套的Compose 层则特别有用:

λ> import Data.Coerce
λ> _Left4 = compose _Left2 _Left2 (flip fmap)
λ> :t _Left4
_Left4
  :: Optic
       (Compose (Compose Maybe Maybe) (Compose Maybe Maybe))
       (Either (Either (Either (Either c b4) b5) b6) b7)
       c
λ> view _Left4 (Left (Left (Left (Left True))))
Compose (Compose (Just (Just (Compose (Just (Just True))))))
λ> coerce $ view _Left4 (Left (Left (Left (Left True)))) :: Maybe (Maybe (Maybe (Maybe Bool)))
Just (Just (Just (Just True)))

完整代码:

import Data.Coerce
import Data.Functor.Compose

data Optic m a b = Optic { view :: a -> m b
                         , over :: a -> (b -> b) -> a
                         }

type Glue m n b c = m b -> (b -> n c) -> m (n c)

compose :: Optic m a b -> Optic n b c -> Glue m n b c -> Optic (Compose m n) a c
compose optic1 optic2 glue
  = Optic { view = viewCompose (view optic1) (view optic2) glue
          , over = overCompose (over optic1) (over optic2)
          }
  where
    viewCompose view1 view2 glue x = Compose $ glue (view1 x) view2
    overCompose over1 over2 x f = over1 x (\y -> over2 y f)

_Left :: Optic Maybe (Either a b) a
_Left = Optic v o
  where v (Left x) = Just x
        v (Right _) = Nothing
        o (Left x) f = Left (f x)
        o (Right y) _ = Right y

_Left2 :: Optic (Compose Maybe Maybe) (Either (Either c b1) b2) c
_Left2 = compose _Left _Left (flip fmap)

_Left4 :: Optic (Compose (Compose Maybe Maybe) (Compose Maybe Maybe)) (Either (Either (Either (Either c b1) b2) b3) b4) c
_Left4 = compose _Left2 _Left2 (flip fmap)

main = do
  print $ view _Left4 (Left (Left (Left (Left True))))
  print $ (coerce $ view _Left4 (Left (Left (Left (Left True)))) :: Maybe (Maybe (Maybe (Maybe Bool))))