Logs: liberachat/#haskell
| 2021-05-23 23:20:01 | → | slack1256 joins (~slack1256@181.203.76.139) |
| 2021-05-23 23:20:13 | × | nan` quits (~nan`@rrcs-70-60-83-42.central.biz.rr.com) (Client Quit) |
| 2021-05-23 23:21:10 | <boxscape> | ah, actually, the existential would have to be different |
| 2021-05-23 23:21:24 | <boxscape> | data EUser a = forall b . Hash b => User a b |
| 2021-05-23 23:21:32 | <boxscape> | and then you can use [EUser a] directly |
| 2021-05-23 23:21:48 | → | nan` joins (~nan`@rrcs-70-60-83-42.central.biz.rr.com) |
| 2021-05-23 23:21:48 | <boxscape> | with the other definition there's still only one b for the entire list |
| 2021-05-23 23:22:13 | × | abrar quits (~abrar@static-108-30-103-121.nycmny.fios.verizon.net) (Ping timeout: 272 seconds) |
| 2021-05-23 23:23:12 | <Restle> | You could `type UserList a = [forall b. User a b]` I think |
| 2021-05-23 23:23:42 | <Restle> | Missed the constraint but I'm falling asleep at the keyboard, time to logoff I think |
| 2021-05-23 23:23:52 | <boxscape> | seems like it would have to be `type UserList a = [exists b . Hash b => User a b]` no? |
| 2021-05-23 23:24:03 | <boxscape> | (except of course we don't have the exists keyword yet) |
| 2021-05-23 23:24:28 | <Restle> | exists can _always_ be transformed into some Rank N of forall though no? |
| 2021-05-23 23:24:48 | <boxscape> | yes, exists n . P n = forall r (forall n . P n -> r) -> r, I believe |
| 2021-05-23 23:25:02 | → | kaskal joins (~user@2001:4bb8:2e8:6ec5:e985:ebf:4001:b154) |
| 2021-05-23 23:26:20 | ← | kaskal parts (~user@2001:4bb8:2e8:6ec5:e985:ebf:4001:b154) () |
| 2021-05-23 23:27:04 | × | nan` quits (~nan`@rrcs-70-60-83-42.central.biz.rr.com) (Quit: Computer is sleeping. ZZZzzz…) |
| 2021-05-23 23:27:10 | × | Gurkenglas__ quits (~Gurkengla@dslb-088-075-022-175.088.075.pools.vodafone-ip.de) (Ping timeout: 264 seconds) |
| 2021-05-23 23:28:27 | × | heath quits (~heath@68.68.64.38) (Ping timeout: 264 seconds) |
| 2021-05-23 23:33:47 | × | epolanski quits (uid312403@id-312403.brockwell.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-05-23 23:34:01 | → | kaskal joins (~user@2001:4bb8:2e8:6ec5:e985:ebf:4001:b154) |
| 2021-05-23 23:35:01 | × | space-shell quits (5862f726@107.161.19.109) (Quit: Connection closed) |
| 2021-05-23 23:37:57 | × | kaskal quits (~user@2001:4bb8:2e8:6ec5:e985:ebf:4001:b154) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2021-05-23 23:38:34 | → | heath joins (~heath@68.68.64.38) |
| 2021-05-23 23:40:56 | × | WikiLycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 2021-05-23 23:46:45 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2021-05-23 23:49:21 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-05-23 23:50:32 | → | koolazer joins (~koolazer@user/koolazer) |
| 2021-05-23 23:53:31 | × | juhp quits (~juhp@128.106.188.199) (Quit: juhp) |
| 2021-05-23 23:53:45 | → | juhp joins (~juhp@128.106.188.199) |
| 2021-05-23 23:55:38 | Carter | is now known as carter_ |
| 2021-05-23 23:55:41 | carter_ | is now known as carter |
| 2021-05-23 23:56:15 | → | kaskal joins (~user@2001:4bb8:2e8:6ec5:e985:ebf:4001:b154) |
| 2021-05-24 00:03:55 | → | kaskal_ joins (~kaskal@cqc02.itp.tuwien.ac.at) |
| 2021-05-24 00:09:20 | <ski> | Restle : no, `[forall b. User a b]' is very different |
| 2021-05-24 00:10:41 | → | daenth joins (~textual@162.218.217.186) |
| 2021-05-24 00:10:46 | × | kaskal_ quits (~kaskal@cqc02.itp.tuwien.ac.at) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 2021-05-24 00:12:19 | × | daenth quits (~textual@162.218.217.186) (Quit: Textual IRC Client: www.textualapp.com) |
| 2021-05-24 00:12:33 | → | kaskal_ joins (~kaskal@cqc02.itp.tuwien.ac.at) |
| 2021-05-24 00:13:35 | × | dtman34 quits (~dtman34@c-73-62-246-247.hsd1.mn.comcast.net) (Quit: ZNC 1.7.2+deb3 - https://znc.in) |
| 2021-05-24 00:15:31 | boxscape | sighs |
| 2021-05-24 00:15:37 | × | chddr quits (~Thunderbi@91.226.34.182) (Ping timeout: 272 seconds) |
| 2021-05-24 00:15:39 | <boxscape> | I so often want Bool to have a Monoid instance for && |
| 2021-05-24 00:15:43 | × | kewa quits (~kewa@5.138.148.77) (Ping timeout: 265 seconds) |
| 2021-05-24 00:15:52 | <boxscape> | so I can do `predicate1 <> predicate2 :: a -> Bool` |
| 2021-05-24 00:16:41 | <boxscape> | (without messing around with newtypes, because at that point I might as well write it all out) |
| 2021-05-24 00:20:22 | <boxscape> | Alternatively I guess (&&) and (||) could be methods of some class and `a -> Bool` could be an instance of that class |
| 2021-05-24 00:20:37 | × | kaskal_ quits (~kaskal@cqc02.itp.tuwien.ac.at) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 2021-05-24 00:20:59 | → | kaskal_ joins (~kaskal@cqc02.itp.tuwien.ac.at) |
| 2021-05-24 00:21:15 | <boxscape> | hm, maybe that's something to put in a custom prelude when I use one, that avoids the orphan instances |
| 2021-05-24 00:22:00 | <boxscape> | ...or just import the Boolean package :) |
| 2021-05-24 00:24:18 | carter | is now known as cartazio |
| 2021-05-24 00:24:34 | cartazio | is now known as Carter |
| 2021-05-24 00:27:09 | → | horex539 joins (~horex539@2a02:a03f:6aa5:a00:64fb:7080:45f7:39d3) |
| 2021-05-24 00:29:43 | <doyougnu> | boxscape: isn't Data.Monoid.All and Data.Monoid.Any what you're looking for? |
| 2021-05-24 00:30:20 | <boxscape> | doyougnu, no, because if I used that, it would be significantly longer and less readable than `\c -> predicate1 c && predicate2 c` |
| 2021-05-24 00:30:39 | <dmwit> | doyougnu: I don't think so, that's the wrong direction: it's one class, where you can pick (&&) or (||) depending on which instance you get. I think boxscape wants one class with (&&) and (||) that you can implement for many types. |
| 2021-05-24 00:30:55 | <boxscape> | yes |
| 2021-05-24 00:31:06 | <dmwit> | :t liftA2 (&&) |
| 2021-05-24 00:31:07 | <lambdabot> | Applicative f => f Bool -> f Bool -> f Bool |
| 2021-05-24 00:31:16 | <boxscape> | okay yes that is better than using All |
| 2021-05-24 00:31:28 | <boxscape> | but I wish we had a way to use liftA2 in a nice looking way with operators |
| 2021-05-24 00:31:47 | <dmwit> | Actually, maybe doyougnu has got more going for him than you might think. (<>) does actually work on functions if they return an All or an Any. |
| 2021-05-24 00:32:03 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds) |
| 2021-05-24 00:32:05 | × | horex539 quits (~horex539@2a02:a03f:6aa5:a00:64fb:7080:45f7:39d3) (Ping timeout: 272 seconds) |
| 2021-05-24 00:32:14 | <dmwit> | But what are the chances your functions return one of those instead of a Bool? Pretty small. |
| 2021-05-24 00:32:27 | <doyougnu> | dmwit: ah I see |
| 2021-05-24 00:32:49 | <dmwit> | boxscape: I think the numeric prelude does have a suitable class. |
| 2021-05-24 00:32:53 | <Axman6> | So glad to see how active this channel has become so quickly! |
| 2021-05-24 00:32:57 | <dmwit> | So that could be one route. |
| 2021-05-24 00:33:16 | <boxscape> | I'll check it out, thanks |
| 2021-05-24 00:33:58 | <doyougnu> | I wonder if you could do something like this with GADTs, that would allow the Applicative f to take on different instances depending on the sub-ADT right? |
| 2021-05-24 00:35:37 | <dmwit> | boxscape: http://hackage.haskell.org/package/numeric-prelude-0.4.3.3/docs/Algebra-Lattice.html, I think. |
| 2021-05-24 00:35:56 | <boxscape> | ah, thanks |
| 2021-05-24 00:36:04 | <boxscape> | % :t getAll <$> ((All <$> isSpace) <> (All <$> (/= '\n'))) -- this is the best I can think of with All |
| 2021-05-24 00:36:04 | <yahb> | boxscape: Char -> Bool |
| 2021-05-24 00:36:10 | <dmwit> | Looks like it doesn't have a function instance, but it easily can I think. |
| 2021-05-24 00:36:32 | <dmwit> | % :t getAll . (All . isSpace) <> (All . (/= '\n')) |
| 2021-05-24 00:36:32 | <yahb> | dmwit: ; <interactive>:1:30: error:; * Couldn't match type `All' with `Bool'; Expected: Char -> Bool; Actual: Char -> All; * In the second argument of `(<>)', namely `(All . (/= '\n'))'; In the expression: getAll . (All . isSpace) <> (All . (/= '\n')) |
| 2021-05-24 00:36:40 | <dmwit> | % :t getAll . ((All . isSpace) <> (All . (/= '\n'))) |
| 2021-05-24 00:36:40 | <yahb> | dmwit: Char -> Bool |
| 2021-05-24 00:36:44 | <boxscape> | ah yes that is better |
| 2021-05-24 00:37:04 | <dmwit> | % :t ala |
| 2021-05-24 00:37:04 | <yahb> | dmwit: forall {f :: * -> *} {s} {t}. (Functor f, Rewrapped s t, Rewrapped t s) => (Unwrapped s -> s) -> ((Unwrapped t -> t) -> f s) -> f (Unwrapped s) |
| 2021-05-24 00:37:13 | <dmwit> | % :t ala All |
| 2021-05-24 00:37:13 | <yahb> | dmwit: forall {f :: * -> *}. Functor f => ((Bool -> All) -> f All) -> f Bool |
| 2021-05-24 00:37:50 | <dmwit> | Oh, this is a different ala than I was hoping for. |
| 2021-05-24 00:38:09 | <boxscape> | % :i ala |
| 2021-05-24 00:38:09 | <yahb> | boxscape: ala :: forall (f :: * -> *) s t. (Functor f, Rewrapping s t) => (Unwrapped s -> s) -> ((Unwrapped t -> t) -> f s) -> f (Unwrapped s) -- Defined in `Control.Lens.Wrapped' |
| 2021-05-24 00:41:59 | → | scrazen joins (~scrazen@user/scrazen) |
| 2021-05-24 00:42:02 | <boxscape> | various preludes also have <&&> |
| 2021-05-24 00:42:38 | × | kaskal_ quits (~kaskal@cqc02.itp.tuwien.ac.at) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 2021-05-24 00:42:57 | → | kaskal_ joins (~kaskal@cqc02.itp.tuwien.ac.at) |
| 2021-05-24 00:43:52 | <dmwit> | I wouldn't object to having a Heyting algebra class that `if` was polymorphic over. |
| 2021-05-24 00:44:16 | <boxscape> | I guess that's possible with -XRebindableSyntax |
| 2021-05-24 00:44:25 | <dmwit> | yep |
| 2021-05-24 00:44:43 | <mniip> | why would that be a heyting algebra |
| 2021-05-24 00:46:07 | <dmwit> | You need a lub and glb to stand in for (&&) and (||), and you need either an upper or a lower bound so if can make a choice. |
| 2021-05-24 00:47:53 | <dmwit> | I guess there are weaker structures than Heyting algebra that would be good enough. |
| 2021-05-24 00:48:01 | bens_ | is now known as bens |
All times are in UTC.