Basic package structure
This commit is contained in:
parent
1f1bfc0428
commit
090b06a899
|
@ -10,5 +10,9 @@ sourcedir = "src"
|
|||
readme = "README.md"
|
||||
|
||||
langversion >= 0.6.0
|
||||
depends = profunctors >= 1.1.2
|
||||
|
||||
modules =
|
||||
modules = Control.Lens.Optic,
|
||||
Control.Lens.Equality,
|
||||
Control.Lens.Iso,
|
||||
Control.Lens.Lens
|
||||
|
|
50
src/Control/Lens/Equality.idr
Normal file
50
src/Control/Lens/Equality.idr
Normal file
|
@ -0,0 +1,50 @@
|
|||
module Control.Lens.Equality
|
||||
|
||||
import Control.Lens.Optic
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
public export
|
||||
record IsEquality {0 k,k' : _} (p : k -> k' -> Type) where
|
||||
constructor MkIsEquality
|
||||
|
||||
public export
|
||||
0 Equality : k -> k' -> k -> k' -> Type
|
||||
Equality s t a b = forall p. IsEquality p => p a b -> p s t
|
||||
|
||||
public export
|
||||
0 Equality' : k -> k -> Type
|
||||
Equality' s a = Equality s s a a
|
||||
|
||||
|
||||
public export
|
||||
runEq : Equality s t a b -> (s = a, t = b)
|
||||
runEq l = (l {p = \x,_ => x = a} Refl,
|
||||
l {p = \_,y => y = b} Refl)
|
||||
|
||||
public export
|
||||
runEq' : Equality s t a b -> s = a
|
||||
runEq' l = l {p = \x,_ => x = a} Refl
|
||||
|
||||
|
||||
public export
|
||||
substEq : forall p. Equality s t a b -> p a b a b -> p s t a b
|
||||
substEq {p} l = l {p = \x,y => p x y a b}
|
||||
|
||||
public export
|
||||
congEq : forall f,g. Equality s t a b -> Equality (f s) (g t) (f a) (g b)
|
||||
congEq l {p} = l {p = \x,y => p (f x) (g y)}
|
||||
|
||||
public export
|
||||
symEq : Equality s t a b -> Equality b a t s
|
||||
symEq l = case runEq l of (Refl, Refl) => id
|
||||
|
||||
|
||||
public export
|
||||
refl : Equality a b a b
|
||||
refl = id
|
||||
|
||||
public export
|
||||
simple : Equality' a a
|
||||
simple = id
|
143
src/Control/Lens/Iso.idr
Normal file
143
src/Control/Lens/Iso.idr
Normal file
|
@ -0,0 +1,143 @@
|
|||
module Control.Lens.Iso
|
||||
|
||||
import Data.Maybe
|
||||
import Data.Contravariant
|
||||
import Data.Tensor
|
||||
import Data.Profunctor
|
||||
import Control.Lens.Optic
|
||||
import Control.Lens.Equality
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
public export
|
||||
record IsIso p where
|
||||
constructor MkIsIso
|
||||
runIsIso : Profunctor p
|
||||
|
||||
|
||||
|
||||
public export
|
||||
0 Iso : (s,t,a,b : Type) -> Type
|
||||
Iso = Optic IsIso
|
||||
|
||||
public export
|
||||
0 Iso' : (s,a : Type) -> Type
|
||||
Iso' s a = Iso s s a a
|
||||
|
||||
|
||||
public export
|
||||
getIso : Iso s t a b -> (s -> a, b -> t)
|
||||
getIso l = l @{MkIsIso coexp} (id, id)
|
||||
where
|
||||
[coexp] Profunctor (\x,y => (x -> a, b -> y)) where
|
||||
dimap f g (f', g') = (f' . f, g . g')
|
||||
|
||||
public export
|
||||
withIso : Iso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
|
||||
withIso l f = uncurry f (getIso l)
|
||||
|
||||
public export
|
||||
under : Iso s t a b -> (t -> s) -> (b -> a)
|
||||
under l = let (f,g) = getIso l in (f .) . (. g)
|
||||
|
||||
|
||||
public export
|
||||
iso : (s -> a) -> (b -> t) -> Iso s t a b
|
||||
iso f g @{MkIsIso _} = dimap f g
|
||||
|
||||
public export
|
||||
fromEqv : s <=> a -> Iso' s a
|
||||
fromEqv (MkEquivalence l r) = iso l r
|
||||
|
||||
public export
|
||||
from : Iso s t a b -> Iso b a t s
|
||||
from l @{MkIsIso _} = withIso l (flip dimap)
|
||||
|
||||
|
||||
|
||||
public export
|
||||
au : Functor f => Iso s t a b -> ((b -> t) -> f s) -> f a
|
||||
au l f = withIso l $ \g,h => g <$> f h
|
||||
|
||||
public export
|
||||
auf : (Functor f, Functor g) => Iso s t a b -> (f t -> g s) -> f b -> g a
|
||||
auf l f x = withIso l $ \g,h => g <$> f (h <$> x)
|
||||
|
||||
public export
|
||||
xplat : Functor f => Iso s t a b -> ((s -> a) -> f b) -> f t
|
||||
xplat l f = withIso l $ \g,h => h <$> f g
|
||||
|
||||
public export
|
||||
xplatf : (Functor f, Functor g) => Iso s t a b -> (f a -> g b) -> f s -> g t
|
||||
xplatf l f x = withIso l $ \g,h => h <$> f (g <$> x)
|
||||
|
||||
|
||||
-- Example Isos
|
||||
|
||||
public export
|
||||
constant : a -> Iso (a -> b) (a' -> b') b b'
|
||||
constant x = iso ($ x) const
|
||||
|
||||
public export
|
||||
involuted : (a -> a) -> Iso' a a
|
||||
involuted f = iso f f
|
||||
|
||||
public export
|
||||
flipped : Iso (a -> b -> c) (a' -> b' -> c') (b -> a -> c) (b' -> a' -> c')
|
||||
flipped = iso flip flip
|
||||
|
||||
public export
|
||||
swapped : Symmetric f => Iso (f a b) (f a' b') (f b a) (f b' a')
|
||||
swapped = iso swap' swap'
|
||||
|
||||
public export
|
||||
casted : (Cast s a, Cast b t) => Iso s t a b
|
||||
casted = iso cast cast
|
||||
|
||||
public export
|
||||
non : Eq a => a -> Iso' (Maybe a) a
|
||||
non x = iso (fromMaybe x) (\y => guard (x /= y) $> y)
|
||||
|
||||
-- Mapping
|
||||
|
||||
public export
|
||||
mapping : (Functor f, Functor g) => Iso s t a b -> Iso (f s) (g t) (f a) (g b)
|
||||
mapping l = withIso l $ \f,g => iso (map f) (map g)
|
||||
|
||||
public export
|
||||
contramapping : (Contravariant f, Contravariant g) => Iso s t a b -> Iso (f a) (g b) (f s) (g t)
|
||||
contramapping l = withIso l $ \f,g => iso (contramap f) (contramap g)
|
||||
|
||||
public export
|
||||
bimapping : (Bifunctor f, Bifunctor g) => Iso s t a b -> Iso s' t' a' b' ->
|
||||
Iso (f s s') (g t t') (f a a') (g b b')
|
||||
bimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
|
||||
iso (bimap f f') (bimap g g')
|
||||
|
||||
public export
|
||||
mappingFst : (Bifunctor f, Bifunctor g) => Iso s t a b ->
|
||||
Iso (f s x) (g t y) (f a x) (g b y)
|
||||
mappingFst l = withIso l $ \f,g => iso (mapFst f) (mapFst g)
|
||||
|
||||
public export
|
||||
mappingSnd : (Bifunctor f, Bifunctor g) => Iso s t a b ->
|
||||
Iso (f x s) (g y t) (f x a) (g y b)
|
||||
mappingSnd l = withIso l $ \f,g => iso (mapSnd f) (mapSnd g)
|
||||
|
||||
public export
|
||||
dimapping : (Profunctor f, Profunctor g) => Iso s t a b -> Iso s' t' a' b' ->
|
||||
Iso (f a s') (g b t') (f s a') (g t b')
|
||||
dimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
|
||||
iso (dimap f f') (dimap g g')
|
||||
|
||||
public export
|
||||
lmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
|
||||
Iso (f a x) (g b y) (f s x) (g t y)
|
||||
lmapping l = withIso l $ \f,g => iso (lmap f) (lmap g)
|
||||
|
||||
public export
|
||||
rmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
|
||||
Iso (f x s) (g y t) (f x a) (g y b)
|
||||
rmapping l = withIso l $ \f,g => iso (rmap f) (rmap g)
|
||||
|
63
src/Control/Lens/Lens.idr
Normal file
63
src/Control/Lens/Lens.idr
Normal file
|
@ -0,0 +1,63 @@
|
|||
module Control.Lens.Lens
|
||||
|
||||
import Data.Profunctor
|
||||
import Data.Profunctor.Yoneda
|
||||
import Control.Lens.Optic
|
||||
import Control.Lens.Equality
|
||||
import Control.Lens.Iso
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
public export
|
||||
record IsLens p where
|
||||
constructor MkIsLens
|
||||
runIsLens : Strong p
|
||||
|
||||
export %hint
|
||||
lensToIso : IsLens p => IsIso p
|
||||
lensToIso @{MkIsLens _} = MkIsIso %search
|
||||
|
||||
|
||||
public export
|
||||
0 Lens : (s,t,a,b : Type) -> Type
|
||||
Lens = Optic IsLens
|
||||
|
||||
public export
|
||||
0 Lens' : (s,a : Type) -> Type
|
||||
Lens' s a = Lens s s a a
|
||||
|
||||
|
||||
public export
|
||||
lens : (s -> a) -> (s -> b -> t) -> Lens s t a b
|
||||
lens get set @{MkIsLens _} = dimap (\x => (x, get x)) (uncurry set) . second
|
||||
|
||||
public export
|
||||
getLens : Lens s t a b -> (s -> a, s -> b -> t)
|
||||
getLens l = l @{MkIsLens strong} (id, const id)
|
||||
where
|
||||
Profunctor (\x,y => (x -> a, x -> b -> y)) where
|
||||
dimap f g (get, set) = (get . f, (g .) . set . f)
|
||||
|
||||
[strong] GenStrong Pair (\x,y => (x -> a, x -> b -> y)) where
|
||||
strongl (get, set) = (get . fst, \(a,c),b => (set a b, c))
|
||||
strongr (get, set) = (get . snd, \(c,a),b => (c, set a b))
|
||||
|
||||
public export
|
||||
withLens : Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r
|
||||
withLens l f = uncurry f (getLens l)
|
||||
|
||||
|
||||
public export
|
||||
devoid : Lens Void Void a b
|
||||
devoid @{MkIsLens _} = dimap absurd snd . first
|
||||
|
||||
public export
|
||||
united : Lens' a ()
|
||||
united @{MkIsLens _} = dimap ((),) snd . first
|
||||
|
||||
|
||||
|
||||
public export
|
||||
fusing : IsIso p => Optic' (Yoneda p) s t a b -> Optic' p s t a b
|
||||
fusing @{MkIsIso _} l = proextract . l . propure
|
14
src/Control/Lens/Optic.idr
Normal file
14
src/Control/Lens/Optic.idr
Normal file
|
@ -0,0 +1,14 @@
|
|||
module Control.Lens.Optic
|
||||
|
||||
import Data.Profunctor
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
public export
|
||||
Optic' : (p : Type -> Type -> Type) -> (s,t,a,b : Type) -> Type
|
||||
Optic' p s t a b = p a b -> p s t
|
||||
|
||||
public export
|
||||
0 Optic : ((Type -> Type -> Type) -> Type) -> (s,t,a,b : Type) -> Type
|
||||
Optic constr s t a b = forall p. constr p => Optic' p s t a b
|
Loading…
Reference in a new issue