-
-
Notifications
You must be signed in to change notification settings - Fork 53
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Splitting the optics, and re-named to
Aspect
s (part 6 of optics).
- Loading branch information
1 parent
4007d73
commit 93f356d
Showing
11 changed files
with
740 additions
and
547 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,114 @@ | ||
... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. | ||
... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. | ||
|
||
(.using | ||
[library | ||
[lux (.except macro | ||
all with) | ||
[abstract | ||
[functor (.only Functor) | ||
["[0]" pro]]] | ||
[type | ||
["[0]" nominal]] | ||
["[0]" function] | ||
[data | ||
["[0]" product]]]]) | ||
|
||
(the macro | ||
(<| (.in_module# .prelude) | ||
.template#macro)) | ||
|
||
(the with_template | ||
(<| (.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))) | ||
|
||
... TODO: Make this nominal type unnecessary. | ||
(nominal.every .public (Membership one all) | ||
(Variant | ||
{#All all} | ||
{#One one (Membership one (-> one all))}) | ||
|
||
(the outer | ||
(for_any (_ one all) | ||
(-> (Membership one all) | ||
(Or all (And one (Membership one (-> one all)))))) | ||
(|>> nominal.reification)) | ||
|
||
(the inner | ||
(for_any (_ one all) | ||
(-> (Or all (And one (Membership one (-> one all)))) | ||
(Membership one all))) | ||
(|>> nominal.abstraction)) | ||
|
||
(the .public membership_functor | ||
(for_any (_ one) | ||
(Functor (Membership one))) | ||
(implementation | ||
(the (each value it) | ||
(nominal.abstraction | ||
(.when (nominal.reification it) | ||
{#All all} | ||
{#All (value all)} | ||
|
||
{#One one next} | ||
{#One one (each (function (_ before) | ||
(|>> before | ||
value)) | ||
next)})) | ||
))) | ||
|
||
(every .public (Apply context) | ||
(Interface | ||
(is (Functor context) | ||
functor) | ||
(is (for_any (_ it) | ||
(-> it | ||
(context it))) | ||
pure) | ||
(is (for_any (_ it it') | ||
(-> (context (-> it it')) | ||
(-> (context it) | ||
(context it')))) | ||
with))) | ||
|
||
(the .public membership_apply | ||
(for_any (_ one) | ||
(Apply (Membership one))) | ||
(implementation | ||
(the functor ..membership_functor) | ||
(the pure (|>> {#All} nominal.abstraction)) | ||
(the (with internal_effect internal_cause) | ||
(.when (nominal.reification internal_effect) | ||
{#All internal_effect} | ||
(by ..membership_functor each internal_effect internal_cause) | ||
|
||
{#One one internal_effect} | ||
(nominal.abstraction | ||
{#One one (with (by ..membership_functor each function.flipped internal_effect) | ||
internal_cause)}))))) | ||
|
||
(the .public (one it) | ||
(for_any (_ it) | ||
(-> it | ||
(Membership it it))) | ||
(nominal.abstraction {#One it (nominal.abstraction {#All (|>>)})})) | ||
|
||
(the .public (all it) | ||
(for_any (_ one all) | ||
(-> (Membership one all) | ||
all)) | ||
(.when (nominal.reification it) | ||
{#All it} | ||
it | ||
|
||
{#One one next} | ||
((all next) one))) | ||
|
||
(every .public (Member all one) | ||
(-> all | ||
(Membership one all))) | ||
) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,65 @@ | ||
... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. | ||
... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. | ||
|
||
(.using | ||
[library | ||
[lux (.except macro | ||
when)]]) | ||
|
||
(the macro | ||
(<| (.in_module# .prelude) | ||
.template#macro)) | ||
|
||
(the with_template | ||
(<| (.in_module# .prelude) | ||
.with_template)) | ||
|
||
(the When' | ||
(macro (_ context context' | ||
case case') | ||
[(-> context | ||
(Or context' case))])) | ||
|
||
(the Some' | ||
(macro (_ context context' | ||
case case') | ||
[(-> case' | ||
context')])) | ||
|
||
(every (Case' context context' | ||
case case') | ||
(Record | ||
[#when (When' context context' case case') | ||
#some (Some' context context' case case')])) | ||
|
||
(the When | ||
(macro (_ context case) | ||
[(When' context context | ||
case case)])) | ||
|
||
(the Some | ||
(macro (_ context case) | ||
[(Some' context context | ||
case case)])) | ||
|
||
(every .public (Case context case) | ||
(Case' context context | ||
case case)) | ||
|
||
(the .public (case when some) | ||
(for_any (_ context case) | ||
(-> (When context case) (Some context case) | ||
(Case context case))) | ||
[#when when | ||
#some some]) | ||
|
||
(with_template [,name ,type ,tag] | ||
[(the .public ,name | ||
(for_any (_ context case) | ||
(-> (Case context case) | ||
(,type context case))) | ||
(.its ,tag))] | ||
|
||
[when When #when] | ||
[some Some #some] | ||
) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,147 @@ | ||
... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. | ||
... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. | ||
|
||
(.using | ||
[library | ||
[lux (.except macro | ||
its revised has) | ||
[abstract | ||
[functor | ||
["[0]" pro]]] | ||
["[0]" function] | ||
[data | ||
["[0]" product]]]] | ||
["[0]" //]) | ||
|
||
(the macro | ||
(<| (.in_module# .prelude) | ||
.template#macro)) | ||
|
||
(the Its' | ||
(macro (_ context context' | ||
focus focus') | ||
[(-> context | ||
focus)])) | ||
|
||
(the Has' | ||
(macro (_ context context' | ||
focus focus') | ||
[(-> [focus' context] | ||
context')])) | ||
|
||
(every (Property' context context' | ||
focus focus') | ||
(Record | ||
[#its (Its' context context' | ||
focus focus') | ||
#has (Has' context context' | ||
focus focus')])) | ||
|
||
(the Its | ||
(macro (_ context focus) | ||
[(Its' context context | ||
focus focus)])) | ||
|
||
(the Has | ||
(macro (_ context focus) | ||
[(Has' context context | ||
focus focus)])) | ||
|
||
(every .public (Property context focus) | ||
(Property' context context | ||
focus focus)) | ||
|
||
(the .public (property its has) | ||
(for_any (_ context focus) | ||
(-> (Its context focus) (Has context focus) | ||
(Property context focus))) | ||
[#its its | ||
#has has]) | ||
|
||
(the .public identity | ||
(for_any (_ it) | ||
(Property it it)) | ||
(property function.identity product.left)) | ||
|
||
(the .public its | ||
(for_any (_ context focus) | ||
(-> (Property context focus) | ||
(Its context focus))) | ||
(.its #its)) | ||
|
||
(the .public (has property value context) | ||
(for_any (_ context focus) | ||
(-> (Property context focus) | ||
(-> focus | ||
(Change context)))) | ||
(by property #has [value context])) | ||
|
||
(the .public (revised property change context) | ||
(for_any (_ context focus) | ||
(-> (Property context focus) | ||
(-> (Change focus) | ||
(Change context)))) | ||
(by property #has [(change (its property context)) context])) | ||
|
||
(the .public (composite outer inner) | ||
(for_any (_ focus middle context) | ||
(-> (Property context middle) (Property middle focus) | ||
(Property context focus))) | ||
[#its (|>> (its outer) | ||
(its inner)) | ||
#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)) | ||
) |
Oops, something went wrong.