Skip to content

Commit

Permalink
Pro-functor lenses (part 4 of optics).
Browse files Browse the repository at this point in the history
  • Loading branch information
@eduardoejp
eduardoejp committed May 13, 2024
1 parent 2308e87 commit 3812076
Show file tree
Hide file tree
Showing 6 changed files with 259 additions and 52 deletions.
26 changes: 26 additions & 0 deletions stdlib/source/library/lux/abstract/functor/pro.lux
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
... 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)]])

(every .public (Functor it)
(Interface
(is (for_any (_ cause effect
cause' effect')
(-> (-> cause' cause) (-> effect effect')
(-> (it cause effect)
(it cause' effect'))))
each)))

(every .public (Cartesian it)
(Interface
(is (for_any (_ cause effect extra)
(-> (it cause effect)
(it (And cause extra) (And effect extra))))
in_left)
(is (for_any (_ cause effect extra)
(-> (it cause effect)
(it (And extra cause) (And extra effect))))
in_right)))
41 changes: 33 additions & 8 deletions stdlib/source/library/lux/function.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,34 +5,59 @@
[library
[lux (.except)
[abstract
[monoid (.only Monoid)]]]])
[monoid (.only Monoid)]
[functor
["[0]" pro]]]]])

(the .public identity
(for_any (_ a) (-> a a))
(for_any (_ it)
(-> it
it))
(|>>))

(the .public (composite f g)
(for_any (_ a b c)
(-> (-> b c) (-> a b) (-> a c)))
(|>> g f))

(the .public monoid
(for_any (_ it)
(Monoid (-> it it)))
(implementation
(the identity ..identity)
(the composite ..composite)))

(the .public (constant value)
(for_any (_ o) (-> o (for_any (_ i) (-> i o))))
(function (_ _) value))

(the .public (flipped f)
(for_any (_ a b c)
(-> (-> a b c) (-> b a c)))
(-> (-> a b c)
(-> b a c)))
(function (_ x y) (f y x)))

(the .public (on input function)
(for_any (_ i o)
(-> i (-> i o) o))
(function input))

(the .public monoid
(for_any (_ a)
(Monoid (-> a a)))
(every .public (Function cause effect)
(-> cause
effect))

(the .public pro_functor
(pro.Functor Function)
(implementation
(the identity ..identity)
(the composite ..composite)))
(the (each before after it)
(|>> before it after))))

(the .public cartesian
(pro.Cartesian Function)
(implementation
(the (in_left it)
(function (_ [cause extra])
[(it cause) extra]))
(the (in_right it)
(function (_ [extra cause])
[extra (it cause)]))))
111 changes: 87 additions & 24 deletions stdlib/source/library/lux/optic.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,13 @@
when
all with)
[abstract
[functor (.only Functor)]]
[functor (.only Functor)
["[0]" pro]]]
[type
["[0]" nominal]]
["[0]" function]]])
["[0]" function]
[data
["[0]" product]]]])

