Logs: freenode/#haskell
| 2021-03-21 17:14:47 | <edmundnoble> | `unsafeCoerce . unsafeCoerce == unsafeCoerce` |
| 2021-03-21 17:15:00 | × | mastarija quits (~mastarija@31.217.19.201) (Client Quit) |
| 2021-03-21 17:15:02 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:7956:c631:2eb4:a488) (Ping timeout: 264 seconds) |
| 2021-03-21 17:15:02 | × | stree quits (~stree@68.36.8.116) (Quit: Caught exception) |
| 2021-03-21 17:15:04 | <chisui> | Well I just built a bad `Proxy` I guess. |
| 2021-03-21 17:15:26 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-21 17:15:38 | <edmundnoble> | If you use `const unsafeCoerce` that will typecheck for anything, not just `Proxy` and things isomorphic to it |
| 2021-03-21 17:15:53 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-21 17:16:03 | <edmundnoble> | I guess this is one reason why we need the free theorems for `fmap` to determine that there is only one lawful instance of `Functor` per type |
| 2021-03-21 17:16:25 | <chisui> | I was just trying to break the second law |
| 2021-03-21 17:17:12 | → | tsaka__ joins (~torstein@ppp-94-65-45-45.home.otenet.gr) |
| 2021-03-21 17:17:35 | → | dsrt^ joins (dsrt@ip98-184-89-2.mc.at.cox.net) |
| 2021-03-21 17:18:30 | <edmundnoble> | As a counterexample to the "second functor law is always true in cases where the first law is true"? If so, parametricity is part of the proof if I understand correctly, so `unsafeCoerce` would be cheating if it worked |
| 2021-03-21 17:18:32 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:c1f2:e355:53f0:4ab8) (Ping timeout: 240 seconds) |
| 2021-03-21 17:18:43 | × | kuribas quits (~user@ptr-25vy0i7q7d8r48rlgds.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2021-03-21 17:20:40 | <edmundnoble> | Hm maybe you can cheat another way, iirc you can sort of recover types at runtime by looking at the runtime's data structures |
| 2021-03-21 17:21:04 | <chisui> | without `Typeable`? |
| 2021-03-21 17:21:24 | <edmundnoble> | Yes, it was packaged up in https://hackage.haskell.org/package/recover-rtti |
| 2021-03-21 17:21:44 | <edmundnoble> | Oh you might also be able, and this is very cheeky, you could use `reallyUnsafePtrEquality` to "detect" `id` |
| 2021-03-21 17:22:01 | <edmundnoble> | Check if `f x` is pointer-equal to `x`, and do something special in that case |
| 2021-03-21 17:22:57 | <edmundnoble> | That will detect functions which are operationally the same as `id`, but there are going to be other functions which are extensionally the same as `id` that it won't work with, like `\(C x) -> C x` |
| 2021-03-21 17:23:52 | <chisui> | Ok, but all these break parametricity. But there is really no way to break the composition law while satisfying the identity law without breaking parametricity. |
| 2021-03-21 17:24:06 | <ski> | (unless `C' is a `newtype' data constructor) |
| 2021-03-21 17:24:23 | <edmundnoble> | Right, there is no way |
| 2021-03-21 17:24:26 | <dolio> | All these 'really unsafe' things are irrelevant, because they are not sound with respect to the semantics used to talk about parametricity. |
| 2021-03-21 17:24:28 | <edmundnoble> | And yes true ski |
| 2021-03-21 17:24:56 | × | elliott_ quits (~elliott_@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 240 seconds) |
| 2021-03-21 17:25:16 | <edmundnoble> | dolio: because they also break the type system in some way? |
| 2021-03-21 17:26:48 | × | jamm__ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 2021-03-21 17:28:23 | → | DavidEichmann joins (~david@47.27.93.209.dyn.plus.net) |
| 2021-03-21 17:28:27 | <edmundnoble> | I guess you need to have a notion of "equality" to have a semantics at all, and that notion of equality won't brook `x == y -/> f x == f y` |
| 2021-03-21 17:29:57 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 2021-03-21 17:30:12 | → | rybern joins (18c25abd@cpe-24-194-90-189.nycap.res.rr.com) |
| 2021-03-21 17:30:30 | → | ADG1089__ joins (~aditya@27.58.165.185) |
| 2021-03-21 17:30:32 | × | plutoniix quits (~q@node-uhl.pool-125-24.dynamic.totinternet.net) (Ping timeout: 240 seconds) |
| 2021-03-21 17:30:34 | → | frozenErebus joins (~frozenEre@94.129.70.18) |
| 2021-03-21 17:30:37 | <edmundnoble> | The "equations" part of "equational reasoning" breaks |
| 2021-03-21 17:30:57 | ADG1089__ | is now known as ADG1089 |
| 2021-03-21 17:31:08 | <ADG1089> | can someone explain https://github.com/haskell/cabal/issues/6221 in simple terms? |
| 2021-03-21 17:31:15 | <ski> | extensionality |
| 2021-03-21 17:31:27 | × | tsaka__ quits (~torstein@ppp-94-65-45-45.home.otenet.gr) (Remote host closed the connection) |
| 2021-03-21 17:32:32 | <edmundnoble> | ski: no, congruence of equality |
| 2021-03-21 17:32:51 | <dolio> | The point of parametricity is that it models of how 99.999% of written code works, and is useful for reasoning about that portion of code. That doesn't mean that you can't just add non-parametric functions and have something different, or that certain low level escape hatches won't act that way. So going and looking for the latter is misunderstanding the point of the model. |
| 2021-03-21 17:32:57 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 264 seconds) |
| 2021-03-21 17:33:40 | <ski> | yes. but sometimes it's expressed as an operation being extensional. e.g. Bishop defines a function as an operation that respects the equivalence relation that his (basically) setoids come equipped with |
| 2021-03-21 17:33:41 | × | orion quits (~orion@unaffiliated/orion) (Remote host closed the connection) |
| 2021-03-21 17:33:45 | <edmundnoble> | ADG1089: Don't add `-O` options to ghc-options in your .cabal file, tell `cabal` that you want an optimization level by adding it as a flag |
| 2021-03-21 17:33:59 | <edmundnoble> | Either to your cabal.project file or to your cabal invocation |
| 2021-03-21 17:34:09 | × | srk quits (~sorki@gateway/tor-sasl/sorki) (Remote host closed the connection) |
| 2021-03-21 17:34:09 | × | hexo quits (~hexo@gateway/tor-sasl/hexo) (Remote host closed the connection) |
| 2021-03-21 17:34:11 | <ski> | er, to clarify, defines that property as the operation being extensional, and then being a function |
| 2021-03-21 17:34:13 | → | Lycurgus joins (~niemand@98.4.116.165) |
| 2021-03-21 17:34:22 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 2021-03-21 17:34:23 | → | srk joins (~sorki@gateway/tor-sasl/sorki) |
| 2021-03-21 17:34:28 | → | hexo joins (~hexo@gateway/tor-sasl/hexo) |
| 2021-03-21 17:34:48 | <ADG1089> | edmundnoble: cabal.project, right? I think then I can push it to git too |
| 2021-03-21 17:35:39 | <edmundnoble> | Yes, `optimization: 2` in there or whichever you want |
| 2021-03-21 17:35:51 | <edmundnoble> | Or you can put it in `cabal.project.local`which is traditionally in `.gitignore` |
| 2021-03-21 17:36:18 | <ADG1089> | I actually want the maximum performance so I'll need to check in the file |
| 2021-03-21 17:36:35 | <geekosaur> | -O2 doesn't necessarily mean max performance |
| 2021-03-21 17:36:35 | <geekosaur> | \ |
| 2021-03-21 17:36:56 | <geekosaur> | it means expensive optimization passes that may end up doing nothing or even pessimizing |
| 2021-03-21 17:37:13 | <ADG1089> | I'll try some benchmarks using that |
| 2021-03-21 17:37:27 | → | Sgeo joins (~Sgeo@ool-18b98aa4.dyn.optonline.net) |
| 2021-03-21 17:37:35 | <ADG1089> | also can i speread a function definition over multiple files like f 1 in file 1 and f 2 in file 2 and f 3 in file 3 and so on |
| 2021-03-21 17:37:39 | <ADG1089> | *spread |
| 2021-03-21 17:37:46 | <geekosaur> | nope |
| 2021-03-21 17:37:47 | <edmundnoble> | No |
| 2021-03-21 17:38:15 | × | Hi-Angel quits (~constanti@broadband-188-32-15-112.ip.moscow.rt.ru) (Read error: Connection reset by peer) |
| 2021-03-21 17:38:19 | <rybern> | So I have this basic question that keeps coming up in applications. Suppose I want to have components that declare effects like (MonadReader Int m, MonadReader String m) =>, so that I can also execute the effects one at a time with e.g. runReaderT 0. How do people usually solve this? I don't think I should have to use a Free-based effect library, |
| 2021-03-21 17:38:20 | <rybern> | and capability seems like a very heavy solution with all of the newtypes. The best solution I've found is Ether, but it's not maintained anymore, so people must be using something else |
| 2021-03-21 17:38:40 | <ski> | no mixin module like things |
| 2021-03-21 17:39:24 | → | __minoru__shirae joins (~shiraeesh@77.94.25.47) |
| 2021-03-21 17:41:08 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-03-21 17:42:36 | × | tenniscp25 quits (~tenniscp2@134.196.209.118) (Remote host closed the connection) |
| 2021-03-21 17:43:07 | <chisui> | rybern you could use Effect systems like https://hackage.haskell.org/package/freer-effects |
| 2021-03-21 17:43:16 | → | tenniscp25 joins (~tenniscp2@134.196.209.118) |
| 2021-03-21 17:44:53 | × | rajivr quits (uid269651@gateway/web/irccloud.com/x-tunnvuktqcelikkp) (Quit: Connection closed for inactivity) |
| 2021-03-21 17:44:55 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:c1f2:e355:53f0:4ab8) |
| 2021-03-21 17:45:26 | <rybern> | thanks chisui, I looked into that one and it's probably what I'll do. I think what I'm asking is why we can't have that simple pattern with mtl, Ether seemed to solve the problem but no one used it |
| 2021-03-21 17:45:53 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 245 seconds) |
| 2021-03-21 17:45:56 | → | DTZUZU_ joins (~DTZUZO@205.ip-149-56-132.net) |
| 2021-03-21 17:46:03 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Read error: Connection reset by peer) |
| 2021-03-21 17:46:07 | DTZUZU_ | is now known as DTZUZU |
| 2021-03-21 17:46:14 | × | xff0x_ quits (~xff0x@2001:1a81:52b5:3300:bd27:5212:7f1:6207) (Ping timeout: 264 seconds) |
| 2021-03-21 17:46:32 | × | malumore quits (~malumore@151.62.127.88) (Ping timeout: 240 seconds) |
| 2021-03-21 17:46:41 | → | xff0x_ joins (~xff0x@2001:1a81:52b5:3300:c707:488e:58f1:2927) |
| 2021-03-21 17:47:15 | → | Garbanzo joins (~Garbanzo@70.234.205.193) |
| 2021-03-21 17:47:44 | × | tenniscp25 quits (~tenniscp2@134.196.209.118) (Ping timeout: 240 seconds) |
| 2021-03-21 17:48:27 | <dolio> | Having multiple, scoped instances like that would require not using fundeps, which would make inference bad. |
| 2021-03-21 17:48:35 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 2021-03-21 17:48:47 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2021-03-21 17:49:06 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-21 17:49:46 | <dolio> | And it might get kind of confusing if there are cases where the environment type is not known to be the same, but then end up the same, and such. |
| 2021-03-21 17:49:48 | → | dcoutts joins (~dcoutts@unaffiliated/dcoutts) |
| 2021-03-21 17:50:20 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 2021-03-21 17:50:35 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:c1f2:e355:53f0:4ab8) (Ping timeout: 272 seconds) |
| 2021-03-21 17:51:04 | <carter> | agreed with dolio |
| 2021-03-21 17:52:16 | <edmundnoble> | IMO, "effects" has just not worked out as an abstraction in the way people want it to. There are basically three concerns which people are tempted to combine which are best kept separate: composing `>>=` implementations, abstracting over `>>=` implementations, and composing datatypes. Respectively, transformers, mtl, and lens solve these problems well |
| 2021-03-21 17:52:16 | <carter> | and more broadly, theres an issue with writing transformer / mtl code as MonadFoo m, MonadBar m) =>, namely that youre presuming that the operations in those nested monads commute |
All times are in UTC.