Logs: freenode/#haskell
| 2021-03-24 17:11:19 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 2021-03-24 17:16:21 | × | bitmagie quits (~Thunderbi@200116b8066df900d5323f70f4278fa3.dip.versatel-1u1.de) (Quit: bitmagie) |
| 2021-03-24 17:16:38 | → | bitmagie joins (~Thunderbi@200116b8066df900d5323f70f4278fa3.dip.versatel-1u1.de) |
| 2021-03-24 17:17:12 | × | bitmagie quits (~Thunderbi@200116b8066df900d5323f70f4278fa3.dip.versatel-1u1.de) (Client Quit) |
| 2021-03-24 17:17:44 | <hololeap> | class Divisible f => Decidable f where ; lose :: (a -> Void) -> f a ; choose :: (a -> Either b c) -> f b -> f c -> f a |
| 2021-03-24 17:18:01 | <hololeap> | the intuition for choose is pretty obvious, but i don't understand the intuition for lose |
| 2021-03-24 17:20:23 | <hololeap> | "give me a function that takes 'a' and returns Void, and i'll give you 'a -> ByteString'" (for instance) |
| 2021-03-24 17:20:59 | → | hexfive joins (~hexfive@50.35.83.177) |
| 2021-03-24 17:21:00 | × | emmanuel_erc quits (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) (Read error: Connection reset by peer) |
| 2021-03-24 17:21:23 | → | emmanuel_erc joins (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) |
| 2021-03-24 17:21:30 | <ski> | iirc, when you find yourself in an impossible case, in your divide-and-conquer |
| 2021-03-24 17:21:30 | <Franciman> | (a -> Void) means like, give me something false |
| 2021-03-24 17:21:35 | <Franciman> | and I will assert that it is false |
| 2021-03-24 17:21:36 | <Franciman> | ? |
| 2021-03-24 17:21:36 | <Franciman> | lol |
| 2021-03-24 17:22:26 | <monochrom> | Looks to me f is a contravariant functor. |
| 2021-03-24 17:22:40 | <ski> | yes |
| 2021-03-24 17:23:20 | <monochrom> | (a->Void) -> (a->ByteString) isn't that far-fetched |
| 2021-03-24 17:23:32 | <Franciman> | it would be |
| 2021-03-24 17:23:35 | <Franciman> | f :: a -> Void |
| 2021-03-24 17:23:38 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-24 17:23:39 | <Franciman> | efq :: Void -> b |
| 2021-03-24 17:23:45 | <Franciman> | efq . f :: a -> b |
| 2021-03-24 17:23:46 | <ski> | <https://hackage.haskell.org/package/contravariant-1.5.3/docs/Data-Functor-Contravariant-Divisible.html> |
| 2021-03-24 17:23:54 | <hololeap> | efq? |
| 2021-03-24 17:24:01 | <hololeap> | i thought that function was called absurd |
| 2021-03-24 17:25:21 | <hololeap> | anyway, i suppose it makes sense in a bizarre way. there's no way to construct 'f', thus nothing that can be passed into 'lose' |
| 2021-03-24 17:25:22 | × | juri_ quits (~juri@212.86.35.86) (Read error: Connection reset by peer) |
| 2021-03-24 17:25:30 | × | Franciman quits (~francesco@host-79-53-62-46.retail.telecomitalia.it) (Quit: Leaving) |
| 2021-03-24 17:25:32 | × | Merfont quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 2021-03-24 17:25:36 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-109-157.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-03-24 17:25:38 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 2021-03-24 17:25:43 | → | Merfont joins (~Kaiepi@47.54.252.148) |
| 2021-03-24 17:25:53 | → | neiluj joins (~jco@91-167-203-101.subs.proxad.net) |
| 2021-03-24 17:25:54 | <hololeap> | or i suppose 'f' could be 'const undefined' |
| 2021-03-24 17:25:57 | <monochrom> | "you have nothing to lose" |
| 2021-03-24 17:25:58 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-109-157.w86-212.abo.wanadoo.fr) |
| 2021-03-24 17:25:59 | × | neiluj quits (~jco@91-167-203-101.subs.proxad.net) (Changing host) |
| 2021-03-24 17:25:59 | → | neiluj joins (~jco@unaffiliated/neiluj) |
| 2021-03-24 17:26:05 | × | graf_blutwurst quits (~user@2001:171b:226e:adc0:102c:ecb5:8d03:4f2b) (Remote host closed the connection) |
| 2021-03-24 17:26:19 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-24 17:26:21 | <monochrom> | Ah but a=Void is possible |
| 2021-03-24 17:26:46 | <monochrom> | lose (id :: Void -> Void) is possible. |
| 2021-03-24 17:27:59 | <ski> | you might have a case-splitting where you'll later discover that one of the cases is impossible. i'm guessing that would be one main use of `lose' |
| 2021-03-24 17:28:01 | <monochrom> | I think you keep forgetting that f is a contravariant functor. "sx :: f a" does not mean that sx produces an 'a' value or else bottoms out. |
| 2021-03-24 17:28:23 | → | Kaeipi joins (~Kaiepi@47.54.252.148) |
| 2021-03-24 17:28:28 | × | Merfont quits (~Kaiepi@47.54.252.148) (Read error: Connection reset by peer) |
| 2021-03-24 17:29:58 | → | bahamas joins (~lucian@188.27.48.99) |
| 2021-03-24 17:29:58 | × | bahamas quits (~lucian@188.27.48.99) (Changing host) |
| 2021-03-24 17:29:58 | → | bahamas joins (~lucian@unaffiliated/bahamas) |
| 2021-03-24 17:30:10 | × | dbmikus quits (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) (Ping timeout: 265 seconds) |
| 2021-03-24 17:30:19 | <hololeap> | regardless of it being a contravariant functor, it seems to me the only possibilities for 'f' would be 'const undefined' or 'id' |
| 2021-03-24 17:30:22 | × | Boomerang quits (~Boomerang@2a05:f6c7:2179:0:f97c:9426:ef00:f528) (Quit: Leaving) |
| 2021-03-24 17:30:50 | <monochrom> | Is "const" a term? a type? |
| 2021-03-24 17:31:18 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds) |
| 2021-03-24 17:31:39 | <peanut_> | :t const |
| 2021-03-24 17:31:41 | <lambdabot> | a -> b -> a |
| 2021-03-24 17:31:46 | <shapr> | :t Const |
| 2021-03-24 17:31:48 | <lambdabot> | forall k a (b :: k). a -> Const a b |
| 2021-03-24 17:31:50 | × | Garbanzo quits (~Garbanzo@2602:304:6eac:dc10::2e) (Ping timeout: 264 seconds) |
| 2021-03-24 17:32:09 | <hololeap> | i'm talking about 'const :: a -> b -> a' from Prelude |
| 2021-03-24 17:32:16 | <monochrom> | So, term. |
| 2021-03-24 17:32:21 | <hololeap> | :t const undefined |
| 2021-03-24 17:32:22 | <lambdabot> | b -> a |
| 2021-03-24 17:32:22 | <monochrom> | Is f a term? a type? |
| 2021-03-24 17:32:51 | <hololeap> | 'f' is a term, the function that you pass into 'lose' from Data.Functor.Contravariant.Divisible |
| 2021-03-24 17:33:28 | <monochrom> | If f is a term, what does "(a -> Either b c) -> f b -> f c -> f a" mean? |
| 2021-03-24 17:33:35 | × | s00pcan quits (~chris@107.181.165.217) (Ping timeout: 240 seconds) |
| 2021-03-24 17:33:51 | <hololeap> | i'm not talking about that 'f'. different 'f' |
| 2021-03-24 17:33:52 | <ski> | hololeap : `void :: forall a. Void -> a; void v = case v of {}' would fit the bill, no ? (no `undefined' in sight !) |
| 2021-03-24 17:34:25 | → | augnun joins (~augnun@2804:14c:658b:41bb:9d27:655f:eef9:d872) |
| 2021-03-24 17:34:25 | × | emmanuel_erc quits (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) (Read error: Connection reset by peer) |
| 2021-03-24 17:34:58 | → | emmanuel_erc joins (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) |
| 2021-03-24 17:34:59 | <ski> | @kind Const |
| 2021-03-24 17:35:00 | <lambdabot> | * -> k -> * |
| 2021-03-24 17:35:25 | <hololeap> | lose :: (a -> Void) -> f a ; lose f = ... |
| 2021-03-24 17:36:08 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 2021-03-24 17:36:29 | <monochrom> | Do you mind not using the same name "f" for two different things? |
| 2021-03-24 17:37:16 | <hololeap> | ok. this is just how the documentation names things, and also how Franciman named it when i first asked |
| 2021-03-24 17:37:34 | <monochrom> | Fine. |
| 2021-03-24 17:38:24 | <ski> | so `lose' will only be called with an `f' like `id' or `void', assuming no bottoms. so in that case `a' must be something like `Void'. possibly `Int :~: Bool' or some other vacuous of of a GADT |
| 2021-03-24 17:38:44 | <monochrom> | "lose" is a class method. You're now talking implementing it. So you are talking writing "instance Decidable AnActualType where ...". What do you propose for AnActualType? Or would you want me to propose one? |
| 2021-03-24 17:38:58 | <ski> | so, when `lose' is called, you know that there are no (total) elements of `a', which you can then use to successfully build an `f a' for your `f' |
| 2021-03-24 17:39:41 | × | kuribas quits (~user@ptr-25vy0i8r3m7ulrlbw64.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2021-03-24 17:39:49 | → | viluon joins (uid453725@gateway/web/irccloud.com/x-tsrnritnmsiiiwsr) |
| 2021-03-24 17:40:11 | <ski> | (perhaps `f a' does contain some other useful information, apart from a component that takes in an `a', that will be trivial in this case, calling `f' (and then `void'/`absurd', possibly) |
| 2021-03-24 17:40:15 | <ski> | ) |
| 2021-03-24 17:40:21 | × | rajivr quits (uid269651@gateway/web/irccloud.com/x-yuttflczfhjstiup) (Quit: Connection closed for inactivity) |
| 2021-03-24 17:40:37 | <hololeap> | monochrom: in the documentation, it uses 'newtype Serializer a = Serializer { runSerializer :: a -> ByteString }'. this is the instance of Decidable i was using conceptually |
| 2021-03-24 17:41:48 | <monochrom> | So lose :: (a->Void) -> Serializer a. Morally, (a->Void)->(a->Bytestring). I think you know the answer now. |
| 2021-03-24 17:41:50 | × | son0p quits (~son0p@181.136.122.143) (Quit: Lost terminal) |
| 2021-03-24 17:42:02 | × | borne quits (~fritjof@200116b8644f8c00bc09546e2ac68572.dip.versatel-1u1.de) (Ping timeout: 264 seconds) |
| 2021-03-24 17:43:43 | <hololeap> | i wasn't looking for an "answer", i was looking for help developing an intuition as to when 'lose' would be used and why it's included in the class. |
| 2021-03-24 17:44:09 | hololeap | will ponder what ski said |
| 2021-03-24 17:44:19 | <c_wraith> | you'd use it to erase a case that can't happen |
| 2021-03-24 17:44:48 | <c_wraith> | that's what acting as an identity to choose implies |
| 2021-03-24 17:45:11 | <ski> | @type either absurd |
| 2021-03-24 17:45:13 | <lambdabot> | (b -> c) -> Either Void b -> c |
| 2021-03-24 17:45:18 | <ski> | @type either absurd id |
| 2021-03-24 17:45:20 | <lambdabot> | Either Void c -> c |
All times are in UTC.