Abstraction over profunctor optics' kinds

AbstractOptic.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}

import Data.Data

class OpticKind k where
  -- This definition would give us injectivity with respect to s, t, a, b
  -- but it doesn't allow to write @Base OKGetter s t a b = s -> a@, since
  -- there is no lambdas on type level and type synonyms can't be partially
  -- applied:
  --
  -- type Base k :: Type -> Type -> Type -> Type -> Type
  --
  -- This definition would also be better (though not so clear), but also is
  -- impossible now:
  --
  -- type Base k s t a b = r | (k, r) -> s, (k, r) -> t, (k, r) -> a, (k, r) -> b
  type Base k s t a b
  trivOptic :: Base k a b a b

newtype OpticP k a b s t = OpticP { runOpticP :: Base k s t a b }

type AnOptic k s t a b = OpticP k a b a b -> OpticP k a b s t

runOptic :: forall k s t a b. OpticKind k => AnOptic k s t a b -> Base k s t a b
runOptic = runOpticP . ($ OpticP (trivOptic @k @a @b))

class OpticKind k => OpticC k p where
  opticOp :: Base k s t a b -> p a b -> p s t

type Optic k s t a b = forall p. OpticC k p => p a b -> p s t

optic :: forall k s t a b. OpticKind k => Base k s t a b -> Optic k s t a b
optic = opticOp @k

class (OpticKind k1, OpticKind k2) => Is k1 k2 where
  comp :: Proxy (k1, k2, s, t, a, b, u, v)
    -> Base k1 s t a b -> Base k2 a b u v -> Base k2 s t u v

-- This looks awful since we don't know that "Base k1" is a normal type =>
-- is injective. See also comment to "Base" definition
instance forall k1 k2 u v. (Is k1 k2) => OpticC k1 (OpticP k2 u v) where
  opticOp :: forall s t a b. Base k1 s t a b -> OpticP k2 u v a b -> OpticP k2 u v s t
  opticOp b1 p2 = OpticP $
    comp (Proxy @(k1, k2, s, t, a, b, u, v)) b1 (runOpticP p2)

store :: (Is k k) => Optic k s t a b -> AnOptic k s t a b
store = id

clone :: forall k s t a b. AnOptic k s t a b -> Optic k s t a b
clone = optic @k . runOptic

-- Getter

data OKGetter

instance OpticKind OKGetter where
  type Base OKGetter s t a b = s -> a
  trivOptic = id

instance Is OKGetter OKGetter where
  comp _ sa au = au . sa

type AGetter s t a b = AnOptic OKGetter s t a b

view :: AGetter s t a b -> s -> a
view = runOptic

type Getter s t a b = Optic OKGetter s t a b

getter :: (s -> a) -> Getter s t a b
getter = optic @OKGetter

storeGetter :: Getter s t a b -> AGetter s t a b
storeGetter = store

cloneGetter :: AGetter s t a b -> Getter s t a b
cloneGetter = clone

-- Lens

data OKLens

instance OpticKind OKLens where
  type Base OKLens s t a b = (s -> a, s -> b -> t)
  trivOptic = (id, const id)

instance Is OKLens OKLens where
  comp _ (sa, sbt) (au, avb) = (au . sa, \s v -> sbt s $ avb (sa s) v)

instance Is OKLens OKGetter where
  comp _ (sa, sbt) au = au . sa

type ALens s t a b = AnOptic OKLens s t a b

viewAndSet :: ALens s t a b -> (s -> a, s -> b -> t)
viewAndSet = runOptic @OKLens

type Lens s t a b = Optic OKLens s t a b

lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
lens = curry (optic @OKLens)

storeLens :: Lens s t a b -> ALens s t a b
storeLens = store

cloneLens :: ALens s t a b -> Lens s t a b
cloneLens = clone

-- Here I use primitive combinators instead of synonyms 'Lens', 'lens' etc.
-- to make it more clear how it works

_1 :: Optic OKLens (a, a') (b, a') a b
_1 = optic @OKLens (fst, \(_, a') b -> (b, a'))

-- >>> runOptic @OKGetter _1 (True, 'x')
-- True

{-
  runOptic @OKGetter _1 (True, 'x')
    ≡ runOpticP (_1 $ OpticP (trivOptic @OKGetter)) (True, 'x')
    ≡ runOpticP (optic @OKLens (fst, \(_, a') b -> (b, a'))
                  $ OpticP (trivOptic @OKGetter)
                ) (True, 'x')
    ≡ runOpticP (OpticP $
                  comp
                    Proxy
                    (fst, \(_, a') b -> (b, a'))
                    (trivOptic @OKGetter)
                ) (True, 'x')
    ≡ runOpticP (OpticP $
                  comp
                    _
                    (fst, \(_, a') b -> (b, a'))
                    id
                ) (True, 'x')
    ≡ runOpticP (OpticP $
                  id . fst
                ) (True, 'x')
    ≡ (id . fst) (True, 'x')
    ≡ True
-}