Skip to content

Commit

Permalink
Pro-functor case/prism (part 7 of optics).
Browse files Browse the repository at this point in the history
  • Loading branch information
@eduardoejp
eduardoejp committed Jun 10, 2024
1 parent 8326a79 commit 54ddea9
Show file tree
Hide file tree
Showing 7 changed files with 203 additions and 116 deletions.
11 changes: 11 additions & 0 deletions stdlib/source/library/lux/abstract/functor/pro.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,3 +24,14 @@
(-> (it cause effect)
(it (And extra cause) (And extra effect))))
in_right)))

(every .public (Co_Cartesian it)
(Interface
(is (for_any (_ cause effect extra)
(-> (it cause effect)
(it (Or cause extra) (Or effect extra))))
when_left)
(is (for_any (_ cause effect extra)
(-> (it cause effect)
(it (Or extra cause) (Or extra effect))))
when_right)))
6 changes: 3 additions & 3 deletions stdlib/source/library/lux/aspect.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,9 @@
(<| (.in_module# .prelude)
.with_template))

(every .public (Aspect it internal_cause internal_effect external_cause external_effect)
(-> (it internal_cause internal_effect)
(it external_cause external_effect)))
(every .public (Aspect it context context' aspect aspect')
(-> (it aspect aspect')
(it context context')))

... TODO: Make this nominal type unnecessary.
(nominal.every .public (Membership one all)
Expand Down
65 changes: 64 additions & 1 deletion stdlib/source/library/lux/aspect/case.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,14 @@
(.using
[library
[lux (.except macro
when)]])
when)
[abstract
[functor
["[0]" pro]]]
["[0]" function]
[data
["[0]" sum]]]]
["[0]" //])

(the macro
(<| (.in_module# .prelude)
Expand Down Expand Up @@ -53,6 +60,12 @@
[#when when
#some some])

(the .public identity
(for_any (_ it)
(Case it it))
(case sum.right
function.identity))

(with_template [,name ,type ,tag]
[(the .public ,name
(for_any (_ context case)
Expand All @@ -63,3 +76,53 @@
[when When #when]
[some Some #some]
)

(every .public (Aspect context context' case case')
(for_any (_ it)
(-> [(pro.Functor it) (pro.Co_Cartesian it)]
(//.Aspect it context context' case case'))))

(the functor
(for_any (_ case case')
(pro.Functor (for_any (_ context context')
(Case' context context'
case case'))))
(implementation
(the (each before after [/#when /#some])
[#when (|>> before /#when (sum.then after function.identity))
#some (|>> /#some after)])))

(the co_cartesian
(for_any (_ case case')
(pro.Co_Cartesian (for_any (_ context context')
(Case' context context'
case case'))))
(implementation
(the (when_left [/#when /#some])
[#when (sum.either (|>> /#when (sum.then sum.left function.identity))
(|>> sum.right sum.left))
#some (|>> /#some sum.left)])
(the (when_right [/#when /#some])
[#when (sum.either (|>> sum.left sum.left)
(|>> /#when (sum.then sum.right function.identity)))
#some (|>> /#some sum.right)])))

(the .public (as_aspect [/#when /#some]
[pro_functor co_cartesian])
(for_any (_ context context' case case')
(-> (Case' context context' case case')
(Aspect context context' case case')))
(<| (with pro_functor)
(with co_cartesian)
(|>> when_right
(each /#when (sum.either function.identity /#some)))))

(the .public (of_aspect it)
(for_any (_ context context' case case')
(-> (Aspect context context' case case' (for_any (_ context context')
(Case' context context'
case case')))
(Case' context context' case case')))
(it [..functor ..co_cartesian]
[#when sum.right
#some function.identity]))
110 changes: 57 additions & 53 deletions stdlib/source/library/lux/aspect/property.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,56 +92,60 @@
#has (function (_ [focus context])
(revised outer (has inner focus) context))])

(comment
(every .public (Aspect external_cause external_effect internal_cause internal_effect)
(for_any (_ it)
(-> [(pro.Functor it) (pro.Cartesian it)]
(//.Aspect it external_cause external_effect internal_cause internal_effect))))

(the functor
(for_any (_ internal_cause internal_effect)
(pro.Functor (Property' internal_cause internal_effect)))
(implementation
(the (each before after [/#its /#has])
(..property' (|>> before
/#its)
(|>> (product.then function.identity before)
/#has
after)))))

(the cartesian
(for_any (_ internal_cause internal_effect)
(pro.Cartesian (Property' internal_cause internal_effect)))
(implementation
(the (in_left [/#its /#has])
(..property' (|>> product.left
/#its)
(product.forked (|>> (product.then function.identity product.left)
/#has)
(|>> product.right
product.right))))
(the (in_right [/#its /#has])
(..property' (|>> product.right
/#its)
(product.forked (|>> product.right
product.left)
(|>> (product.then function.identity product.right)
/#has))))))

(the .public (as_property [/#its /#has]
[pro_functor cartesian])
(for_any (_ internal_cause internal_effect external_cause external_effect)
(-> (Property' internal_cause internal_effect external_cause external_effect)
(Aspect internal_cause internal_effect external_cause external_effect)))
(<| (.with pro_functor)
(.with cartesian)
(|>> in_left
(each (product.forked /#its function.identity) /#has))))

(the .public (as_property' it)
(for_any (_ internal_cause internal_effect external_cause external_effect)
(-> (Aspect internal_cause internal_effect external_cause external_effect (Property' internal_cause internal_effect))
(Property' internal_cause internal_effect external_cause external_effect)))
(it [..functor ..cartesian]
..identity))
)
(every .public (Aspect context context' focus focus')
(for_any (_ it)
(-> [(pro.Functor it) (pro.Cartesian it)]
(//.Aspect it context context' focus focus'))))

(the functor
(for_any (_ focus focus')
(pro.Functor (for_any (_ context context')
(Property' context context'
focus focus'))))
(implementation
(the (each before after [/#its /#has])
[#its (|>> before
/#its)
#has (|>> (product.then function.identity before)
/#has
after)])))

(the cartesian
(for_any (_ focus focus')
(pro.Cartesian (for_any (_ context context')
(Property' context context'
focus focus'))))
(implementation
(the (in_left [/#its /#has])
[#its (|>> product.left
/#its)
#has (product.forked (|>> (product.then function.identity product.left)
/#has)
(|>> product.right
product.right))])
(the (in_right [/#its /#has])
[#its (|>> product.right
/#its)
#has (product.forked (|>> product.right
product.left)
(|>> (product.then function.identity product.right)
/#has))])))

(the .public (as_aspect [/#its /#has]
[pro_functor cartesian])
(for_any (_ context context' focus focus')
(-> (Property' context context' focus focus')
(Aspect context context' focus focus')))
(<| (with pro_functor)
(with cartesian)
(|>> in_left
(each (product.forked /#its function.identity) /#has))))

(the .public (of_aspect it)
(for_any (_ context context' focus focus')
(-> (Aspect context context' focus focus' (for_any (_ context context')
(Property' context context' focus focus')))
(Property' context context' focus focus')))
(it [..functor ..cartesian]
[#its function.identity
#has product.left]))
108 changes: 52 additions & 56 deletions stdlib/source/library/lux/aspect/view.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,51 +20,51 @@
.with_template))

(the As'
(macro (_ it it'
(macro (_ context context'
analogy analogy')
[(-> it'
analogy')]))
[(-> context
analogy)]))

(the Of'
(macro (_ it it'
(macro (_ context context'
analogy analogy')
[(-> analogy
it)]))
[(-> analogy'
context')]))

(every (View' it it'
(every (View' context context'
analogy analogy')
(Record
[#as (As' it it'
[#as (As' context context'
analogy analogy')
#of (Of' it it'
#of (Of' context context'
analogy analogy')]))

(the As
(macro (_ it analogy)
[(As' it it
(macro (_ context analogy)
[(As' context context
analogy analogy)]))

(the Of
(macro (_ it analogy)
[(Of' it it
(macro (_ context analogy)
[(Of' context context
analogy analogy)]))

(every .public (View it analogy)
(View' it it
(every .public (View context analogy)
(View' context context
analogy analogy))

(the .public (view as of)
(for_any (_ it analogy)
(-> (As it analogy) (Of it analogy)
(View it analogy)))
(for_any (_ context analogy)
(-> (As context analogy) (Of context analogy)
(View context analogy)))
[#as as
#of of])

(with_template [,name ,type ,tag]
[(the .public ,name
(for_any (_ it analogy)
(-> (View it analogy)
(,type it analogy)))
(for_any (_ context analogy)
(-> (View context analogy)
(,type context analogy)))
(.its ,tag))]

[as As #as]
Expand All @@ -76,38 +76,34 @@
(View it it))
(..view function.identity function.identity))

(comment
(every .public (Aspect it it' analogy analogy')
(for_any (_ it)
(-> (pro.Functor it)
(//.Aspect it it it' analogy analogy'))))

(the (as_aspect [/#as /#of]
[pro_functor])
(for_any (_ it it' analogy analogy')
(-> (View' it it' analogy analogy')
(Aspect it it' analogy analogy')))
(<| (.with pro_functor)
(each /#of /#as)))

(the functor
(for_any (_ it it')
(pro.Functor (View' it it')))
(implementation
(the (each before after [/#as /#of])
[#as (|>> /#as after)
#of (|>> before /#of)])))

(the .public identity'
(for_any (_ it)
(Aspect it it
it it))
(..as_aspect ..identity))

(the (of_aspect it)
(for_any (_ it it' analogy analogy')
(-> (Aspect it it' analogy analogy' (View' it it'))
(View' it it' analogy analogy')))
(it [..functor]
..identity))
)
(every .public (Aspect context context' analogy analogy')
(for_any (_ it)
(-> (pro.Functor it)
(//.Aspect it context context' analogy analogy'))))

(the functor
(for_any (_ analogy analogy')
(pro.Functor (for_any (_ context context')
(View' context context'
analogy analogy'))))
(implementation
(the (each before after [/#as /#of])
[#as (|>> before /#as)
#of (|>> /#of after)])))

(the .public (as_aspect [/#as /#of]
[pro_functor])
(for_any (_ context context' analogy analogy')
(-> (View' context context' analogy analogy')
(Aspect context context' analogy analogy')))
(<| (with pro_functor)
(each /#as /#of)))

(the .public (of_aspect it)
(for_any (_ context context' analogy analogy')
(-> (Aspect context context' analogy analogy' (for_any (_ context context')
(View' context context' analogy analogy')))
(View' context context' analogy analogy')))
(it [..functor]
[#as function.identity
#of function.identity]))
7 changes: 4 additions & 3 deletions stdlib/source/library/lux/data/sum.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,11 @@
["[0]" template]]]])

(template.with [<right?> <name>]
[(the .public (<name> value)
[(the .public <name>
(for_any (_ left right)
(-> <name> (Or left right)))
{<right?> value})]
(-> <name>
(Or left right)))
(|>> {<right?>}))]

[#0 left]
[#1 right])
Expand Down
12 changes: 12 additions & 0 deletions stdlib/source/library/lux/function.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,3 +61,15 @@
(the (in_right it)
(function (_ [extra cause])
[extra (it cause)]))))

(the .public co_cartesian
(pro.Co_Cartesian Function)
(implementation
(the (when_left it left|right)
(when left|right
{#0 left} {#0 (it left)}
{#1 right} {#1 right}))
(the (when_right it left|right)
(when left|right
{#0 left} {#0 left}
{#1 right} {#1 (it right)}))))

0 comments on commit 54ddea9

Please sign in to comment.