optics.hs

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


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 (Either a c) (Either b c)
  right :: p a b -> p (Either c a) (Either 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 (c -> a) (c -> b)

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 (Closed p, Traversing p) => Polynodal p where
  gridded :: p a b -> p (d -> ([a], c)) (d -> ([b], c))
  gridded = closed . stretchl

class (Strong p, Closed p) => Glassed p where
  glassed :: p a b -> p (t, u -> a) (t, u -> b)
  glassed = second . closed

class (Strong p, Choice p) => Magnified p where
  magnify :: p a b -> p (c, Either a d) (c, Either b d)
  magnify = second . left

class (Closed p, Choice p) => Telescoped p where
  telescope :: p a b -> p (Either (c -> a) d) (Either (c -> b) d)
  telescope = left . closed

class (Choice p, Strong p, Closed p) => Windowed p where
  windowed :: p a b -> p (Either v (t, u -> a)) (Either v (t, u -> b))
  windowed = right . second . closed

-- i'm just using random words at this point. The naming convention doesn't scale well :x
class Profunctor p => Polyp p where
  polyper :: Applicative f => p a b -> p (f a) (f b)

-- --------------------------------------------------------------------- --
-- 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 AffineTraversal s t a b = forall p.    Magnified p => Optic p s t a b
type AffineWindow    s t a b = forall p.   Telescoped 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 Grid            s t a b = forall p.    Polynodal p => Optic p s t a b -- closed traversal
type Kaleidescope    s t a b = forall p.        Polyp 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 -

-- Isos are like equivalences 
type a ~= b = Iso b a b a

-- Prisms act like <= relations 
type a <= b = Prism' b a

-- Lenses act like "divides by" (i.e. a | b) relations
type a .| b = Lens' b a

-- Traversals act like taylor series
type a .& b = Traversal' b a

-- Grates act like logarithms (which makes sense consider 
-- all naperian functors are iso to (->) t). A logarithm for a type
-- is like understanding how to factor it into a transition function
--
type Log a b = Grate b a b a

-- Like a Grate, but packages the starting state with 
-- the transition function
--
type Logg a b = Glass b a b a

-- a state machine which either yields a value, or continues with a logg
--
type AutExp b a = Window b a b a 

-- --------------------------------------------------------------------- --
-- Examples: Optics form proof-relevant arithmetic relations

type Z = ()
type S a = Either 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 <= (Either a b)
_Left = left

_Right :: b <= (Either 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)) (\(a,f) -> f a) . glassed

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

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

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

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

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

-- --------------------------------------------------------------------- --
-- Traversal Example using Analytic functors

-- free tambara monad
data Phi p a b where
  Phi :: (a -> ([u], c))
      -> p u v
      -> (b -> ([v], d))
      -> Phi p a b

-- cofree tambara comonad
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

in the first case stretchr could be made more polymorphic, but in order for the laws to work out, we require d ~ c. In holistic terms, c is the residue of the optic - the complement of its focus. This residue must be the same, or be something isomorphic to c in order to be a valid update with a new b, so it's only a superficial abstraction!

In the case of the second, yes! I could reuse Glassed. Thanks!