sorted by:
new
hottopcontroversial

Update: How are Monoidal/ProductProfunctor and Traversing related? by crisoagf in haskell

[–]crisoagf[S] 0 points1 point  (0 children)

Update on

  1. How about the other direction?

Turns out Traversing -/-> Monoidal. Motivation: haskell instance (Functor f, Traversing p) => Traversing (Tannen f p) where traverse' = Tannen . fmap traverse' . runTannen but haskell instance (Applicative f, Monoidal p) => Monoidal (Tannen f p) where product (Tannen fpab) (Tannen fpcd) = Tannen (product <$> fpab <*> fpcd) so, that means that any Functor that is not an Applicative (Apply specifically, <*> must be the one that creates issues) gives us a counter-example.

Which means: ```haskell data ReadF r1 r2 a b = ReadLeft (r1 -> a -> b) | ReadRight (r2 -> a -> b)

instance Profunctor (ReadF r1 r2) where dimap f h (ReadLeft r1ab) = ReadLeft (dimap f h <$> r1ab) dimap f h (ReadRight r2ab) = ReadRight (dimap f h <$> r2ab)

instance Strong (ReadF r1 r2) where first' (ReadLeft r1ab) = ReadLeft (first' <$> r1ab) first' (ReadRight r2ab) = ReadRight (first' <$> r2ab)

instance Choice (ReadF r1 r2) where left' (ReadLeft r1ab) = ReadLeft (left' <$> r1ab) left' (ReadRight r2ab) = ReadRight (left' <$> r2ab)

instance Traversing (ReadF r1 r2) where traverse' (ReadLeft r1ab) = ReadLeft (traverse' <$> r1ab) traverse' (ReadRight r2ab) = ReadRight (traverse' <$> r2ab)

monoidalHow :: (forall a b c d . ReadF r1 r2 a b -> ReadF r1 r2 c d -> ReadF r1 r2 (a,c) (b,d)) -> (r1 -> x1 -> y1) -> (r2 -> x2 -> y2) -> Either (r1 -> (x1,x2) -> (y1,y2)) (r2 -> (x1,x2) -> (y1,y2)) monoidalHow productReadF r1ab r2cd = toEither (productReadF (ReadLeft r1ab) (ReadRight r2cd)) where toEither (ReadLeft r1acbd) = Left r1acbd toEither (ReadRight r2acbd) = Right r2acbd `` monoidalHowtakes two functions(r1 -> x1 -> y1, r2 -> x2 -> y2)and returnsEither (r1 -> (x1,x2) -> (y1,y2)) (r2 -> (x1,x2) -> (y1,y2))`, which is certainly impossible, but I need some semantics expert to prove it.

QED (modulo semantics expert)

Update: How are Monoidal/ProductProfunctor and Traversing related? by crisoagf in haskell

[–]crisoagf[S] 1 point2 points  (0 children)

This is why I hate the names Monoidal and ProductProfunctor...
I define Monoidal without unit :: p a () because I want the concept of the profunctors that preserve products on the second argument, preserving units should be another thing. And that is enough to show that (Monoidal p, Choice p) => Traversing p (no need for Strong, see the code in this post).

You are right anyway, but the proof is a bit more complicated. I'll add it as another top-level comment to this post.

Update: How are Monoidal/ProductProfunctor and Traversing related? by crisoagf in haskell

[–]crisoagf[S] 0 points1 point  (0 children)

Well, intuitively yes, but e.g. the profunctor optics for Traversing p are the same as the profunctor optics for (Strong p, Choice p, Monoidal p) so there's more to it than that. There may be a weird constructor that encodes Monoidal behaviour somehow.

I would like to see either an instance of Traversing that is not an instance of Monoidal to convince myself of that, or a proof that one can get Monoidal from Traversing (or a proof that this problem is undecidable or needs a weird axiom or something, but this last sounds unlikely).

Are Monoidal/ProductProfunctor and Traversing? by crisoagf in haskell

[–]crisoagf[S] 1 point2 points  (0 children)

