MiniIndexedOptics.hs

{-

Problem: Talk.pdf says "This just works, because our Lens type isn’t polymorphic"

But it's not true. The true 'Lens' type in current @optics@ is

    forall i. Lens i s t a b

i.e. we __have__ leave it free. Not good.
(We can set it to () or Void, to put into container,
 but then we cannot compose with those optics)

Also the double indices __leak__ the implementation details. Not good either.


Solition: We can cure this, with some additional hackery.
And we can make CheckIndices less hacky, as it would only match on type level list!
I only comment the parts which are changed.

The idea is to use 

    newtype Optic (k :: OptikKind) (is :: [Type) s t a b
        Optic (forall p i. Constraints k p => p i a b -> p (Curry is i) s t)

abstract interface. I.e. move the first (of double indices) to be inside the
Optic.

Note: The implementation is still a compromise.
- A_Setter has always empty index list
- An_IxSettter has always non empty index list
But we are forced to it this way so Constraints reduce properly.  i.e. we can
`sub` Setter into IxSetter, but it would be unusable (as it would have empty
index list.

We can use CheckIndices (and CheckNonIndices if we like) to get better errors.
I think latter is not needed as library doesn't give means to construct
non-indexed optic with non-empty index-list.

More elegantly we'd only have `A_Setter` and differentiate
between indexed and non-indexed variants based on index-list.
But then the type-checker will fight back.

- Making Constraints (k :: OpticKind) (is :: [*]) p breaks `Is` implementation:
  in implies `is` is rigid, so type-family cannot match on it (or we need more
  proofs)

- Using `Constraints An_Traversal p = IxTraversing p`
  but then e.g. `over` would need to be implemented using `IxFunArrow`,
  e.g. passing some dummy index value. Not good.

-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module MiniIndexedOptics where

import Data.Functor.Identity
import Data.Kind (Type)
import Data.Type.Equality
import Data.Proxy (Proxy (..))

import GHC.Exts (Constraint)
import GHC.TypeLits

-------------------------------------------------------------------------------
-- Optics.Internal.Types
-------------------------------------------------------------------------------tr

-- Here: _No_ changes.

-- TODO: Add A_Getter and A_Setter
data OpticKind
    = An_Iso
    | A_Lens

    | An_IxSetter

type family Constraints (k :: OpticKind) (p :: * -> * -> * -> *) where
    Constraints 'An_Iso p = Profunctor p
    Constraints 'A_Lens p = Strong p
    Constraints 'An_IxSetter p = p ~ IxFunArrow

-------------------------------------------------------------------------------
-- Optics.Internal.Type.List
-------------------------------------------------------------------------------

-- This is new.
--
-- Append is very simple class which provides witness
--
--    foldr f (foldr f init xs) ys = foldr f init (ys ++ xs)
--
-- In real implementation, i'd replace Append with type-family
-- and use unsafeCoerce instead of matching on Refl.
-- The only place this witness is needed is in (%%)
-- 

type family Curry (xs :: [*]) (y :: *) :: * where
    Curry '[]       y = y
    Curry (x ': xs) y = x -> Curry xs y

class Append (xs :: [Type]) (ys :: [Type]) (zs :: [Type]) | xs ys -> zs where
    appendProof :: Proxy i -> Curry xs (Curry ys i) :~: Curry zs i
           
instance Append '[] ys ys where
    appendProof _ = Refl

instance Append xs ys zs => Append (x ': xs) ys (x ': zs) where
    appendProof :: forall i. Proxy i -> Curry (x ': xs) (Curry ys i) :~: Curry (x ': zs) i
    appendProof i = case appendProof @xs @ys @zs i of
        Refl -> Refl

-------------------------------------------------------------------------------
-- Optics.Internal.Subtyping
-------------------------------------------------------------------------------

class Is (k :: OpticKind) (l :: OpticKind) where
    implies :: proxy k l p -> (Constraints k p => r) -> (Constraints l p => r)

instance Is k k where
    implies _ = id

instance Is 'An_Iso 'A_Lens      where implies _ = id
instance Is 'An_Iso 'An_IxSetter where implies _ = id
instance Is 'A_Lens 'An_IxSetter where implies _ = id

type family Join (k :: OpticKind) (l :: OpticKind) :: OpticKind where
  Join 'An_Iso 'An_Iso = 'An_Iso
  Join 'An_Iso 'A_Lens = 'A_Lens
  Join 'A_Lens 'An_Iso = 'A_Lens
  Join 'A_Lens 'A_Lens = 'A_Lens

  Join 'An_IxSetter a = 'An_IxSetter
  Join a 'An_IxSetter = 'An_IxSetter

-------------------------------------------------------------------------------
-- Optics.Internal.Optic
-------------------------------------------------------------------------------

newtype Optic (k :: OpticKind) (is :: [Type]) s t a b =
    Optic { getOptic :: forall p i. Optic_ k p i (Curry is i) s t a b }

type Optic' k is s a = Optic k is s s a a

type Optic_ k p i o s t a b = Constraints k p => Optic__ p i o s t a b

type Optic__ p i o s t a b = p i a b -> p o s t

data IsProxy (k :: OpticKind) (l :: OpticKind) (p :: * -> * -> * -> *) = IsProxy

sub :: forall k l is s t a b . Is k l => Optic k is s t a b -> Optic l is s t a b
sub (Optic o) = Optic (implies' o)
  where
    implies' :: forall p i. Optic_ k p i (Curry is i) s t a b -> Optic_ l p i (Curry is i) s t a b
    implies' x = implies (IsProxy :: IsProxy k l p) x

(%) :: (Is k m, Is l m, m ~ Join k l, Append is js ks)
    => Optic k is s t u v
    -> Optic l js u v a b
    -> Optic m ks s t a b
o % o' = sub o %% sub o'
{-# INLINE (%) #-}

-- Here we need to prove things. Wiht unsafeCoerce many headaches will go away.
(%%) :: forall k is js ks s t u v a b. Append is js ks
     => Optic k is s t u v
     -> Optic k js u v a b
     -> Optic k ks  s t a b
Optic o %% Optic o' = Optic oo
  where
    oo :: forall p i. Optic_ k p i (Curry ks i) s t a b
    oo = case appendProof @is @js @ks (Proxy :: Proxy i) of
        Refl -> o . o'
{-# INLINE (%%) #-}

-------------------------------------------------------------------------------
-- Optics.Iso
-------------------------------------------------------------------------------

-- An iso is unindexed
type Iso = Optic An_Iso '[]

iso :: (s -> a) -> (b -> t) -> Iso s t a b
iso f g = Optic (dimap f g)

_Identity :: Iso (Identity a) (Identity b) a b
_Identity = iso runIdentity Identity

-------------------------------------------------------------------------------
-- Optics.Lens
-------------------------------------------------------------------------------

-- A lens is unindexed too.
type Lens = Optic A_Lens '[]

lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
lens get set = Optic
    $ dimap
        (\s -> (get s, s))
        (\(b, s) -> set s b)
    . first'

toLens :: Is k A_Lens => Optic k '[] s t a b -> Lens s t a b
toLens = sub

_1 :: Lens (a, c) (b, c) a b
_1 = Optic first'

-------------------------------------------------------------------------------
-- Optics.Getter
-------------------------------------------------------------------------------

class is ~ '[] => CheckNonIndexed is
instance CheckNonIndexed '[]
instance (TypeError (Text "ERROR: non empty " :<>: ShowType (i ': is)), (i ': is) ~ '[]) => CheckNonIndexed (i ': is) where

view1 :: (Is k A_Lens, CheckNonIndexed is) => Optic' k is s a -> s -> a
view1 o = runForget $ getOptic (toLens o) (Forget id)

-------------------------------------------------------------------------------
-- Optics.Setter
-------------------------------------------------------------------------------

over :: (Is k A_Lens, CheckNonIndexed is) => Optic k is s t a b -> (a -> b) -> s -> t
over o ab = runFunArrow $ getOptic (toLens o) (FunArrow ab)

-------------------------------------------------------------------------------
-- Optics.IxSetter
-------------------------------------------------------------------------------

-- An indexed setter expects exactly one index.
type IxSetter i = Optic An_IxSetter '[i]

toIxSetter :: Is k An_IxSetter => Optic k '[i] s t a b -> IxSetter i s t a b
toIxSetter = sub

isets
  :: ((i -> a -> b) -> s -> t)
  -> IxSetter i s t a b
isets f = Optic (\(IxFunArrow k) -> IxFunArrow $ \ij -> f $ \i -> k (ij i))

iover :: Is k An_IxSetter => Optic k '[i] s t a b -> (i -> a -> b) -> s -> t
iover o iab = runIxFunArrow (getOptic (toIxSetter o) (IxFunArrow iab)) id

iEither :: IxSetter Bool (Either a a) (Either b b) a b
iEither = isets $ \iab e -> case e of
    Left a  -> Left (iab False a)
    Right a -> Right (iab True a)

-- Story with icompose will be more complicated, it has to operate on full optic
-- precomposing isn't possible

-- real type would use Is k "lowest indexed optic" and Join, i.e. be like (%)
icompose
  :: (i -> j -> ix)
  -> Optic An_IxSetter '[i, j] s t a b
  -> Optic An_IxSetter '[ix] s t a b
icompose f (Optic o) = Optic (ixcontramap (\g i j -> g (f i j)) . o)
{-# INLINE icompose #-}

-------------------------------------------------------------------------------
-- Demo
-------------------------------------------------------------------------------

{-

λ *MiniIndexedOptics>  :t _Identity % _1 % _1
_Identity % _1 % _1
  :: Optic
       'A_Lens '[] (Identity ((a, c1), c2)) (Identity ((b, c1), c2)) a b

λ *MiniIndexedOptics>  :t _Identity % _1 % _1 % iEither 
_Identity % _1 % _1 % iEither
  :: Optic
       'An_IxSetter
       '[Bool]
       (Identity ((Either a a, c1), c2))
       (Identity ((Either b b, c1), c2))
       a
       b

λ *MiniIndexedOptics>  iover (_Identity % _1 % _1 % iEither) (&&) (Identity ((Left True, 'x'), 'y'))
Identity ((Left False,'x'),'y')

λ *MiniIndexedOptics>  iover (_Identity % _1 % _1 % iEither) (&&) (Identity ((Right True, 'x'), 'y'))
Identity ((Right True,'x'),'y')

-}

-------------------------------------------------------------------------------
-- Profunctor
-------------------------------------------------------------------------------

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p i b c -> p i a d

instance Profunctor (Forget r) where
  dimap f _ (Forget k) = Forget (k . f)
  {-# INLINE dimap #-}

instance Profunctor FunArrow where
  dimap f g (FunArrow k) = FunArrow (g . k . f)
  {-# INLINE dimap #-}

instance Profunctor IxFunArrow where
  dimap f g (IxFunArrow k) = IxFunArrow (\i -> g . k i . f)
  {-# INLINE dimap #-}

-------------------------------------------------------------------------------
-- Strong
-------------------------------------------------------------------------------

class Profunctor p => Strong p where
  first'  :: p i a b -> p i (a, c) (b, c)
  second' :: p i a b -> p i (c, a) (c, b)

instance Strong (Forget r) where
  first'  (Forget k) = Forget (k . fst)
  second' (Forget k) = Forget (k . snd)
  {-# INLINE first' #-}
  {-# INLINE second' #-}

instance Strong FunArrow where
  first'  (FunArrow k) = FunArrow $ \ ~(a, c) -> (k a, c)
  second' (FunArrow k) = FunArrow $ \ ~(c, a) -> (c, k a)
  {-# INLINE first' #-}
  {-# INLINE second' #-}

instance Strong IxFunArrow where
  first'  (IxFunArrow k) = IxFunArrow $ \i ~(a, c) -> (k i a, c)
  second' (IxFunArrow k) = IxFunArrow $ \i ~(c, a) -> (c, k i a)
  {-# INLINE first' #-}
  {-# INLINE second' #-}

-------------------------------------------------------------------------------
-- IxProfunctor
-------------------------------------------------------------------------------

class IxProfunctor p where
  ixcontramap :: (i -> j) -> p j a b -> p i a b

instance IxProfunctor IxFunArrow where
  ixcontramap ij (IxFunArrow k) = IxFunArrow $ \i -> k (ij i)
  {-# INLINE ixcontramap #-}

-------------------------------------------------------------------------------
-- Newtypes
-------------------------------------------------------------------------------

newtype Forget r i a b = Forget { runForget :: a -> r }

newtype FunArrow i a b = FunArrow { runFunArrow :: a -> b }

newtype IxFunArrow i a b = IxFunArrow { runIxFunArrow :: i -> a -> b }