Logs: liberachat/#haskell
| 2021-07-21 12:59:31 | → | __monty__ joins (~toonn@user/toonn) |
| 2021-07-21 13:00:12 | <ddb> | if you clarify your claim then it might be easier to see what about it is unsound |
| 2021-07-21 13:01:02 | × | Core2996 quits (~agua@2804:18:4a:c35:1:0:3be5:8cb2) (Ping timeout: 252 seconds) |
| 2021-07-21 13:02:48 | <ddb> | I am not that familiar with haskell, so when you say it's "impossible to write a function" and then you, apparently, write that function I get confused |
| 2021-07-21 13:04:30 | <Orbstheorem> | > you, apparently, write that function |
| 2021-07-21 13:04:30 | <Orbstheorem> | I'm not sure where suggested I wrote that function? |
| 2021-07-21 13:04:31 | <lambdabot> | <hint>:1:4: error: parse error on input ‘,’ |
| 2021-07-21 13:04:57 | <ddb> | in your original statement you have some syntax that appears to describe a function |
| 2021-07-21 13:05:52 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-07-21 13:06:18 | <ddb> | m a -> (a -> t m b) -> t m b |
| 2021-07-21 13:10:32 | <Orbstheorem> | Yes, that's the signature of a function I think it is not possible to write, given `(Monad m, MonadTrans t)` |
| 2021-07-21 13:11:53 | × | juhp quits (~juhp@128.106.188.220) (Quit: juhp) |
| 2021-07-21 13:12:08 | → | juhp joins (~juhp@128.106.188.220) |
| 2021-07-21 13:13:04 | <ddb> | can you give a simpler example of a signature for which no function exists? |
| 2021-07-21 13:13:32 | → | xsperry joins (~as@user/xsperry) |
| 2021-07-21 13:14:09 | <Orbstheorem> | `(Monad m1, Monad m2) => m1 (m2 a) -> m2 (m1 a)` |
| 2021-07-21 13:15:08 | <Orbstheorem> | <dminuoso "This should be doable, consider "> I'm curious though, why did the particle 'Fix' come to mind? |
| 2021-07-21 13:15:15 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Read error: Connection reset by peer) |
| 2021-07-21 13:15:40 | <ddb> | can you briefly describe the obstruction in this simpler case? |
| 2021-07-21 13:18:07 | <haveo> | Orbstheorem: I don't think you can find a law-obeying counter-example, the problem seems to be you can't prove `Monad (t m)' unless you use a very recent version of transformers |
| 2021-07-21 13:18:19 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-21 13:18:30 | <Orbstheorem> | I don't understand the algebraic foundations on monads enough to give a sound argument about why this doesn't work. That said, I think I can give a conbinatorial argument why given the operations available on any instance of Monad `(>>=), fmap, pure, mempty, <*>`, I cannot build such equation. |
| 2021-07-21 13:18:41 | <dminuoso> | haveo: At least lysxia seems to have some reasons why ContT wont yield a valid instance |
| 2021-07-21 13:19:28 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-21 13:19:51 | <haveo> | @type \x f -> lift x >>= f |
| 2021-07-21 13:19:52 | <lambdabot> | (MonadTrans t, Monad m, Monad (t m)) => m a -> (a -> t m b) -> t m b |
| 2021-07-21 13:20:38 | <ddb> | If monads are too abstract, can you rephrase the problem using a particular instance of a monad? Strings under concatenation come to mind, but I do not know if they count as haskell monads. |
| 2021-07-21 13:21:39 | <ddb> | ack, monoid not monad, retract that last comment |
| 2021-07-21 13:21:52 | <haveo> | `Monad (t m)' is guaranteed to exist (that's kind of the whole point) but you can't get it from (MonadTrans t, Monad m) for technical reasons (which are fixed now, but I haven't tested it) |
| 2021-07-21 13:23:18 | <ddb> | I think a simpler example for monads could be Maybe? |
| 2021-07-21 13:23:34 | <ddb> | so if it doesn't work for Maybe it definitely can't work for Monad. |
| 2021-07-21 13:23:58 | → | chomwitt joins (~chomwitt@ppp-94-67-220-135.home.otenet.gr) |
| 2021-07-21 13:26:59 | <haveo> | dminuoso: I wasn't talking about MonadTransFix, just the function he's trying to build |
| 2021-07-21 13:28:09 | → | dunkeln joins (~dunkeln@188.70.26.84) |
| 2021-07-21 13:29:24 | → | zebrag joins (~chris@user/zebrag) |
| 2021-07-21 13:29:34 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 2021-07-21 13:29:34 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 2021-07-21 13:29:37 | allbery_b | is now known as geekosaur |
| 2021-07-21 13:33:58 | → | zaquest joins (~notzaques@5.128.210.178) |
| 2021-07-21 13:34:12 | × | azeem quits (~azeem@176.201.19.41) (Ping timeout: 255 seconds) |
| 2021-07-21 13:34:36 | → | azeem joins (~azeem@176.201.19.41) |
| 2021-07-21 13:43:05 | × | chris_ quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2021-07-21 13:44:20 | → | fef joins (~thedawn@user/thedawn) |
| 2021-07-21 13:48:09 | × | mikail quits (~mikail@90.212.77.3) (Ping timeout: 255 seconds) |
| 2021-07-21 13:48:18 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 240 seconds) |
| 2021-07-21 13:50:48 | → | MorrowM joins (~Morrow@bzq-110-168-31-106.red.bezeqint.net) |
| 2021-07-21 13:51:26 | × | Morrow quits (~Morrow@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 258 seconds) |
| 2021-07-21 13:52:41 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-07-21 13:54:28 | × | azeem quits (~azeem@176.201.19.41) (Ping timeout: 252 seconds) |
| 2021-07-21 13:55:19 | → | shriekingnoise joins (~shrieking@186.137.144.80) |
| 2021-07-21 13:59:27 | → | azeem joins (~azeem@176.200.238.62) |
| 2021-07-21 14:07:03 | × | drd quits (~drd@2001:b07:a70:9f1f:1562:34de:f50f:77d4) (Ping timeout: 250 seconds) |
| 2021-07-21 14:07:58 | × | azeem quits (~azeem@176.200.238.62) (Ping timeout: 246 seconds) |
| 2021-07-21 14:08:43 | → | azeem joins (~azeem@176.200.238.62) |
| 2021-07-21 14:13:04 | → | amahl joins (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 2021-07-21 14:13:17 | × | azeem quits (~azeem@176.200.238.62) (Ping timeout: 258 seconds) |
| 2021-07-21 14:15:31 | → | dunj3 joins (~dunj3@2001:16b8:30c4:6b00:b2db:db95:c4f5:af2c) |
| 2021-07-21 14:15:32 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Quit: FinnElija) |
| 2021-07-21 14:17:09 | → | azeem joins (~azeem@176.200.238.62) |
| 2021-07-21 14:17:32 | × | finsternis quits (~X@23.226.237.192) (Remote host closed the connection) |
| 2021-07-21 14:19:20 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 2021-07-21 14:20:41 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 2021-07-21 14:20:54 | × | Xnuk quits (~xnuk@vultr.xnu.kr) (Quit: ZNC - https://znc.in) |
| 2021-07-21 14:21:09 | × | hendursaga quits (~weechat@user/hendursaga) (Remote host closed the connection) |
| 2021-07-21 14:21:12 | → | Xnuk joins (~xnuk@vultr.xnu.kr) |
| 2021-07-21 14:21:33 | → | hendursaga joins (~weechat@user/hendursaga) |
| 2021-07-21 14:23:48 | → | _xor joins (~xor@74.215.232.67) |
| 2021-07-21 14:25:27 | → | jneira_ joins (~jneira_@28.red-80-28-169.staticip.rima-tde.net) |
| 2021-07-21 14:26:00 | × | jippiedoe quits (~david@229-197-145-85.ftth.glasoperator.nl) (Ping timeout: 252 seconds) |
| 2021-07-21 14:28:12 | → | agua joins (~agua@2804:18:4a:c35:1:0:3be5:8cb2) |
| 2021-07-21 14:29:06 | × | DNH quits (~DNH@2a02:8108:1100:16d8:a03c:ba96:6f1a:16fa) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-07-21 14:29:14 | × | acidjnk quits (~acidjnk@p200300d0c72b9516f180e3afe24121d7.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2021-07-21 14:30:01 | × | slep quits (~slep@cpc150002-brnt4-2-0-cust437.4-2.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2021-07-21 14:30:57 | × | pesada quits (~agua@2804:14c:8793:8e2f:3988:44e0:45e5:bd04) (Ping timeout: 245 seconds) |
| 2021-07-21 14:32:14 | × | juhp quits (~juhp@128.106.188.220) (Quit: juhp) |
| 2021-07-21 14:32:28 | → | juhp joins (~juhp@128.106.188.220) |
| 2021-07-21 14:33:16 | → | Ariakenom joins (~Ariakenom@c83-255-154-140.bredband.tele2.se) |
| 2021-07-21 14:33:32 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 2021-07-21 14:33:55 | → | DNH joins (~DNH@2a02:8108:1100:16d8:808b:9f4a:c222:7def) |
| 2021-07-21 14:34:03 | × | Obo quits (~roberto@70.pool90-171-81.dynamic.orange.es) (Ping timeout: 255 seconds) |
| 2021-07-21 14:34:35 | → | slep joins (~slep@cpc150002-brnt4-2-0-cust437.4-2.cable.virginm.net) |
| 2021-07-21 14:34:54 | × | oxide quits (~lambda@user/oxide) (Quit: oxide) |
| 2021-07-21 14:34:55 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Quit: Leaving) |
| 2021-07-21 14:41:27 | <Taneb> | Is there a common newtype on Maybe that makes Nothing compare as if it's it infinity? |
| 2021-07-21 14:47:12 | <Cajun> | are you saying `Just x < Nothing` for any x? also, im not sure how a newtype on maybe would work since maybe has 2 fields |
| 2021-07-21 14:47:36 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 2021-07-21 14:48:40 | <Taneb> | newtype Foo a = Foo { unFoo :: Maybe a }; instance Ord a => Ord (Foo a) where |
| 2021-07-21 14:48:51 | <Taneb> | And yeah, that's the ordering I'm after |
| 2021-07-21 14:50:09 | <Rembane> | Taneb: Use a custom sum type instead, it makes it much easier to read the code when you look at it again in three months. |
| 2021-07-21 14:50:31 | <Taneb> | Rembane: I'm being given a big old list of Maybes and want to do this in one place |
| 2021-07-21 14:50:40 | curiousgay_ | is now known as curiousgay |
| 2021-07-21 14:51:07 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 2021-07-21 14:51:39 | × | curiousgay quits (~curiousga@77-120-144-167.kha.volia.net) (Quit: Leaving) |
| 2021-07-21 14:51:41 | <Rembane> | Taneb: Okay, lets see what we can do then. :) |
| 2021-07-21 14:51:53 | → | curiousgay joins (~curiousga@77-120-144-167.kha.volia.net) |
| 2021-07-21 14:51:58 | <haveo> | Taneb: you could use Down (Maybe (Down a)) |
| 2021-07-21 14:52:33 | <Taneb> | haveo: that is certainly an option, I'll give you that |
| 2021-07-21 14:54:04 | → | doyougnu joins (~user@c-73-25-202-122.hsd1.or.comcast.net) |
| 2021-07-21 14:54:52 | <Cajun> | using Down is likely much more convenient than defining your own instance of Maybe with reverse order |
| 2021-07-21 14:54:53 | <Rembane> | Taneb: Or use sortBy and write a sorting function that does what you want. |
All times are in UTC.