Added member (a.k.a. Traversal) (part 3 of optics).

stdlib/source/library/lux/optic.lux

@@ -6,7 +6,13 @@
   [lux (.except macro
                 its revised has
                 as
-                when)]])
+                when
+                all with)
+   [abstract
+    [functor (.only Functor)]]
+   [type
+    ["[0]" nominal]]
+   ["[0]" function]]])
 
 (the macro
   (<| (.in_module# .prelude)
@@ -130,3 +136,90 @@
   [when When #when]
   [some Some #some]
   )
+
+... 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 effect cause)
+       (.when (nominal.reification effect)
+         {#All effect}
+         (by ..membership_functor each effect cause)
+
+         {#One one effect}
+         (nominal.abstraction
+          {#One one (with (by ..membership_functor each function.flipped effect)
+                      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)))

stdlib/source/library/lux/type/check.lux

@@ -9,11 +9,13 @@
     [functor (.only Functor)]
     [monad (.only Monad do)]]
    [control
-    ["[0]" maybe]]
+    ["[0]" maybe]
+    ["[0]" state]]
    [error
     ["[0]" try (.only Try) (.use "[1]#[0]" functor)]
     ["[0]" exception (.only Exception)]]
    [function
+    [predicate (.only Predicate)]
     ["[0]" mixin (.only Mixin)]]
    [data
     ["[0]" product]
@@ -24,7 +26,8 @@
      ["[0]" set (.only Set)]]]
    [math
     [number
-     ["n" natural (.use "[1]#[0]" base_10)]]]
+     ["n" natural (.use "[1]#[0]" base_10)]
+     ["[0]" i64]]]
    [macro
     ["^" pattern]
     ["[0]" template]]]]
@@ -48,39 +51,16 @@
    (list ["Super type" (//.absolute_text super)]
          ["Sub type" (//.absolute_text sub)])))
 
-(every .public (Check it)
-  (-> Type_Context
-      (Try [Type_Context it])))
-
-(the .public functor
-  (Functor Check)
-  (implementation
-   (the (each f fa)
-     (function (_ context)
-       (when (fa context)
-         {try.#Success [context' output]}
-         {try.#Success [context' (f output)]}
-
-         {try.#Failure error}
-         {try.#Failure error})))))
+(every .public Check
+  (state.With Type_Context Try))
 
 (the .public monad
   (Monad Check)
-  (implementation
-   (the functor ..functor)
-
-   (the (in x)
-     (function (_ context)
-       {try.#Success [context x]}))
+  (state.with try.monad))
 
-   (the (conjoint ffa)
-     (function (_ context)
-       (when (ffa context)
-         {try.#Success [context' fa]}
-         (fa context')
-
-         {try.#Failure error}
-         {try.#Failure error})))))
+(the .public functor
+  (Functor Check)
+  (by ..monad functor))
 
 (use "/#[0]" ..monad)
 
@@ -617,6 +597,25 @@
   (.type (-> [(List Hypothesis) Type Type]
              (Check (List Hypothesis)))))
 
+(the limit (i64.left_shifted 7 1))
+
+(the not_too_many?
+  (Predicate (List Hypothesis))
+  (|>> list.size
+       (n.< ..limit)))
+
+(the (hypothesis_as_text it)
+  (text.Injection Hypothesis)
+  (text (//.as_text (its #super it))
+        " = "
+        (//.as_text (its #sub it))))
+
+(exception.the .public (too_many_hypotheses [it])
+  (Exception [(List Hypothesis)])
+  (exception.report
+   (list ["Limit" (n#as limit)]
+         ["Hypotheses" (exception.listing ..hypothesis_as_text it)])))
+
 (the (super_reification complete hypotheses super_parameter super_abstraction sub)
   (-> Complete_Subsumption
       (List Hypothesis) Type Type Type
@@ -625,9 +624,14 @@
                         #sub sub]]
     (if (hypothesized? new_hypothesis hypotheses)
         (/#in hypotheses)
+
+        (not_too_many? hypotheses)
         (do ..monad
           [super' (..on (list super_parameter) super_abstraction)]
-          (complete [(list#composite (list new_hypothesis) hypotheses) super' sub])))))
+          (complete [(list#composite (list new_hypothesis) hypotheses) super' sub]))
+
+        ... else
+        (..except ..too_many_hypotheses [hypotheses]))))
 
 (the (opaque_reification complete hypotheses
                          [super_quantification super_parameters]

stdlib/source/test/lux/optic.lux

@@ -153,6 +153,27 @@
                    {.#Left it})))
            integer.decimal))
 
+(every (Tree it)
+  (Variant
+   {#Leaf}
+   {#Branch (Tree it) it (Tree it)}))
+
+(the (in_order it)
+  (for_any (_ it)
+    (/.Member (Tree it) it))
+  (<| (with /.membership_apply)
+      (when it
+        {#Leaf}
+        (pure {#Leaf})
+
+        {#Branch left it right}
+        (left_associative with
+                          (pure (function (_ left it right)
+                                  {#Branch left it right}))
+                          (in_order left)
+                          (/.one it)
+                          (in_order right)))))
+
 (the .public test
   Test
   (<| (_.covering /._)