-
Notifications
You must be signed in to change notification settings - Fork 0
/
Optic.blod
34 lines (24 loc) · 1.34 KB
/
Optic.blod
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
-- -------------------------------------------------------------- [ Optic.blod ]
-- Description : Linear optics in Idris
-- Copyright : (c) 2019 Vanessa McHale
-- --------------------------------------------------------------------- [ EOH ]
module Optic
import Category.ProViewFunctor
import Function
import Logic.Linear
ViewOptic : (Type -> Type -> Type) -> Type -> Type -> Type -> Type -> Type
ViewOptic p a b s t = p a b -> p s t
ViewIso : Type -> Type -> Type -> Type -> Type
ViewIso a b s t = { p : Type -> Type -> Type } -> ProViewFunctor p => ViewOptic p a b s t
ViewLens : Type -> Type -> Type -> Type -> Type
ViewLens a b s t = { p : Type -> Type -> Type } -> ViewCartesian p => ViewOptic p a b s t
ViewPrism : Type -> Type -> Type -> Type -> Type
ViewPrism a b s t = { p : Type -> Type -> Type } -> CoViewCartesian p => ViewOptic p a b s t
ViewTraversal : Type -> Type -> Type -> Type -> Type
ViewTraversal a b s t = { p : Type -> Type -> Type } -> ViewCartesian p -> CoViewCartesian p -> MonoidalView p => ViewOptic p a b s t
data ViewIsoC : (a : Type) -> (b : Type) -> (s : Type) -> (t : Type) -> Type where
MkIso : (s -. a) -> (b -. t) -> ViewIsoC a b s t
ProViewFunctor (ViewIsoC a b) where
diviewmap f g (MkIso o i) = MkIso (o .! f) (g .! i)
mkAbstract : ViewIsoC a b s t -> ViewIso a b s t
mkAbstract (MkIso from to) = diviewmap from to