Logs: liberachat/#haskell
| 2025-12-01 21:28:38 | <tomsmeding> | no, it's javascript that is compiled to the json |
| 2025-12-01 21:28:42 | <merijn> | That, yeah |
| 2025-12-01 21:28:58 | <tomsmeding> | well, the json is the grammar, kind of, but in the same way that an LR parsing table is also "the grammar" |
| 2025-12-01 21:29:13 | <tomsmeding> | I know _that_ much about treesitter :p |
| 2025-12-01 21:29:42 | <tomsmeding> | merijn: I dunno, but wouldn't they just have faithfully implemented the haskell2010 grammar plus extensions? |
| 2025-12-01 21:30:02 | <tomsmeding> | the keys in operator.js for example make me think of the haskell grammar |
| 2025-12-01 21:30:08 | <merijn> | tomsmeding: That's what *I* would do, but I certainly would make it more readable than that :p |
| 2025-12-01 21:30:25 | <merijn> | I can't make heads of tails of that grammar and I wrote and graded quite a few |
| 2025-12-01 21:30:30 | <jreicher> | What's the json generated from? I thought the json was written. |
| 2025-12-01 21:30:40 | <tomsmeding> | jreicher: from the .js files in the grammar/ directory |
| 2025-12-01 21:31:21 | <jreicher> | How did I miss that. I wonder if the grammars I built are the same. |
| 2025-12-01 21:31:21 | → | Anarchos joins (~Anarchos@91-161-254-16.subs.proxad.net) |
| 2025-12-01 21:36:33 | <haskellbridge> | <zoil> can anyone help me understand this? |
| 2025-12-01 21:36:33 | <haskellbridge> | <zoil> zoil: You would need e.g. "data WhichNE xs where { IsCons :: WhichNE (Cons x xs); IsLast :: WhichNE (Last x) }; class KnownNE ne where { knownNE :: WhichNE ne }; <both instances>; instance KnownNE xs => Read (Transfers xs) where { read s = case knownNE of { ... } }". |
| 2025-12-01 21:36:43 | <haskellbridge> | <zoil> i have time today, i got my code to compile |
| 2025-12-01 21:36:58 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-12-01 21:37:01 | <haskellbridge> | <zoil> (nets that have regularizers reweighting internal branches at neurons) |
| 2025-12-01 21:37:28 | <haskellbridge> | <zoil> they were saying something about having a type witness, eta something, and singletons |
| 2025-12-01 21:37:55 | <haskellbridge> | <zoil> i have enough time today to put together a working example |
| 2025-12-01 21:46:35 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-12-01 21:46:55 | <merijn> | Spaking of neovim, I at one point had a working hls config, but apparently I broke it and now LspInfo claims there's no active langauge server? |
| 2025-12-01 21:47:03 | <merijn> | What am I missing? |
| 2025-12-01 21:47:21 | <fgarcia> | ski: i think possibly the inverses of functions. reading more about this though i am seeing the 'maps to' symbol,|->, being used for substition. there are other times where the arrow => is used, though i feel this one is not so nice the times i see it |
| 2025-12-01 21:50:08 | <ski> | fgarcia : i'm still not sure what context your original question was in. writing math or logic vernacular ? talking about syntax in programming languages ? programming idioms ? |
| 2025-12-01 21:54:35 | <haskellbridge> | <zoil> can anyone see this? https://onlinegdb.com/mqdS1he_N |
| 2025-12-01 21:54:58 | trickard_ | is now known as trickard |
| 2025-12-01 21:57:13 | <fgarcia> | ski: earlier i read the bracketed substitutions and thought those were referring to a written shorthand in text. some examples being [x/y] and [x:=y] which i have not seen in my limited experience |
| 2025-12-01 21:57:19 | × | rekahsoft quits (~rekahsoft@70.51.99.245) (Ping timeout: 246 seconds) |
| 2025-12-01 21:57:33 | <haskellbridge> | <zoil> heres a paste if thats not easy to interface with |
| 2025-12-01 21:57:34 | <haskellbridge> | <zoil> https://paste.tomsmeding.com/Z84KWqJO |
| 2025-12-01 21:57:37 | <merijn> | hmm |
| 2025-12-01 21:57:42 | <merijn> | good news I got hls working |
| 2025-12-01 21:57:59 | <haskellbridge> | <zoil> so, on line 96 there is this terrifying constraint |
| 2025-12-01 21:58:03 | <merijn> | bad new, it's giving me stupid refactor instructions >.> |
| 2025-12-01 21:59:36 | <haskellbridge> | <zoil> https://kf8nh.com/_heisenbridge/media/matrix.org/GPGBChpFvPQwIjAnsVOZLpwr/D5DpfDeh0w0/image.png |
| 2025-12-01 21:59:54 | <ski> | zoil : so the `KnownNE xs', when pattern-matching on the value of `knownNE', will inform the type-checker that either `xs = Cons x ys' or `xs = Last x' (for some unknown `x',`ys'), and then presumably that helps with `read' (ought to be `readsPrec', really) knowing what to expect (presumably `Transfers' is a GADT) |
| 2025-12-01 22:00:37 | <haskellbridge> | <zoil> data Transfers (xs :: Nonempty *) where |
| 2025-12-01 22:00:37 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/vssawUkriMdYrWhgxHeCbFgP/6JDVkeGWpLw (3 lines) |
| 2025-12-01 22:01:47 | <ski> | fgarcia : well, these are (somewhat) standard formal (meta-)notation, when talking about abstract syntax of programming languages, logics, specification languages, &c. |
| 2025-12-01 22:01:47 | <haskellbridge> | <zoil> so WhichNE is a singleton datatype? and it acts as a type witness allowing the instances to have just one class instance, and then it wont require the constraint? |
| 2025-12-01 22:02:00 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-01 22:02:06 | <haskellbridge> | <zoil> i thought the ide would allow to share and edit and compile, but it makes it readonly |
| 2025-12-01 22:02:27 | × | michalz quits (~michalz@185.246.207.193) (Remote host closed the connection) |
| 2025-12-01 22:03:57 | <haskellbridge> | <zoil> i think this version should be interactive |
| 2025-12-01 22:03:57 | <haskellbridge> | https://play.haskell.org/saved/9XWoHwsD |
| 2025-12-01 22:10:24 | <tomsmeding> | merijn: https://paste.tomsmeding.com/iS6vrndp |
| 2025-12-01 22:12:27 | <tomsmeding> | merijn: possibly add vim.lsp.enable('hls') afterwards |
| 2025-12-01 22:12:39 | <tomsmeding> | (lua) |
| 2025-12-01 22:12:59 | <tomsmeding> | assuming you're using the nvim builtin LSP client and not something else |
| 2025-12-01 22:13:38 | <merijn> | tomsmeding: Yeah, I got it working, just need to figure out which stupid linters to turn on |
| 2025-12-01 22:14:06 | <haskellbridge> | <zoil> i put the extra bit for the refactoring; |
| 2025-12-01 22:14:06 | <haskellbridge> | https://play.haskell.org/saved/9XWoHwsD |
| 2025-12-01 22:15:19 | <haskellbridge> | <zoil> glguy also put this which might help; https://paste.tomsmeding.com/UEfrQUiN |
| 2025-12-01 22:15:47 | <haskellbridge> | <zoil> i got to take a break for a bit now, that kind of used up my available programming energy |
| 2025-12-01 22:19:52 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2025-12-01 22:20:26 | <haskellbridge> | <zoil> idk what im supposed to do next |
| 2025-12-01 22:20:48 | × | Anarchos quits (~Anarchos@91-161-254-16.subs.proxad.net) (Quit: Vision[]: i've been blurred!) |
| 2025-12-01 22:24:31 | × | trickard quits (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-01 22:24:45 | → | trickard_ joins (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-01 22:24:51 | <haskellbridge> | <zoil> sory the paste didnt update |
| 2025-12-01 22:24:52 | <haskellbridge> | <zoil> here |
| 2025-12-01 22:24:55 | <haskellbridge> | <zoil> https://play.haskell.org/saved/GwyPOlmo |
| 2025-12-01 22:25:45 | <haskellbridge> | <zoil> so these whichNE are like type witnesses? |
| 2025-12-01 22:26:05 | <haskellbridge> | <zoil> i think im still going to end up picking up a constraint... |
| 2025-12-01 22:26:50 | <haskellbridge> | <zoil> like, i provide 2 instances which might help match in consequent instances |
| 2025-12-01 22:27:20 | <haskellbridge> | <zoil> but now im not going to be able to assert the exhaustive coverage of the singletons! |
| 2025-12-01 22:27:24 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-12-01 22:27:32 | <haskellbridge> | <zoil> this defies the whole point |
| 2025-12-01 22:27:38 | <haskellbridge> | <zoil> :-( |
| 2025-12-01 22:30:06 | → | st_aldini joins (~Thunderbi@2605:a601:a07c:7400:6e26:f360:f11d:472c) |
| 2025-12-01 22:32:09 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 250 seconds) |
| 2025-12-01 22:33:40 | × | trickard_ quits (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-01 22:34:46 | × | divlamir quits (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2025-12-01 22:34:57 | → | divlamir joins (~divlamir@user/divlamir) |
| 2025-12-01 22:36:13 | → | trickard_ joins (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-01 22:42:20 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-01 22:47:39 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 2025-12-01 22:48:00 | → | weary-traveler joins (~user@user/user363627) |
| 2025-12-01 22:53:56 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-01 22:57:47 | <haskellbridge> | <zoil> bah, what a waste of time |
| 2025-12-01 22:58:32 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-01 22:58:52 | <ski> | zoil : i would not call `WhichNE' a singleton, since it does not reflect the structure of the type index in the value (you can't recover the structure of the index, by pattern-matching on the value) |
| 2025-12-01 23:01:06 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-12-01 23:01:19 | → | peterbecich joins (~Thunderbi@172.222.148.214) |
| 2025-12-01 23:09:28 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-01 23:11:00 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-01 23:11:16 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-12-01 23:13:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-01 23:13:36 | × | tromp quits (~textual@2001:1c00:3487:1b00:9c00:2cdd:fe3f:e613) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-12-01 23:19:15 | → | Anarchos joins (~Anarchos@91-161-254-16.subs.proxad.net) |
| 2025-12-01 23:24:09 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 2025-12-01 23:24:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-01 23:28:34 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2025-12-01 23:29:33 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-12-01 23:33:55 | × | Tuplanolla quits (~Tuplanoll@91-152-225-194.elisa-laajakaista.fi) (Ping timeout: 240 seconds) |
| 2025-12-01 23:34:19 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 2025-12-01 23:40:14 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-01 23:41:01 | trickard_ | is now known as trickard |
| 2025-12-01 23:44:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-01 23:55:37 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
All times are in UTC.