你能在Haskell类型签名中使用参数化类型吗？

Question

我一直在尝试编写一个自定义的Optics数据结构，它可以泛化Lenses、Prisms和Traversals。我的数据结构长这样：

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

我想编写一个函数来组合两个“Optic”，optic1 :: Optic m a b 和 optic2 :: Optic n b c，以生成包含 view :: a -> m (n c) 和 over :: a -> (c -> c) -> a 的“Optic”。在我的脑海中，这个组合的“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的光学对象，那么GHC会理解第一个类型参数具有* -> *的类型，并且不会因为参数不足而抱怨。但是我不知道如何将类型组合在一起，以创建另一种* -> *类型。

是否有任何方法（带或不带语言扩展）可以表达类似以下内容的东西：

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

- anundermone

---

为什么没有扩展名？ - Fyodor Soikin

如果使用Compose，它是否有效？也就是说，Optic (Compose m n) a c。 - bradrn

Compose 会使得 view :: a -> Compose m n c，而不是 OP 所需的 view :: a -> m (n c)。 - Fyodor Soikin

我认为Compose是最接近的选择。Haskell不允许类型级别的lambda，因为在类型推断的许多点上它假定单射性，这是由于我们有_类型名称_而不是_类型函数_，粗略地说（也请参见名义与结构类型）。 - chi

感谢您的纠正@FyodorSoikin - 我完全忽略了这一点！ - bradrn

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 是一种选择。它的定义如下：

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)

对于一个典型的基于Maybe的光学器：

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

- K. A. Buhr