Logs: liberachat/#haskell
| 2021-08-10 06:11:22 | <Gurkenglas> | Ah, I suppose I am just arguing about definitions if you're aware of the situations. |
| 2021-08-10 06:11:40 | → | qbt joins (~edun@user/edun) |
| 2021-08-10 06:12:02 | <euouae> | I know a little bit about it from the math side |
| 2021-08-10 06:12:10 | <euouae> | But I know little about Haskell and its formalizaiton |
| 2021-08-10 06:12:26 | <Gurkenglas> | Might be good to note that Hask is technically not a category, though that's a statement for party poopers and it's so-called morally correct to pretend |
| 2021-08-10 06:12:48 | <euouae> | I've heard of that too. Something about System-F or such maybe system-w it was |
| 2021-08-10 06:13:06 | <euouae> | Yeah it's two steps from being a category, you need some system and then you need to adjoint something to it |
| 2021-08-10 06:13:29 | → | Obo joins (~roberto@70.pool90-171-81.dynamic.orange.es) |
| 2021-08-10 06:13:31 | <euouae> | Probably not worthwhile talking about without me getting deeper into it... if ever |
| 2021-08-10 06:13:36 | × | Obo quits (~roberto@70.pool90-171-81.dynamic.orange.es) (Client Quit) |
| 2021-08-10 06:13:46 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-08-10 06:14:03 | <Gurkenglas> | https://hackage.haskell.org/package/kan-extensions-5.2.3/docs/Data-Functor-Yoneda.html reifies (is that the word?) the yoneda lemma |
| 2021-08-10 06:15:32 | <euouae> | Looks like there's a nice informative blog post linked there, thanks |
| 2021-08-10 06:16:51 | <Gurkenglas> | Is there a language that goes above and beyond in its type inference, such as by inferring from "a + b + c" that + must be associative and adding that as a theorem that needs to be proven by the compiler? |
| 2021-08-10 06:17:42 | × | euouae quits (~euouae@user/euouae) (Quit: thank you, off to lunch) |
| 2021-08-10 06:19:22 | <Gurkenglas> | Or perhaps, given a % b § c it might infer that out of the two ways to add parentheses, each that compiles must come out the same way |
| 2021-08-10 06:20:41 | <c_wraith> | that seems like a level of inference not supported by standard conventions. a + b * c is usually expected to parse only one way |
| 2021-08-10 06:21:05 | → | curiousgay joins (~curiousga@77-120-186-48.kha.volia.net) |
| 2021-08-10 06:21:18 | <Gurkenglas> | then i suppose i am asking for a language above and beyond the standard conventions >:P |
| 2021-08-10 06:21:27 | <c_wraith> | I suppose you could say that it only applies to pairs of operators that don't have a precedence specified |
| 2021-08-10 06:22:03 | <c_wraith> | make a partial order out of precedences. |
| 2021-08-10 06:22:06 | <hsek[m]> | Is there a way to unset a tool with `ghcup`? For times I don't want it to be present in path at all. |
| 2021-08-10 06:22:13 | <Gurkenglas> | yeah, of course you can add a theorem that the one way to place parantheses compiles, and a command that the other doesn't. |
| 2021-08-10 06:22:26 | <c_wraith> | hsek[m]: see if "ghcup tui" makes sense to you |
| 2021-08-10 06:22:44 | <c_wraith> | hsek[m]: unless you mean one specific tool, rather than a whole distribution. I don't think it handles that |
| 2021-08-10 06:23:15 | <Gurkenglas> | even a language that only goes to the "infer associativity theorem to prove" level would be neat if you know one :) |
| 2021-08-10 06:23:38 | <hsek[m]> | c_wraith: Yeah there seems to only be a set option, same with the CLI. :( |
| 2021-08-10 06:24:34 | → | Akronymus joins (~Akronymus@85.31.8.181) |
| 2021-08-10 06:24:52 | <c_wraith> | Gurkenglas: Haskell is almost there. Just change the default fixity to infix rather than infixl |
| 2021-08-10 06:25:13 | <c_wraith> | Gurkenglas: well. it won't force you to prove anything, but it'll reject the code! |
| 2021-08-10 06:25:32 | <Gurkenglas> | force me to prove? it should try on its own, first. |
| 2021-08-10 06:25:59 | → | Obo joins (~roberto@70.pool90-171-81.dynamic.orange.es) |
| 2021-08-10 06:26:33 | <Gurkenglas> | (and then if it can't the error should be worded as a difficulty with a "uh help me compile this pls", unless it can disprove the theorem) |
| 2021-08-10 06:26:37 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-08-10 06:26:47 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-08-10 06:26:54 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-08-10 06:26:59 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-08-10 06:27:27 | <Gurkenglas> | here's some insane musing i did in an imagined language https://gist.github.com/Gurkenglas/9f02cfeba04b35e178753ae4663349ef a$b % c is sugar for (a $ b) % c |
| 2021-08-10 06:28:24 | × | ham quits (~ham4@user/ham) (Ping timeout: 256 seconds) |
| 2021-08-10 06:28:39 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 2021-08-10 06:29:58 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 272 seconds) |
| 2021-08-10 06:30:32 | <Gurkenglas> | or i should say, for any operation %, a%b is sugar for (a % b) |
| 2021-08-10 06:31:13 | <edwardk> | Gurkenglas: http://comonad.com/haskell/Category.k is from an old toy language of mine |
| 2021-08-10 06:31:18 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2021-08-10 06:31:39 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 258 seconds) |
| 2021-08-10 06:31:52 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2021-08-10 06:32:14 | Gurkenglas | starstruck |
| 2021-08-10 06:32:15 | <edwardk> | the key there was that types were purely for code reuse |
| 2021-08-10 06:32:54 | <Gurkenglas> | Did your work at miri produce any language innovations? |
| 2021-08-10 06:33:50 | <edwardk> | when i get some more time, now that i'm at groq, and miri has mostly greenlit me to open up things i think aren't infohazard-ish, i'll see what i can put in the public space. there's still a fair bit of coda i'd like to do. |
| 2021-08-10 06:34:05 | <edwardk> | and i want to get that stuff and my LF work out there. |
| 2021-08-10 06:34:09 | × | pe200012 quits (~pe200012@113.105.10.33) (Ping timeout: 248 seconds) |
| 2021-08-10 06:34:24 | → | pe200012 joins (~pe200012@218.107.49.28) |
| 2021-08-10 06:34:46 | × | MorrowM quits (~Morrow@176.12.187.199) (Read error: Connection reset by peer) |
| 2021-08-10 06:34:53 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:3fc0:c335:9234:c2e2) |
| 2021-08-10 06:35:05 | → | MorrowM joins (~Morrow@176.12.187.199) |
| 2021-08-10 06:35:35 | <edwardk> | to read the code above basically it uses a sort of 'additive' adjective system, where adjectives can add traits to a noun contextually. and in the end ties the knot on the definition based on the fixed point of all the stuff you inherit through this strictly positive process |
| 2021-08-10 06:36:00 | <edwardk> | but this was from like 12-13 years ago when i was just learning haskell |
| 2021-08-10 06:36:38 | → | ham joins (~ham4@user/ham) |
| 2021-08-10 06:37:20 | <Gurkenglas> | Have you benefited from any NLP-based tools yet, such as for alerting you of IRC conversations you may find interesting? |
| 2021-08-10 06:37:21 | <edwardk> | the other weird feature is 'grey boxing' which lets you define result records/products returned from functions field-by-field |
| 2021-08-10 06:38:10 | <edwardk> | did my descent into the middle of this one give you that impression? |
| 2021-08-10 06:39:49 | <edwardk> | my system there is pretty boring. i have rotating list of keywords i swap out every day or so to keep me from getting too annoyed at getting too many false positives too frequently for the same thing |
| 2021-08-10 06:40:05 | <edwardk> | and if i don't like what it pops up i prune the list pretty aggressively |
| 2021-08-10 06:40:59 | <Gurkenglas> | It's a simple-enough sounding tool I would want that it seemed like an easy sell, and one I hoped the top researchers had. |
| 2021-08-10 06:41:35 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-08-10 06:41:43 | <Gurkenglas> | A step further would be telling GPT to summarize IRC logs. |
| 2021-08-10 06:42:05 | <edwardk> | good language models are stupid expensive to train, and need lots of good source data, while old style NLP is stupidly bad at its job. |
| 2021-08-10 06:42:49 | <Gurkenglas> | Modern language models are good across many tasks, though! |
| 2021-08-10 06:43:08 | <Gurkenglas> | Surely all of miri had GPT-3 access handed to them on a silver platter... |
| 2021-08-10 06:44:50 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2021-08-10 06:45:01 | <edwardk> | I hate to disillusion you, but I mostly played around with it through early AI Dungeon dragon model access myself. =P |
| 2021-08-10 06:45:59 | <edwardk> | that said, it did produce some pretty funny fake eliezer dialogues. |
| 2021-08-10 06:46:03 | <Gurkenglas> | A simple alert implementation would finetune an LM to predict #haskell logs and alert you when it predicts a sufficient probability that you reply. |
| 2021-08-10 06:46:17 | <edwardk> | yeah that's how i'd do it myself |
| 2021-08-10 06:46:47 | <edwardk> | of course, then it'd mostly just learn my existing keyword rotation ;) |
| 2021-08-10 06:47:26 | <edwardk> | and er.. quite how seasonal the rotation of ideas i care about is |
| 2021-08-10 06:47:53 | <Gurkenglas> | Do you have a log of your keyword rotation? You could insert the alert events into the log, and alert you when it predicts that you replied but weren't alerted by the keyword system. |
| 2021-08-10 06:48:24 | <edwardk> | if i had any foresight when writing the little perl script that would totally have been a great idea |
| 2021-08-10 06:48:31 | × | shriekingnoise quits (~shrieking@186.137.144.80) (Quit: Quit) |
| 2021-08-10 06:48:44 | <Gurkenglas> | May I take this moment to suggest that you log your daily internal monologue if this does not significantly reduce your productivity. |
| 2021-08-10 06:48:51 | <Gurkenglas> | Like, all the time. Maybe just install a keylogger |
| 2021-08-10 06:49:00 | <Gurkenglas> | Then 2 years from now, tell GPT-5 to tell you what you missed. |
| 2021-08-10 06:49:22 | <edwardk> | so many passwords getting fed to gpt-5 ;) |
| 2021-08-10 06:49:45 | <Gurkenglas> | In 1.9 years, tell your local GPT-3 instance to scrub passwords. |
| 2021-08-10 06:50:33 | <Gurkenglas> | The password problem has low enough probability of being unsolvable that the potential upside should be worth it! |
| 2021-08-10 06:52:04 | → | lortabac_ joins (~lortabac@2a01:e0a:541:b8f0:38bf:81bf:24b:2c61) |
| 2021-08-10 06:52:12 | <Gurkenglas> | Do you still use a trivial development environment? Have you tried copilot? |
| 2021-08-10 06:52:31 | <Gurkenglas> | Copilot seems most useful when you're working in an unfamiliar language |
| 2021-08-10 06:54:07 | <edwardk> | i occasionally use TabNine and let it's kinda crappy language model and language server support comingle. i've yet to jump over to Copilot. i find though that the tabnine suggestions want to take up screen space i usually prefer to use to read my code, so i often toggle it off completely. |
| 2021-08-10 06:54:28 | <Gurkenglas> | (Or in a strong enough type system, I suppose - filtering a thousand completions for the shortest one that compiles must come in handy) |
| 2021-08-10 06:54:42 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
| 2021-08-10 06:54:49 | × | shredder quits (~user@user/shredder) (Quit: quitting) |
| 2021-08-10 06:54:55 | <edwardk> | the filtering language model completions thing is _much_ nearer and dearer to my heart as an approximation of the right thing to do |
| 2021-08-10 06:55:39 | <edwardk> | i'd prefer something using a masked language model myself, and something more suited to haskell identation conventions, etc. |
| 2021-08-10 06:55:58 | <edwardk> | but i also don't want to spend several million dollars training a model today. |
| 2021-08-10 06:56:09 | → | shredder joins (~user@user/shredder) |
| 2021-08-10 06:56:22 | <edwardk> | will wait until i can get groq chips to train language models ;) |
| 2021-08-10 06:56:34 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:3fc0:c335:9234:c2e2) (Ping timeout: 272 seconds) |
| 2021-08-10 06:56:37 | <Gurkenglas> | Indentation surely cant be a serious problem. Send the .hs through an isomorphism that strips the whitespace before you get completions |
All times are in UTC.