Can you compose parameterised types in Haskell type signatures?

Question

I've been trying to write a custom Optics data structure that generalises Lenses, Prisms and Traversals. My data structure looks like this:

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

I want to write a function that composes two Optics, optic1 :: Optic m a b and optic2 :: Optic n b c to produce an Optic containing view :: a -> m (n c) and over :: a -> (c -> c) -> a.

In my head, the type of this composed Optic would be Optic (m n) a c, but this doesn't work - GHC will complain that m has one too many type arguments and n one too few.

Here's my non-compiling implementation of the compose function:

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)

The GHC error messages are:

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

If I create an optic of type Optic Maybe Int Int, GHC understands that the first type argument has kind * -> * and doesn't complain about insufficient arguments. But I can't figure out how to combine types together to create another type of kind * -> *.

Is there any way (with or without language extensions) to express something like:

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

Answer 1

As per @chi's comment, Haskell doesn't directly support type-level lambdas. So, while there exists a type named Maybe of kind * -> * which directly represents the type-level lambda \a ~> Maybe a, there's no corresponding type directly representing the type-level lambda \a ~> Maybe (Maybe a).

This means that given your defined type for the field view:

view :: a -> m b

it is impossible to find an optic Optic m a b for any type m that would satisfy:

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

You must instead use some kind of encoding for these types. The Compose newtype imported from Data.Functor.Compose is one alternative. It's definition is:

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

It basically wraps up the type lambda \a ~> m (n a) which has no direct Haskell representation into a type lambda \a ~> (Compose m n) a whose direct Haskell representation is simply Compose m n : * -> *.

The drawback is that it will introduce a non-uniformity in your types -- there'll be "plain" optics like Optic Maybe Int Int and then "composed" optics, like Optic (Compose Maybe Maybe) Int Int. You can use coerce to work around this inconvenience in most cases.

The appropriate definition of compose using the Compose newtype would look something like:

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)

and for a typical Maybe-based optic:

_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

a composed optic might look like:

_Left2 = compose _Left _Left (flip fmap)

Using it directly will introduce a Compose wrapper:

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

but you can coerce the result to avoid explicit unwrapping, particularly helpful if there are multiple nested Compose layers:

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

The full code:

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