Profunctor optics

Lens.BaseTypes.idr

module Lens.BaseTypes

public export
data SumType = Opt1 String Double | Opt2

public export
record RecordType where
    constructor MkRecordType
    recValue1 : String
    recValue2 : Double

Lens.Concrete.idr

module Lens.Concrete

import Lens.BaseTypes

public export
record Lens s t a b where
    constructor MkLens
    view : s -> a
    update : (b, s) -> t

export
Lens' : Type -> Type -> Type
Lens' a b = Lens a a b b

export
fstLens : Lens' (a, b) a
fstLens = MkLens (\(a,_) => a) (\(a,(_,b)) => (a, b))

export
sndLens : Lens' (a, b) b
sndLens = MkLens (\(_,a) => a) (\(b,(a,_)) => (a,b))

export
recValue1Lens : Lens' RecordType String
recValue1Lens = MkLens recValue1 (\(b,s) => {recValue1 := b} s)

export
recValue2Lens : Lens' RecordType Double
recValue2Lens = MkLens recValue2 (\(b,s) => {recValue2 := b} s)

export
composeLens : Lens' b c -> Lens' a b -> Lens' a c
composeLens (MkLens v1 u1) (MkLens v2 u2) = MkLens
    { view = v1 . v2
    , update = \(b,s) => u2 (u1 (b,v2 s),s)
    }

public export
record Adapter s t a b where
    constructor MkAdapter
    from : s -> a
    to : b -> t

export
Adapter' : Type -> Type -> Type
Adapter' a b = Adapter a a b b

export
swapAdapter : Adapter' (a,b) (b,a)
swapAdapter = MkAdapter
    { from = swap
    , to = swap
    }

public export
record Prism s t a b where
    constructor MkPrism
    match : s -> Either a t
    build : b -> t

export
Prism' : Type -> Type -> Type
Prism' a b = Prism a a b b

export
thePrism : Prism (Maybe a) (Maybe b) a b
thePrism = MkPrism
    { match = maybe (Right Nothing) Left
    , build = Just
    }

public export
record Affine s t a b where
    constructor MkAffine
    preview : s -> Either a t
    set : (b, s) -> t

export
Affine' : Type -> Type -> Type
Affine' a b = Affine a a b b

export
strAffine : Affine' SumType String
strAffine = MkAffine
    { preview = \x => case x of
        (Opt1 y _) => Left y
        Opt2 => Right x
    , set = \(b,s) => case s of
        (Opt1 _ z) => Opt1 b z
        Opt2 => Opt2
    }

public export
record Traversal s t a b where
    constructor MkTraversal
    contents : s -> List a
    fill : List b -> s -> t

export
Traversal' : Type -> Type -> Type
Traversal' a b = Traversal a a b b

Lens.Profunctor.idr

module Lens.Profunctor

import Profunctors
import Lens.Concrete
import Control.Applicative.Const
import Lens.BaseTypes
import Control.Monad.Identity

AdapterP s t a b = {p : _} -> Profunctor p => p a b -> p s t

AdapterP' a b = AdapterP a a b b

fromP : {a:_} -> AdapterP s t a b -> s -> a
fromP f = runConst . runUpStar (f {p = UpStar (Const a)} (MkUpStar MkConst))

toP : AdapterP s t a b -> b -> t
toP f = unTagged . f . MkTagged

adapterC2P : Adapter s t a b -> AdapterP s t a b
adapterC2P (MkAdapter from to) = dimap from to

adapterP2C : {a:_} -> AdapterP s t a b -> Adapter s t a b
adapterP2C f = MkAdapter (fromP f) (toP f)

swapAdapter : AdapterP' (a, b) (b, a)
swapAdapter = dimap swap swap

LensP s t a b = {p:_} -> Cartesian p => p a b -> p s t

LensP' a b = LensP a a b b

viewP : {a:_} -> LensP s t a b -> s -> a
viewP f = runConst . runUpStar (f {p = UpStar (Const a)} (MkUpStar MkConst))

