Skip to content

Commit 54ddea9

Browse files
eduardoejpeduardoejp
committed
Pro-functor case/prism (part 7 of optics).
1 parent 8326a79 commit 54ddea9

File tree

7 files changed

+203
-116
lines changed

7 files changed

+203
-116
lines changed

‎stdlib/source/library/lux/abstract/functor/pro.lux

+11
Original file line numberDiff line numberDiff line change
@@ -24,3 +24,14 @@
2424
(-> (it cause effect)
2525
(it (And extra cause) (And extra effect))))
2626
in_right)))
27+
28+
(every .public (Co_Cartesian it)
29+
(Interface
30+
(is (for_any (_ cause effect extra)
31+
(-> (it cause effect)
32+
(it (Or cause extra) (Or effect extra))))
33+
when_left)
34+
(is (for_any (_ cause effect extra)
35+
(-> (it cause effect)
36+
(it (Or extra cause) (Or extra effect))))
37+
when_right)))

‎stdlib/source/library/lux/aspect.lux

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@
2222
(<| (.in_module# .prelude)
2323
.with_template))
2424

25-
(every .public (Aspect it internal_cause internal_effect external_cause external_effect)
26-
(-> (it internal_cause internal_effect)
27-
(it external_cause external_effect)))
25+
(every .public (Aspect it context context' aspect aspect')
26+
(-> (it aspect aspect')
27+
(it context context')))
2828

2929
... TODO: Make this nominal type unnecessary.
3030
(nominal.every .public (Membership one all)

‎stdlib/source/library/lux/aspect/case.lux

+64-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,14 @@
44
(.using
55
[library
66
[lux (.except macro
7-
when)]])
7+
when)
8+
[abstract
9+
[functor
10+
["[0]" pro]]]
11+
["[0]" function]
12+
[data
13+
["[0]" sum]]]]
14+
["[0]" //])
815

916
(the macro
1017
(<| (.in_module# .prelude)
@@ -53,6 +60,12 @@
5360
[#when when
5461
#some some])
5562

63+
(the .public identity
64+
(for_any (_ it)
65+
(Case it it))
66+
(case sum.right
67+
function.identity))
68+
5669
(with_template [,name ,type ,tag]
5770
[(the .public ,name
5871
(for_any (_ context case)
@@ -63,3 +76,53 @@
6376
[when When #when]
6477
[some Some #some]
6578
)
79+
80+
(every .public (Aspect context context' case case')
81+
(for_any (_ it)
82+
(-> [(pro.Functor it) (pro.Co_Cartesian it)]
83+
(//.Aspect it context context' case case'))))
84+
85+
(the functor
86+
(for_any (_ case case')
87+
(pro.Functor (for_any (_ context context')
88+
(Case' context context'
89+
case case'))))
90+
(implementation
91+
(the (each before after [/#when /#some])
92+
[#when (|>> before /#when (sum.then after function.identity))
93+
#some (|>> /#some after)])))
94+
95+
(the co_cartesian
96+
(for_any (_ case case')
97+
(pro.Co_Cartesian (for_any (_ context context')
98+
(Case' context context'
99+
case case'))))
100+
(implementation
101+
(the (when_left [/#when /#some])
102+
[#when (sum.either (|>> /#when (sum.then sum.left function.identity))
103+
(|>> sum.right sum.left))
104+
#some (|>> /#some sum.left)])
105+
(the (when_right [/#when /#some])
106+
[#when (sum.either (|>> sum.left sum.left)
107+
(|>> /#when (sum.then sum.right function.identity)))
108+
#some (|>> /#some sum.right)])))
109+
110+
(the .public (as_aspect [/#when /#some]
111+
[pro_functor co_cartesian])
112+
(for_any (_ context context' case case')
113+
(-> (Case' context context' case case')
114+
(Aspect context context' case case')))
115+
(<| (with pro_functor)
116+
(with co_cartesian)
117+
(|>> when_right
118+
(each /#when (sum.either function.identity /#some)))))
119+
120+
(the .public (of_aspect it)
121+
(for_any (_ context context' case case')
122+
(-> (Aspect context context' case case' (for_any (_ context context')
123+
(Case' context context'
124+
case case')))
125+
(Case' context context' case case')))
126+
(it [..functor ..co_cartesian]
127+
[#when sum.right
128+
#some function.identity]))

‎stdlib/source/library/lux/aspect/property.lux

+57-53
Original file line numberDiff line numberDiff line change
@@ -92,56 +92,60 @@
9292
#has (function (_ [focus context])
9393
(revised outer (has inner focus) context))])
9494

95-
(comment
96-
(every .public (Aspect external_cause external_effect internal_cause internal_effect)
97-
(for_any (_ it)
98-
(-> [(pro.Functor it) (pro.Cartesian it)]
99-
(//.Aspect it external_cause external_effect internal_cause internal_effect))))
100-
101-
(the functor
102-
(for_any (_ internal_cause internal_effect)
103-
(pro.Functor (Property' internal_cause internal_effect)))
104-
(implementation
105-
(the (each before after [/#its /#has])
106-
(..property' (|>> before
107-
/#its)
108-
(|>> (product.then function.identity before)
109-
/#has
110-
after)))))
111-
112-
(the cartesian
113-
(for_any (_ internal_cause internal_effect)
114-
(pro.Cartesian (Property' internal_cause internal_effect)))
115-
(implementation
116-
(the (in_left [/#its /#has])
117-
(..property' (|>> product.left
118-
/#its)
119-
(product.forked (|>> (product.then function.identity product.left)
120-
/#has)
121-
(|>> product.right
122-
product.right))))
123-
(the (in_right [/#its /#has])
124-
(..property' (|>> product.right
125-
/#its)
126-
(product.forked (|>> product.right
127-
product.left)
128-
(|>> (product.then function.identity product.right)
129-
/#has))))))
130-
131-
(the .public (as_property [/#its /#has]
132-
[pro_functor cartesian])
133-
(for_any (_ internal_cause internal_effect external_cause external_effect)
134-
(-> (Property' internal_cause internal_effect external_cause external_effect)
135-
(Aspect internal_cause internal_effect external_cause external_effect)))
136-
(<| (.with pro_functor)
137-
(.with cartesian)
138-
(|>> in_left
139-
(each (product.forked /#its function.identity) /#has))))
140-
141-
(the .public (as_property' it)
142-
(for_any (_ internal_cause internal_effect external_cause external_effect)
143-
(-> (Aspect internal_cause internal_effect external_cause external_effect (Property' internal_cause internal_effect))
144-
(Property' internal_cause internal_effect external_cause external_effect)))
145-
(it [..functor ..cartesian]
146-
..identity))
147-
)
95+
(every .public (Aspect context context' focus focus')
96+
(for_any (_ it)
97+
(-> [(pro.Functor it) (pro.Cartesian it)]
98+
(//.Aspect it context context' focus focus'))))
99+
100+
(the functor
101+
(for_any (_ focus focus')
102+
(pro.Functor (for_any (_ context context')
103+
(Property' context context'
104+
focus focus'))))
105+
(implementation
106+
(the (each before after [/#its /#has])
107+
[#its (|>> before
108+
/#its)
109+
#has (|>> (product.then function.identity before)
110+
/#has
111+
after)])))
112+
113+
(the cartesian
114+
(for_any (_ focus focus')
115+
(pro.Cartesian (for_any (_ context context')
116+
(Property' context context'
117+
focus focus'))))
118+
(implementation
119+
(the (in_left [/#its /#has])
120+
[#its (|>> product.left
121+
/#its)
122+
#has (product.forked (|>> (product.then function.identity product.left)
123+
/#has)
124+
(|>> product.right
125+
product.right))])
126+
(the (in_right [/#its /#has])
127+
[#its (|>> product.right
128+
/#its)
129+
#has (product.forked (|>> product.right
130+
product.left)
131+
(|>> (product.then function.identity product.right)
132+
/#has))])))
133+
134+
(the .public (as_aspect [/#its /#has]
135+
[pro_functor cartesian])
136+
(for_any (_ context context' focus focus')
137+
(-> (Property' context context' focus focus')
138+
(Aspect context context' focus focus')))
139+
(<| (with pro_functor)
140+
(with cartesian)
141+
(|>> in_left
142+
(each (product.forked /#its function.identity) /#has))))
143+
144+
(the .public (of_aspect it)
145+
(for_any (_ context context' focus focus')
146+
(-> (Aspect context context' focus focus' (for_any (_ context context')
147+
(Property' context context' focus focus')))
148+
(Property' context context' focus focus')))
149+
(it [..functor ..cartesian]
150+
[#its function.identity
151+
#has product.left]))

‎stdlib/source/library/lux/aspect/view.lux

+52-56
Original file line numberDiff line numberDiff line change
@@ -20,51 +20,51 @@
2020
.with_template))
2121

2222
(the As'
23-
(macro (_ it it'
23+
(macro (_ context context'
2424
analogy analogy')
25-
[(-> it'
26-
analogy')]))
25+
[(-> context
26+
analogy)]))
2727

2828
(the Of'
29-
(macro (_ it it'
29+
(macro (_ context context'
3030
analogy analogy')
31-
[(-> analogy
32-
it)]))
31+
[(-> analogy'
32+
context')]))
3333

34-
(every (View' it it'
34+
(every (View' context context'
3535
analogy analogy')
3636
(Record
37-
[#as (As' it it'
37+
[#as (As' context context'
3838
analogy analogy')
39-
#of (Of' it it'
39+
#of (Of' context context'
4040
analogy analogy')]))
4141

4242
(the As
43-
(macro (_ it analogy)
44-
[(As' it it
43+
(macro (_ context analogy)
44+
[(As' context context
4545
analogy analogy)]))
4646

4747
(the Of
48-
(macro (_ it analogy)
49-
[(Of' it it
48+
(macro (_ context analogy)
49+
[(Of' context context
5050
analogy analogy)]))
5151

52-
(every .public (View it analogy)
53-
(View' it it
52+
(every .public (View context analogy)
53+
(View' context context
5454
analogy analogy))
5555

5656
(the .public (view as of)
57-
(for_any (_ it analogy)
58-
(-> (As it analogy) (Of it analogy)
59-
(View it analogy)))
57+
(for_any (_ context analogy)
58+
(-> (As context analogy) (Of context analogy)
59+
(View context analogy)))
6060
[#as as
6161
#of of])
6262

6363
(with_template [,name ,type ,tag]
6464
[(the .public ,name
65-
(for_any (_ it analogy)
66-
(-> (View it analogy)
67-
(,type it analogy)))
65+
(for_any (_ context analogy)
66+
(-> (View context analogy)
67+
(,type context analogy)))
6868
(.its ,tag))]
6969

7070
[as As #as]
@@ -76,38 +76,34 @@
7676
(View it it))
7777
(..view function.identity function.identity))
7878

79-
(comment
80-
(every .public (Aspect it it' analogy analogy')
81-
(for_any (_ it)
82-
(-> (pro.Functor it)
83-
(//.Aspect it it it' analogy analogy'))))
84-
85-
(the (as_aspect [/#as /#of]
86-
[pro_functor])
87-
(for_any (_ it it' analogy analogy')
88-
(-> (View' it it' analogy analogy')
89-
(Aspect it it' analogy analogy')))
90-
(<| (.with pro_functor)
91-
(each /#of /#as)))
92-
93-
(the functor
94-
(for_any (_ it it')
95-
(pro.Functor (View' it it')))
96-
(implementation
97-
(the (each before after [/#as /#of])
98-
[#as (|>> /#as after)
99-
#of (|>> before /#of)])))
100-
101-
(the .public identity'
102-
(for_any (_ it)
103-
(Aspect it it
104-
it it))
105-
(..as_aspect ..identity))
106-
107-
(the (of_aspect it)
108-
(for_any (_ it it' analogy analogy')
109-
(-> (Aspect it it' analogy analogy' (View' it it'))
110-
(View' it it' analogy analogy')))
111-
(it [..functor]
112-
..identity))
113-
)
79+
(every .public (Aspect context context' analogy analogy')
80+
(for_any (_ it)
81+
(-> (pro.Functor it)
82+
(//.Aspect it context context' analogy analogy'))))
83+
84+
(the functor
85+
(for_any (_ analogy analogy')
86+
(pro.Functor (for_any (_ context context')
87+
(View' context context'
88+
analogy analogy'))))
89+
(implementation
90+
(the (each before after [/#as /#of])
91+
[#as (|>> before /#as)
92+
#of (|>> /#of after)])))
93+
94+
(the .public (as_aspect [/#as /#of]
95+
[pro_functor])
96+
(for_any (_ context context' analogy analogy')
97+
(-> (View' context context' analogy analogy')
98+
(Aspect context context' analogy analogy')))
99+
(<| (with pro_functor)
100+
(each /#as /#of)))
101+
102+
(the .public (of_aspect it)
103+
(for_any (_ context context' analogy analogy')
104+
(-> (Aspect context context' analogy analogy' (for_any (_ context context')
105+
(View' context context' analogy analogy')))
106+
(View' context context' analogy analogy')))
107+
(it [..functor]
108+
[#as function.identity
109+
#of function.identity]))

‎stdlib/source/library/lux/data/sum.lux

+4-3
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,11 @@
1414
["[0]" template]]]])
1515

1616
(template.with [<right?> <name>]
17-
[(the .public (<name> value)
17+
[(the .public <name>
1818
(for_any (_ left right)
19-
(-> <name> (Or left right)))
20-
{<right?> value})]
19+
(-> <name>
20+
(Or left right)))
21+
(|>> {<right?>}))]
2122

2223
[#0 left]
2324
[#1 right])

‎stdlib/source/library/lux/function.lux

+12
Original file line numberDiff line numberDiff line change
@@ -61,3 +61,15 @@
6161
(the (in_right it)
6262
(function (_ [extra cause])
6363
[extra (it cause)]))))
64+
65+
(the .public co_cartesian
66+
(pro.Co_Cartesian Function)
67+
(implementation
68+
(the (when_left it left|right)
69+
(when left|right
70+
{#0 left} {#0 (it left)}
71+
{#1 right} {#1 right}))
72+
(the (when_right it left|right)
73+
(when left|right
74+
{#0 left} {#0 left}
75+
{#1 right} {#1 (it right)}))))

0 commit comments

Comments
 (0)