Last active
February 26, 2021 13:39
-
-
Save emilypi/407838d9c321d5b21ebc1828ad2bedcb to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
in the first case
stretchr
could be made more polymorphic, but in order for the laws to work out, we required ~ 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 toc
in order to be a valid update with a newb
, so it's only a superficial abstraction!In the case of the second, yes! I could reuse
Glassed
. Thanks!