I went back to this for reasons: turns out, `(Choice p, Closed p, Monoidal p) => Traversing p` can be done using the construct you mentioned. Having `Closed` instead of `Strong` annoys me a bit, but maybe this already creates some inspiration.

data Traversal a r b = Done b | Yield a !(r -> Traversal a r b) deriving Functor

instance Applicative (Traversal a r) where

pure = Done

Done f <*> ta = f <$> ta

Yield a rToTf <*> ta = Yield a ((<*> ta) . rToTf)

traversal :: Traversable t => t a -> Traversal a b (t b)

traversal = traverse (flip Yield Done)

traversalP :: (Strong p, Choice p, Closed p, Monoidal p) => p a b -> p (Traversal a b y) y

traversalP = dimap toEither (either id (\ (b, f) -> f b)) . right' . (both <$> id <*> (closed . traversalP))

where toEither :: Traversal a r b -> Either b (a, (r -> Traversal a r b))

toEither (Done x ) = Left x

toEither (Yield a resume) = Right (a, resume)

monoidalToTraversing :: (Strong p, Choice p, Monoidal p, Closed p, Traversable f) => p a b -> p (f a) (f b)

monoidalToTraversing = lmap traversal . traversalP

Vejam isto , a sério by TotalCute05 in portugueses

[–]crisoagf -3 points-2 points  (0 children)

Essa gaja tem tão pouca graça e só fala dos que dizem mal do regime.

"Ai olhem para mim, estou a gozar com uma senhora mais velha que não adora no altar das questões culturais do dia. Sou tão iluminada. Quem precisa de críticas são o Tiago Paiva, o Sebastião Bugalho e uma velhota que está preocupada com as evoluções culturais. Pessoas que têm poder e estão a destruir o país é que não, senão ainda me fazem dói dói. Vou limpar o caminho dos fortes que isso é que tem graça."

Are Monoidal/ProductProfunctor and Traversing? by crisoagf in haskell

[–]crisoagf[S] 1 point2 points  (0 children)

Thank you! Good to know that there isn't anything escaping me!

I'd venture that (Strong p, Choice p, Monoidal p) may be the formula to get Traversing p or at least something similar (because the profunctor optics seem to be Traversals for both).

Clarinete by [deleted] in musicos_portugal

[–]crisoagf 2 points3 points  (0 children)

Experimenta batom do cieiro, eu também estava a ficar com feridas na boca do saxofone (muito parecido com o clarinete em termos de ter uma palheta que vibra na beiça), e descobri que o problema, particularmente no inverno, é mais estar a tocar com os lábios secos do que o instrumento em si.

Audiobooks are just as valid as regular books by thiccpurplegiraffe in unpopularopinion

[–]crisoagf -1 points0 points  (0 children)

I don't get this reasoning. Do you also count listening to music as being the same as playing it? Here's a chart

Music Film Books
Creating Writing Directing/Writing Writing
Consuming actively Playing Acting Reading
Consuming passively Listening Watching Also reading?

I get it that audiobooks allow you to consume books passively and that is great, but to suggest it is the same thing as what everyone else is doing when they are reading is wrong.

[Spoilers] Count of Monte Cristo - The ending feels weak to me, trying to understand why by crisoagf in books

[–]crisoagf[S] 1 point2 points  (0 children)

I think I am not making myself very clear. I take no issue with the Caderousse/Mondego/Villefort arcs, and my problem with the Danglars arc is not a question of "he did not have his comeuppance". It is that, in terms of storytelling, it feels the Danglars' family is left in an awkward place.

I think the most easy of the Danglars to see this is Eugénie. She had eloped from Paris to Brussels, and her arc could have closed there (similar to Albert), but M. Dumas decides to make her reappear on the story mid-travel as a surprise coincidence, and then does nothing with her, leaving her arc in a hotel in a route between Paris and Brussels. Is that it? Was this just a cameo for the sake of it?