updateP : LensP s t a b -> (b, s) -> t
updateP f (b, s) = f {p = \a, b => a -> b} (const b) s

lensP : (s -> a) -> ((b, s) -> t) -> LensP s t a b
lensP v u = dimap (\s => (v s, s)) u . first

recValue1Lens : LensP' RecordType String
recValue1Lens x = dimap (\s => (recValue1 s, s)) (\(b, s) => {recValue1 := b} s) (first x)

recValue2Lens : LensP' RecordType Double
recValue2Lens x = dimap (\s => (recValue2 s, s)) (\(b, s) => {recValue2 := b} s) (first x)

lensC2P : Lens s t a b -> LensP s t a b
lensC2P (MkLens view update) = dimap (\x => (view x,x)) update . first

lensP2C : {a:_} -> LensP s t a b -> Lens s t a b
lensP2C f = MkLens (viewP f) (updateP f)

PrismP s t a b = {p:_} -> Cocartesian p => p a b -> p s t

PrismP' a b = PrismP a a b b

matchP : {a:_} -> PrismP s t a b -> s -> Either a t
matchP f = runUpStar $ f {p = UpStar (Either a)} $ MkUpStar Left

buildP : PrismP s t a b -> b -> t
buildP f = unTagged . f . MkTagged

thePrism : PrismP' (Maybe a) a
thePrism = dimap (\x => maybe (Left x) Right x) (either id Just) . right

prismC2P : Prism s t a b -> PrismP s t a b
prismC2P (MkPrism match build) = dimap match (either build id) . left

prismP2C : {a:_} -> PrismP s t a b -> Prism s t a b
prismP2C f = MkPrism (matchP f) (buildP f)

AffineP s t a b = {p:_} -> (Cartesian p, Cocartesian p) => p a b -> p s t

AffineP' a b = AffineP a a b b

previewP : {a:_} -> AffineP s t a b -> s -> Either a t
previewP f = runUpStar $ f {p = UpStar (Either a)} $ MkUpStar Left

setP : AffineP s t a b -> (b, s) -> t
setP f (b,s) = f {p = \a, b => a -> b} (const b) s

strAffine : AffineP' SumType String
strAffine = dimap (\x => (split x, x)) (uncurry merge) . first . left
    where
    split : SumType -> Either String SumType
    split (Opt1 x _) = Left x
    split Opt2 = Right Opt2

    merge : Either String SumType -> SumType -> SumType
    merge (Left x) (Opt1 _ y) = Opt1 x y
    merge _ x = x

affineC2P : Affine s t a b -> AffineP s t a b -- p a b -> p s t
affineC2P (MkAffine preview set)
    = dimap (\x => (preview x, x)) (\(eb,s) => either (\b => set (b,s)) id eb) . first . left

affineP2C : {a:_} -> AffineP s t a b -> Affine s t a b
affineP2C f = MkAffine (previewP f) (setP f)

TraversalP s t a b = {p:_} -> (Cartesian p, Cocartesian p, Monoidal p) => p a b -> p s t

TraversalP' a b = TraversalP a a b b

contentsP : {a:_} -> TraversalP s t a b -> s -> List a
contentsP f = runConst . runUpStar (f {p = UpStar (Const (List a))} $ MkUpStar $ \x => MkConst [x])

modifyP : TraversalP s t a b -> (a -> b) -> s -> t
modifyP f x = f {p = \a, b => a -> b} x

traversalC2P : Traversal s t a b -> TraversalP s t a b 
traversalC2P (MkTraversal contents fill) x = dimap (\s => (contents s, s)) (uncurry fill) $ first $ iter
    where
        uncons' : List a -> Either () (a, List a)
        uncons' [] = Left ()
        uncons' (x::xs) = Right (x,xs)

        cons' : Either () (b, List b) -> List b
        cons' (Left ()) = []
        cons' (Right (x,xs)) = x::xs

        iter : p (List a) (List b)
        iter = dimap uncons' cons' $ right $ par x iter

