optics.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE GADTs #-}
module Data.Sheaves.Optics where


type a + b = Either a b
type a * b = (a, b)
type a ^ b = b -> a

infixl 6 +
infixl 7 *
infixr 8 ^

class Profunctor p where
  dimap :: (s -> a) -> (b -> t) -> p a b -> p s t

class Profunctor p => Choice p where
  left :: p a b -> p (a + c) (b + c)
  right :: p a b -> p (c + a) (c + b)

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

class Profunctor p => Closed p where
  closed :: p a b -> p (a^c) (b^c)

class Profunctor p => Traversing p where
  stretchl :: p a b -> p ([a] * c) ([b] * c)
  stretchr :: p a b -> p (c * [a]) (d * [b])

class (Strong p, Closed p) => Glassed p where
  glassed :: p a b -> p (t * a^u) (v * b^w)

class (Choice p, Strong p, Closed p) => Windowed p where
  windowed :: p a b -> p (a + (t * a^u)) (b + (v, b^w))

-- --------------------------------------------------------------------- --
-- Optics

type Optic p s t a b = p a b -> p s t

type Iso       s t a b = forall p. Profunctor p => Optic p s t a b
type Lens      s t a b = forall p.     Strong p => Optic p s t a b
type Prism     s t a b = forall p.     Choice p => Optic p s t a b
type Grate     s t a b = forall p.     Closed p => Optic p s t a b
type Glass     s t a b = forall p.    Glassed p => Optic p s t a b
type Window    s t a b = forall p.   Windowed p => Optic p s t a b
type Traversal s t a b = forall p. Traversing p => Optic p s t a b

type Iso' s a = Iso s s a a
type Prism' s a = Prism s s a a
type Lens' s a = Lens s s a a
type Traversal' s a = Traversal s s a a

-- --------------------------------------------------------------------- --
-- Analogies

type a ~= b = Iso b a b a
type a <= b = Prism' b a
type a .| b = Lens' b a
type a .& b = Traversal' b a
type Log a b = Grate b a b a
type Logg a b = Glass b a b a
type Exp b a = Window b a b a

-- --------------------------------------------------------------------- --
-- Examples

type Z = ()
type S a = a + Z
type One = S Z
type Two = S One
type Three = S Two
type Four = S Three

(&) :: a -> (a -> b) -> b
(&) = flip ($)

_I :: a ~= b
_I = dimap id id

_1 :: a .| (a * b)
_1 = first

_2 :: b .| (a * b)
_2 = second

_Left :: a <= (a + b)
_Left = left

_Right :: b <= (a + b)
_Right = right

_Log :: c -> (Log b a)
_Log c = dimap const ($ c) . closed

_LogBased :: Logg b a
_LogBased = dimap (\a -> (a, const a)) (uncurry (&)) . glassed

_Exponential :: Exp b a
_Exponential = dimap Left (either id (uncurry (&))) . windowed

_Traversing :: a .& ([a] * c)
_Traversing = stretchl

twolethree :: Two <= (Two + One)
twolethree = _Left

onelethree :: One <= (Two + One)
onelethree = _Right

divby2 :: Two .| (Two * Three)
divby2 = _1

divby3 :: Three .| (Two * Three)
divby3 = _2

-- --------------------------------------------------------------------- --
-- Traversal Example

data Phi p a b where
  Phi :: (a -> [u] * c)
      -> p u v
      -> (b -> [v] * d)
      -> Phi p a b

data Theta p a b = forall c. Theta p ([a] * c) ([b] * c)

data Stream where
  SCons :: t -> Stream -> Stream

data Analytic a where
  Run :: (Stream, a * Analytic a) -> Analytic a
  Cons :: a -> Analytic a -> Analytic a

singleton :: a -> Analytic a
singleton a = Cons a (singleton a)

class Profunctor p => Expanding p where
  expansion :: p a b -> p (Analytic a) (Analytic b)

type Taylor s t a b = forall p. Expanding p => Optic p s t a b

type a .** b = Taylor a b a b

taylor :: a .** b
taylor = dimap singleton k . expansion
  where
    k (Run (_, (a, _))) = a