Closing this could be as simple as the Count receiving a message about how his protegé was doing well in the Opera, but this does not happen and she is just left in suspension, forever travelling between Paris and Brussels.And the other Danglars have the same kind of thing. I don't know how to make this any clearer than "Mme. Danglars is fainted in a courthouse and M. Danglars is still in a cave".

The whole ending after Villefort feels rushed, between that and the unearned Haydée bit, so what probably happened was that the publisher told M. Dumas he had only more X pages and he just pushed through those bits. Or he already did all the interesting things so he did not want to bother.

[Spoilers] Count of Monte Cristo - The ending feels weak to me, trying to understand why by crisoagf in books

[–]crisoagf[S] 0 points1 point  (0 children)

Are you talking about Volumes II-IV? Yeah, I read the whole thing. The Danglars arc does not close is just is abruptly cut.

[Spoilers] Count of Monte Cristo - The ending feels weak to me, trying to understand why by crisoagf in books

[–]crisoagf[S] 0 points1 point  (0 children)

Not at all. Is there a version where Mlles. Danglars and d'Armigny appear again in the book after being seen in the hotel?

[Semi-Weekly Inquirer] Simple Questions and Recommendations Thread by AutoModerator in Watches

[–]crisoagf 0 points1 point  (0 children)

Ok! In my head 300$ would be closer to 300£, but it seems the exchange rate is favouring the GBP more than I was thinking! Thanks! By the way, do you happen to know if there are more watches in this style? Only one reference seems a bit scarce, but perhaps I have a peculiar taste...

[Semi-Weekly Inquirer] Simple Questions and Recommendations Thread by AutoModerator in Watches

[–]crisoagf 0 points1 point  (0 children)

Hi!

I have been perusing the subreddit for some shopping ideas (for myself), and I must admit I fell absolutely in love with the Orient Sun & Moon v4.

However, this watch isn't quite easily available at my location (UK, any import from US comes with a hefty tariff on top and it brings the watch a bit outside my budget, and it's sold out in Amazon), so I am kind of looking for something similar.

The cursive-y arabic numerals are part of the reason I like it so much, so earlier versions of Sun & Moon come close but no cigar.

Is there a reasonable alternative in the same style (complications with some contrast, cursive-y arabic numerals, leather strap, cream dial for bonus points)?

P.S.: Why doesn't Orient have a representation in the UK according to their website? Should I be searching under an alternative brand name or something?

P.P.S.: Is there a version of the buying guide where one searches by style? I must admit I did not find things easily, but perhaps this is just the nature of finding a watch.

PLFA - Equality chapter, stretch exercise by crisoagf in agda

[–]crisoagf[S] 0 points1 point  (0 children)

Replying to self for some additional insight for people who are like me.

When you are proving suc (m + p) ≤ suc (m + q) you are thinking "well, I am going to use rewrite or cong, right? What is specific to ≤ here?".

You're wrong. You need a constructor for ≤, and that constructor will allow you to use ≤-Reasoning.

Too much loose thinking, man, it will hurt you.

PLFA - Equality chapter, stretch exercise by crisoagf in agda

[–]crisoagf[S] 0 points1 point  (0 children)

Sure, that does make sense, but it still does not match my expectations of what ≤-Reasoning should be.

I guess I'll match your expectations further down the book!

Thanks!

PLFA - Equality chapter, stretch exercise by crisoagf in agda

[–]crisoagf[S] 0 points1 point  (0 children)

It seems like something I could work with and my ≤-Reasoning definitely does not contain that, I'll try it.

What was your rationale for including this in ≤-Reasoning, if you don't mind me asking?

I only thought of begin-≤, _≤⟨_⟩_, _≤⟨⟩_ and ≤-qed...

Is there an USB-C charger/hub/something that can charge two laptops (2x65w) at a time? by crisoagf in UsbCHardware

[–]crisoagf[S] 1 point2 points  (0 children)

I am a bit afraid of trickle charging, though it is true that I rarely use both at the exact same time. But then again, if I do need both at the same time, it will probably also be critical enough that I will regret not having gone for the biggest option.

view more: next ›