(the macro
(<| (.in_module# .prelude)
Expand All @@ -23,49 +26,53 @@
.with_template))

(the Its
(macro (_ context focus)
(macro (_ focus focus' context context')
[(-> context
focus)]))

(the Has
(macro (_ context focus)
[(-> [focus context]
context)]))
(macro (_ focus focus' context context')
[(-> [focus' context]
context')]))

(every .public (Lens context focus)
(every .public (Lens focus focus' context context')
(Record
[#its (Its context focus)
#has (Has context focus)]))
[#its (Its focus focus' context context')
#has (Has focus focus' context context')]))

(the .public (lens its has)
(for_any (_ context focus)
(-> (Its context focus) (Has context focus)
(Lens context focus)))
(for_any (_ focus focus' context context')
(-> (Its focus focus' context context') (Has focus focus' context context')
(Lens focus focus' context context')))
[#its its
#has has])

(the .public its
(for_any (_ context focus)
(-> (Lens context focus)
(Its context focus)))
(for_any (_ focus focus' context context')
(-> (Lens focus focus' context context')
(Its focus focus' context context')))
(.its #its))

(the .public (has lens value context)
(for_any (_ context focus)
(-> (Lens context focus) focus
(Change context)))
(for_any (_ focus focus' context context')
(-> (Lens focus focus' context context')
(-> focus'
(-> context context'))))
(by lens #has [value context]))

(the .public (revised lens change context)
(for_any (_ context focus)
(-> (Lens context focus) (Change focus)
(Change context)))
(for_any (_ focus focus' context context')
(-> (Lens focus focus' context context')
(-> (-> focus focus')
(-> context context'))))
(by lens #has [(change (its lens context)) context]))

(the .public (composite outer inner)
(for_any (_ outermost middle innermost)
(-> (Lens outermost middle) (Lens middle innermost)
(Lens outermost innermost)))
(for_any (_ focus focus'
middle middle'
context context')
(-> (Lens middle middle' context context') (Lens focus focus' middle middle')
(Lens focus focus' context context')))
[#its (|>> (its outer)
(its inner))
#has (function (_ [focus context])
Expand Down Expand Up @@ -223,3 +230,59 @@
(every .public (Member all one)
(-> all
(Membership one all)))

(every .public (Optic it cause effect cause' effect')
(-> (it cause effect)
(it cause' effect')))

(every .public (Property cause effect cause' effect')
(for_any (_ it)
(-> [(pro.Functor it) (pro.Cartesian it)]
(Optic it cause effect cause' effect'))))

(the .public pro_functor_of_lens
(for_any (_ cause effect)
(pro.Functor (Lens cause effect)))
(implementation
(the (each before after [/#its /#has])
(..lens (|>> before
/#its)
(|>> (product.then function.identity before)
/#has
after)))))

(the .public cartesian_of_lens
(for_any (_ cause effect)
(pro.Cartesian (Lens cause effect)))
(implementation
(the (in_left [/#its /#has])
(..lens (|>> product.left
/#its)
(product.forked (|>> (product.then function.identity product.left)
/#has)
(|>> product.right
product.right))))
(the (in_right [/#its /#has])
(..lens (|>> 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 (_ cause effect cause' effect')
(-> (Lens cause effect cause' effect')
(Property cause effect cause' effect')))
(<| (.with pro_functor)
(.with cartesian)
(|>> in_left
(each (product.forked /#its function.identity) /#has))))

(the .public (as_lens it)
(for_any (_ cause effect cause' effect')
(-> (Property cause effect cause' effect' (Lens cause effect))
(Lens cause effect cause' effect')))
(it [..pro_functor_of_lens ..cartesian_of_lens]
(..lens function.identity product.left)))
76 changes: 76 additions & 0 deletions stdlib/source/test/lux/abstract/functor/pro.lux
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
... 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)
[abstract
[equivalence (.only Equivalence)]
[monad (.only do)]]
["[0]" function]
[math
["[0]" random (.only Random)]
[number
["[0]" natural]]]
[test
["_" property (.only Test)]]]]
[\\library
["[0]" /]])

(every .public (Specification it)
(-> it
Test))

(the .public (specification concrete random
functor)
(for_any (_ it)
(-> (-> (it Natural Natural)
(-> Natural Natural))
(Random (it Natural Natural))
(Specification (/.Functor it))))
(<| (do [! random.monad]
[cause random.natural
it random])
(_.for [/.Functor])
(_.coverage [/.each]
(let [it' (by functor each
function.identity
function.identity
it)

identity!
(by natural.equivalence =
((concrete it) cause)
((concrete it') cause))

before_0 (is (Change Natural)
++)
before_1 (is (Change Natural)
(natural.* 2))

after_0 (is (Change Natural)
--)
after_1 (is (Change Natural)
(natural.* 3))

left
(by functor each
(|>> before_0 before_1)
(|>> after_1 after_0)
it)

right
(<| (by functor each
before_0
after_0)
(by functor each
before_1
after_1)
it)

composite!
(by natural.equivalence =
((concrete left) cause)
((concrete right) cause))]
(and identity!
composite!)))))
17 changes: 16 additions & 1 deletion stdlib/source/test/lux/function.lux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@
[equivalence (.only Equivalence)]
[monad (.only do)]
["[0]" monoid
["[1]T" \\test]]]
["[1]T" \\test]]
[functor
["[0]" pro
["[1]T" \\test]]]]
[math
["[0]" random (.only Random)]
[number
Expand Down Expand Up @@ -73,6 +76,18 @@
(_.coverage [/.on]
(n.= (f0 extra)
(/.on extra f0)))
... (<| (_.for [/.Function])
... (all _.and
... (_.for [/.pro_functor]
... (let [as_function (is (-> (/.Function Natural Natural)
... (-> Natural Natural))
... (function (_ it cause)
... (it cause)))]
... (proT.specification as_function
... (is (Random (/.Function Natural Natural))
... (in ++))
... /.pro_functor)))
... ))

/contract.test
/memo.test
Expand Down
Loading

0 comments on commit 3812076

Please sign in to comment.