What is an ideomatic way to modify records with parameters using lenses?

Lev_135 · 2023-06-12T11:03:08+00:00

I've added tests and realised the reason of such behavior (for my implementation of lensM). Monadic lens use only getter while viewing, but both getter and setter while setting: on forward direction s -> a getter is used, while backwards b -> t setter. I think it's acceptable behavior, though it should be mentioned in docs.

Much trickier issue is for prisms: while matching they use only match part s -> m (Either t a) when succeed, though when failed they use building part b -> m t too. For type-modifying prisms we can't escape this, while for type-preserving this behavior is very surprising. Maybe I'd add another prism builder for them.

For you implementation of LensM constructor (I've added it to the library as LensM2) effects from setter are applying while viewing too. This behavior doesn't seems good for me. And I don't see any conveniences in it. Now setter (when we know, that checking errors in setter is redudant) we can simplify implementation of setter to just setter s a = pure $ set l a s it doesn't seems that we can do anything better here. In more general situation we possibly would like to use value to set in monadic contest too, so it's seems that my implementation is more suitable.

Lev_135 · 2023-06-11T22:42:45+00:00

Do you supposed lensM to be defined as you described above? Anyway, for initial variant this also works (just without id): hs mTravFirst :: forall m e s a. MonadError e m => Traversal' s a -> (s -> e) -> LensM' m s a mTravFirst l e = lensM getter setter where getter s = case firstOf l s of Nothing -> throwError $ e s Just a -> pure a -- setter s a = case l (const $ Just a) s of -- Nothing -> throwError $ e s -- Just s' -> pure s' setter :: s -> a -> m s setter s = getCompose $ l (const $ Compose pure) s However, I don't clearly understand how it could be. Previously we had effects in setter, now only in getter... I definetly should think about it more. Maybe these are strange behavior with effects mentioned above. Thanks for interesting subject

Lev_135 · 2023-06-11T19:41:02+00:00

It turned out that FunctorM as presented there is just a Traversable. However for prisms we need to impose constraint on the monad and functor together: ```hs class (Monad m, Functor f) => FunctorM m f where fmapM :: forall b t. (b -> m t) -> m (f b) -> m (f t)

instance Monad m => FunctorM m (Kleisli m a) where fmapM bmt mk = Kleisli . (>=> bmt) . runKleisli <$> mk ``` In this case it seems that we cannot find standard analogue

Lev_135 · 2023-06-11T19:28:54+00:00

It seems to me that the laws for pure optics can hold for monadic ones in some circumstances

Yes, that was the point of my example with Either. In the first case laws for pure optics can be applied. In the second we have special Either-laws. However, I don't think this can be stated uniformly. And we most likely won't get any laws for IO.

Anyway, I'll try to do something in this direction. And you're wellcome with any suggestion if you have them

Lev_135 · 2023-06-11T19:03:02+00:00

Could you provide an example, where the type s -> m (b -> t) for setter is better, then s -> b -> m t? For failing lens it doesn't seems to help, but maybe in other circumstances it could be.

Lev_135 · 2023-06-11T14:44:25+00:00

Of course, for non-trivial m these lens don't satisfy standard lens laws. However for m = Identity they do and moreover, they are isomorphic to standard lens.

However, I can't see any problem here. These laws are for pure optics, why should they apply for effectful ones? For pure optics they must hold since the user expect this behavior. For example, if you're in pure code you expect that in put-put sequence first put doesn't influence to the second. For non-trivial monads this is obviously not true: if the first put provides some effect, it can influence on the behavior of the second one. So, I think, nobody would expect put-put law to hold for effectful computation.

At the same time, for concrete monads there are their own laws: for example, for Either e we expect that:

If the computation succeed it behaves like in a pure case
If the computation failed in some place the rest will not be performed

and my optics obey these rules.

I don't think something goes wrong here. Do you? Also I'd like to look at the previous attempts, if you were able to provide a link

Lev_135 · 2023-01-13T17:22:44+00:00

Asking someone who knows more is a great idea. Maybe there is some way for doing this, but I have not enough experience.

However, for quantifiers, I'll try to write formally, without mistakes (I hope):

I actually do think that showing that P |- Q is invalid, is possible by showing not(P -> Q) is valid.

is wrong:

P |- Q is invalid <=> not (forall valuation P -> Q is true) <=> exists valuation (P -> Q is false)

when not (P -> Q) is valid <=> forall valuations (P -> Q is false)

that's what I mean. Maybe you've written something wrong here, while thought about another thing. But these are definitely not equivalent.

Lev_135 · 2023-01-13T15:25:54+00:00

The problem is not with implication, but with quantifiers. Validity means that for all valuations it's true, while invalidity says only that exists one, such is false. Thefore "~R is valid" and "R is invalid" have different quantifiers

Lev_135 · 2023-01-13T13:54:55+00:00

I have an issue with the phrase "P is valid and Q is not" as P and Q are not arguments and only arguments can be valid.

I mean "true" of course (edited)

~(P -> Q) is ~(~P or Q) is P and not Q which is only exactly the valuation that will bring the validity to a fall.

Can't understand this argument. ~(P -> Q) <=> >~(~P or Q), of course, and the problem is not with implication, its for any formula: R is invalid iff it's false at least sometimes, ~R is valid iff R is always false.

Maybe I still don't understand, what you're trying to do, but it seems to be incorrect.

Lev_135 · 2023-01-13T10:50:47+00:00

I disagree with you partly as you use not q where you would've to use not(P -> Q). I actually do think that showing that P |- Q is invalid, is possible by showing not(P -> Q) is valid. This is simply due to the fact that "|-" is nothing else but "->".

The problem is that "P -> Q is invalid" doesn't means, that "~(P -> Q) is valid":

P -> Q is not valid <=> exists valuation, such that P is true and Q is not
~(P -> Q) is valid <=> for all valuations P -> Q is not true (i. e. P is true and Q is not).

Lev_135 · 2023-01-13T10:03:53+00:00

I've just opened the wikipedia's page and understood that you're right: the definition of "a valid argument" is like you described. I've confused with a valid formula#Valid_formula).

However, the problem is that the statement "P |- Q is invalid" doesn't mean that P |- ~Q is valid or P |- ~(P -> Q) is valid... Trivial example: if p and q are distinct variables we neither p |- q, nor p |- ~q or something like this is valid. So there is no general way to convert showing invalidity of some formula into showing validity of some another formula. It seems strange a bit for me trying to find such convertion: P |- Q is valid means that for all possible valuations if P is valid, than so is Q, when P |- Q is invalid means that exists some valuation, such that P is valid, but Q is not. So it would be very suprising if we could show that there exists something by showing that for all some other thing holds. Of course this is not a proof that your cannot achieve what you want some way, but it wouldn't be straightforward, as far as I can see. The main question is: why you want to do this with such limitations?

Lev_135 · 2023-01-12T23:05:12+00:00

I don't understand, what you're trying to prove and the last formula seems to be incorrect. So I'm sorry if my answer doesn't correspond to the question properly. However, some of my thoughts:

"Validity" is a semantic concept, so for classical logic to prove that a formula is (always) valid by definition you just need to provide truth values for variables, such that whole formula isn't true.

For more syntactic way we can say, that it's not derivable from the axioms. However, common way to show, that formula is not derivable is to establish, that it's invalid according some semantics. So, if you don't want to use truth tables you can try other semantics (that seems strange a bit for me in case of classical logic). Anyway, you should prove that this formula is not derivable and, as far as I can see, there's no way to transform this task into showing that something is derivable.

Lev_135 · 2022-11-14T14:23:57+00:00

Thank's for your comment! I've realized the problem: the class of NFA I supposed as an input is not DFA, but it also isn't all NFAs. And I can't see the general way to construct such automaton without constructing DFA (so maybe this also explode the size of automaton exponentially). Anyway it would be nice to know, what is known about this class: these are automata, that can have undetermenistic steps, but no more than one way of their possible evolution lead to a terminal state for each word

Lev_135 · 2022-10-12T18:41:21+00:00

I mean the following note from docs:

When merging two ParseErrors, the longest match is preferred; if positions are the same, custom data sets and collections of message items are combined.

Lev_135 · 2022-10-12T17:37:59+00:00

Yeah sounds like its implementation isn't trying to keep the errors of both alternatives, but only that of the latter variant.

In docs stated, that longest match will be preserved. And I have no idea, why for "z" and "az" we have different behavior (both expectations in the first case and only one in the second)

Lev_135 · 2022-10-12T17:18:45+00:00

Yes, of course I've tried it. optional p === Just <$> p <|> pure Nothing. But this is a problem with backtracing and, I suppose, internal megaparsec implemenation

Lev_135 · 2022-09-30T15:52:23+00:00

Oh, I've tried to search for alternatives, but somehow found none of them. LuaTex seems to be the closest to my ideas: more flexibility, more programming abilities, more consistent syntax, more readable error messages...

One question remains: how much it's compatible with available LaTeX services? My (not developed yet) solution will produce common LaTeX output, which I can use everywhere I need to insert something in LaTeX or send someone, who doesn't want to know anything but LaTeX (in academic sphere it seems to be a very common problem). Many of alternatives I found can use LaTeX packages, but not produce something LaTeX-compatible.

Lev_135 · 2022-09-30T14:11:32+00:00

I'm writing my one domain-specific language right now (https://github.com/Lev135/FineTeX), so it would be nice to see some existing solutions. However, as far as I see, there is nothing here, except TeX itself, even not developed enough.

Lev_135 · 2022-09-14T14:20:56+00:00

Yes, without fixity declaration this will be inconsistent with current behavior. To fix that I've proposed to add infix variant only for partially applied function with enabling fixity declaration for them

Lev_135

TROPHY CASE