LensVL s t a b = {f:_} -> Functor f => (a -> f b) -> (s -> f t)

lensVL : (s -> a) -> ((b, s) -> t) -> LensVL s t a b
lensVL v u = runUpStar . dimap (\s => (v s, s)) u . first {p = UpStar f} . MkUpStar

viewVL : {a:_} -> LensVL s t a b -> s -> a
viewVL f = runConst . (f {f = (Const a)} MkConst)

updateVL : LensVL s t a b -> (b, s) -> t
updateVL f (b', s) = runIdentity $ f {f = Identity} (Id . const b') s

lensVL2P : {a:_} -> LensVL s t a b -> LensP s t a b
lensVL2P l = lensP (viewVL l) (updateVL l)

lensP2VL : LensP s t a b -> LensVL s t a b
lensP2VL l x = runUpStar $ l $ MkUpStar {f=f} x

Profunctors.idr

module Profunctors

public export
interface Profunctor p where
    dimap : (a' -> a) -> (b -> b') -> p a b -> p a' b'

    lmap : (a' -> a) -> p a b -> p a' b
    lmap f = dimap f id

    rmap : (b -> b') -> p a b -> p a b'
    rmap f = dimap id f

public export
interface Profunctor p => Cartesian p where
    first : p a b -> p (a, c) (b, c)
    second : p a b -> p (c, a) (c, b)

public export
interface Profunctor p => Cocartesian p where
    left : p a b -> p (Either a c) (Either b c)
    right : p a b -> p (Either c a) (Either c b)

public export
interface Profunctor p => Monoidal p where
    par : p a b -> p c d -> p (a, c) (b, d)
    empty : p () ()

public export
Profunctor (\a, b => a -> b) where
    dimap f g h = g . h . f

public export
Cartesian (\a, b => a -> b) where
    first f = \(a, c) => (f a, c)
    second f = \(c, a) => (c, f a)

public export
Cocartesian (\a, b => a -> b) where
    left f = either (Left . f) Right
    right f = either Left (Right . f)

public export
Monoidal (\a, b => a -> b) where
    par f g (a, b) = (f a, g b)
    empty = id

public export
record UpStar (f:Type -> Type) a b where
    constructor MkUpStar
    runUpStar : a -> f b

public export
Functor f => Profunctor (UpStar f) where
    dimap f g h = MkUpStar $ map g . runUpStar h . f

public export
Functor f => Cartesian (UpStar f) where
    first f = MkUpStar $ \(a, c) => map (,c) (runUpStar f a)
    second f = MkUpStar $ \(c, a) => map (c,) (runUpStar f a)

public export
Applicative f => Cocartesian (UpStar f) where
    left f = MkUpStar $ either (map Left . runUpStar f) (pure . Right)
    right f = MkUpStar $ either (pure . Left) (map Right . runUpStar f)

public export
Applicative f => Monoidal (UpStar f) where
    par f g = MkUpStar $ \(a, c) => [| (runUpStar f a,runUpStar g c) |]
    empty = MkUpStar $ const $ pure ()

public export
record DownStar (f:Type -> Type) a b where
    constructor MkDownStar
    runDownStar : f a -> b

public export
Functor f => Profunctor (DownStar f) where
    dimap f g h = MkDownStar $ g . runDownStar h . map f

-- Cannot create definitions of Cartesian and Cocartesian due to the requirement of splitting the value and
-- extracitng it from functors.

public export
Applicative f => Monoidal (DownStar f) where
    par f g = MkDownStar $ \x => (runDownStar f $ map fst x, runDownStar g $ map snd x)
    empty = MkDownStar $ const ()

public export
record Tagged (a:Type) b where
    constructor MkTagged
    unTagged : b

public export
Profunctor Tagged where
    dimap f g h = MkTagged $ g $ unTagged h

public export
Cocartesian Tagged where
    left = MkTagged . Left . unTagged
    right = MkTagged . Right . unTagged

public export
Monoidal Tagged where
    par f g = MkTagged (unTagged f, unTagged g)
    empty = MkTagged ()