Logs: liberachat/#haskell
| 2021-07-12 21:12:16 | × | tremon_ quits (~tremon@217-63-61-89.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in) |
| 2021-07-12 21:13:21 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:6d00:2ab2:6519:235b) (Remote host closed the connection) |
| 2021-07-12 21:13:57 | × | even4void quits (even4void@came.here.for-some.fun) (Remote host closed the connection) |
| 2021-07-12 21:13:58 | × | xacktm quits (xacktm@user/xacktm) (Remote host closed the connection) |
| 2021-07-12 21:13:58 | × | andreas3- quits (andreas303@ip227.orange.bnc4free.com) (Remote host closed the connection) |
| 2021-07-12 21:15:50 | × | phaazon quits (~phaazon@2001:41d0:a:fe76::1) (Ping timeout: 272 seconds) |
| 2021-07-12 21:17:15 | × | ub quits (~Thunderbi@p2e5a50e5.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 2021-07-12 21:19:57 | × | ubert quits (~Thunderbi@p2e5a50e5.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 2021-07-12 21:20:04 | → | chisui joins (~chisui@200116b8667bfd006d48966f94785d9f.dip.versatel-1u1.de) |
| 2021-07-12 21:21:34 | → | warnz joins (~warnz@2600:1700:77c0:5610:acd9:fdbc:f96e:2452) |
| 2021-07-12 21:22:11 | × | fendor quits (~fendor@77.119.208.64.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 2021-07-12 21:22:29 | <Atum_> | If `==` is a function, why can't I call it as `== 1 2`? |
| 2021-07-12 21:22:42 | <Guest25> | (==) 1 2 |
| 2021-07-12 21:22:53 | <geekosaur> | because that's not the syntax for infix // symbol functions |
| 2021-07-12 21:23:03 | <Atum_> | hm, symbol functions |
| 2021-07-12 21:23:08 | <Atum_> | Ok, I'll search about it, thanks! |
| 2021-07-12 21:23:24 | <geekosaur> | symbols are infix unless parenthesized; alphanumerics are prefix unless backticked |
| 2021-07-12 21:23:44 | <geekosaur> | so (==) a b but a `mod` b |
| 2021-07-12 21:24:46 | <Atum_> | I see, ty! |
| 2021-07-12 21:25:00 | → | chexum joins (~chexum@gateway/tor-sasl/chexum) |
| 2021-07-12 21:25:53 | <chisui> | why does `(\case {}) :: forall v a. Proxy (v :: Void) -> a` result in a non-exhaustive Patter warning when using `-Wall`? |
| 2021-07-12 21:26:04 | × | warnz quits (~warnz@2600:1700:77c0:5610:acd9:fdbc:f96e:2452) (Ping timeout: 256 seconds) |
| 2021-07-12 21:26:32 | <chisui> | * needs Extensions: LambdaCase, ScopedTypeVariables, DataKinds, EmptyCase |
| 2021-07-12 21:27:54 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 2021-07-12 21:28:53 | → | Ariakenom joins (~Ariakenom@c83-255-154-140.bredband.tele2.se) |
| 2021-07-12 21:29:15 | <chisui> | My expectation would be that can't create an value for `Proxy (v :: Void)` since Void doesn't have any constructors, thus you could safely create an absurd function. |
| 2021-07-12 21:30:07 | <Hecate> | > :t absurd |
| 2021-07-12 21:30:10 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
| 2021-07-12 21:30:12 | <Hecate> | booo |
| 2021-07-12 21:30:16 | <monochrom> | Proxy (v :: Void) is not Void. |
| 2021-07-12 21:30:16 | <Hecate> | % :t absurd |
| 2021-07-12 21:30:16 | <yahb> | Hecate: forall {a}. Void -> a |
| 2021-07-12 21:30:43 | <boxscape> | % (\case {}) (Proxy :: Proxy Void) |
| 2021-07-12 21:30:43 | <yahb> | boxscape: *** Exception: <interactive>:149:2-9: Non-exhaustive patterns in case |
| 2021-07-12 21:31:13 | <chisui> | monochrom: but you can't create a value of that Type. |
| 2021-07-12 21:31:21 | <boxscape> | chisui: see my example |
| 2021-07-12 21:31:25 | <monochrom> | boxscape just did. |
| 2021-07-12 21:31:36 | <janus> | % (\case Proxy -> "Yo") (Proxy :: Proxy Void) |
| 2021-07-12 21:31:36 | <yahb> | janus: "Yo" |
| 2021-07-12 21:31:39 | <boxscape> | wait |
| 2021-07-12 21:31:46 | <boxscape> | it's Proxy (v :: Void) |
| 2021-07-12 21:32:20 | <chisui> | I want a Proxy where the argument is of the DataKind of Void. |
| 2021-07-12 21:33:13 | <boxscape> | % foo = ((\case {}) :: forall v a. Proxy (v :: Void) -> a) |
| 2021-07-12 21:33:13 | <yahb> | boxscape: |
| 2021-07-12 21:33:16 | → | andreas303 joins (andreas303@ip227.orange.bnc4free.com) |
| 2021-07-12 21:33:46 | <boxscape> | % foo Proxy |
| 2021-07-12 21:33:46 | <yahb> | boxscape: *** Exception: <interactive>:153:9-16: Non-exhaustive patterns in case |
| 2021-07-12 21:34:13 | → | even4void joins (even4void@came.here.for-some.fun) |
| 2021-07-12 21:34:13 | <boxscape> | chisui: that means it really is non-exhaustive |
| 2021-07-12 21:34:48 | <chisui> | huh, do you not have to provide a proof for v? |
| 2021-07-12 21:34:57 | <monochrom> | Proxy is a phantom type that has one data constructor and completely ignores the type parameter so even when the type parameter is nonsense you still have one data constructor to worry about. |
| 2021-07-12 21:35:02 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 2021-07-12 21:35:03 | → | xacktm joins (xacktm@user/xacktm) |
| 2021-07-12 21:35:34 | <chisui> | % foo (Proxy :: Proxy Any) |
| 2021-07-12 21:35:34 | <yahb> | chisui: ; <interactive>:155:21: error:; Ambiguous occurrence `Any'; It could refer to; either `GHC.Exts.Any', imported from `GHC.Exts' (and originally defined in `GHC.Types'); or `Control.Monad.RWS.Any', imported from `Control.Monad.RWS' (and originally defined in `base-4.15.0.0:Data.Semigroup.Internal') |
| 2021-07-12 21:35:49 | → | oldleather joins (~oldleathe@172.58.168.19) |
| 2021-07-12 21:36:12 | <boxscape> | chisui: I'm not actually sure how GHC supplies v here but when in doubt it usually is Any |
| 2021-07-12 21:36:19 | <monochrom> | This is very similar to an error I made when I was learning set theory. |
| 2021-07-12 21:36:36 | <monochrom> | {} is the empty set, but {{}} is non-empty. |
| 2021-07-12 21:37:34 | <monochrom> | My teacher had trouble convincing me of that for like half and hour. |
| 2021-07-12 21:37:42 | <chisui> | Proxy is a functor. So shouldn't `Proxy (v :: Void)` be that functor be applied to the empty category? |
| 2021-07-12 21:37:47 | ← | oldleather parts (~oldleathe@172.58.168.19) (Leaving) |
| 2021-07-12 21:38:09 | <boxscape> | chisui: I think if you were to do this in Agda for example your example really but would exhaustive but I'm not sure |
| 2021-07-12 21:38:16 | <boxscape> | Any breaks the assumption |
| 2021-07-12 21:38:22 | <boxscape> | but Any isn't allowed in Agda |
| 2021-07-12 21:38:45 | <boxscape> | (...the assumption being that you must be able to supply a v) |
| 2021-07-12 21:39:12 | <monochrom> | As far as the Functor class is concerned, it is only concerned about Proxy (v :: *), no? |
| 2021-07-12 21:39:37 | <monochrom> | Because you need "(a -> b) -> Proxy a -> Proxy b" to make sense. |
| 2021-07-12 21:41:18 | <chisui> | monochrom: If understand you correctly then `Proxy Void` would be the set containing the empty set. `Proxy (v :: Void)` would be the image of a function where the empty set is its domain. |
| 2021-07-12 21:42:03 | <boxscape> | chisui: btw looking at the core output confirms that GHC chooses Any as instantiation for v |
| 2021-07-12 21:42:04 | <chisui> | monochrom: I didn't mean Functor in the haskell sense but the category theoretical sense. |
| 2021-07-12 21:42:27 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 255 seconds) |
| 2021-07-12 21:42:36 | <chisui> | boxscape: thank you. Too bad |
| 2021-07-12 21:43:09 | <boxscape> | chisui: if it bothers you I suppose you could open a ticket on the issue tracker to spark a discussion... |
| 2021-07-12 21:43:41 | <boxscape> | though it might not be feasible to disallow it, idk |
| 2021-07-12 21:44:17 | <boxscape> | (s/disallow it/make GHC not choose Any here) |
| 2021-07-12 21:45:19 | <chisui> | boxscape: how did you discover that any was chosen? |
| 2021-07-12 21:47:12 | <boxscape> | chisui: in ghci I put `:set -ddump-simpl`, and then ran `foo Proxy`, which resulted in this output https://paste.tomsmeding.com/hAkGgIvT note how the first type argument supplied to `foo` with the @ is GHC.Types.Any |
| 2021-07-12 21:48:10 | <monochrom> | The IOs are a bit distracting :) |
| 2021-07-12 21:48:24 | <chisui> | Thank you |
| 2021-07-12 21:48:52 | <boxscape> | monochrom: that is true, could be more enlightening to actually compile a file that contains the expression with -ddump-simpl |
| 2021-07-12 21:49:09 | <monochrom> | "Data.Proxy.Proxy @ Data.Void.Void @ GHC.Types.Any" helps, though. |
| 2021-07-12 21:51:54 | <monochrom> | "type family Any :: k" inhabits every kind. That's very kind of it. |
| 2021-07-12 21:52:47 | <chisui> | Well its definition is just `type family Any where {}` so ... |
| 2021-07-12 21:53:39 | × | argento quits (~argent0@168-227-97-29.ptr.westnet.com.ar) (Ping timeout: 276 seconds) |
| 2021-07-12 21:53:40 | × | ukari quits (~ukari@user/ukari) (Remote host closed the connection) |
| 2021-07-12 21:53:57 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-07-12 21:54:27 | → | ukari joins (~ukari@user/ukari) |
| 2021-07-12 21:54:43 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) (Remote host closed the connection) |
| 2021-07-12 21:54:55 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) |
| 2021-07-12 21:55:14 | <boxscape> | chisui: btw here's a version where the core output for that expression is a bit nicer to read (though I omitted the other bindings from the core output) https://paste.tomsmeding.com/TmtRWXRN |
| 2021-07-12 21:56:07 | → | V joins (~v@anomalous.eu) |
| 2021-07-12 21:57:24 | <boxscape> | (without the NOINLINE foo simply becomes an exception about non-exhaustive patterns) |
| 2021-07-12 21:57:30 | <boxscape> | s/foo/test |
| 2021-07-12 21:58:22 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 256 seconds) |
| 2021-07-12 21:59:16 | <chisui> | Isn't using `Any` the same as arguing from False? |
| 2021-07-12 21:59:33 | × | thecoder quits (~mrrobot@c-73-27-71-147.hsd1.fl.comcast.net) (Ping timeout: 255 seconds) |
| 2021-07-12 21:59:39 | × | Ariakenom quits (~Ariakenom@c83-255-154-140.bredband.tele2.se) (Read error: Connection reset by peer) |
| 2021-07-12 21:59:41 | <boxscape> | yes |
| 2021-07-12 22:00:07 | <chisui> | Seems bad |
All times are in UTC.