Newest at the top
| 2025-12-01 23:12:59 +0100 | <tomsmeding> | assuming you're using the nvim builtin LSP client and not something else |
| 2025-12-01 23:12:39 +0100 | <tomsmeding> | (lua) |
| 2025-12-01 23:12:27 +0100 | <tomsmeding> | merijn: possibly add vim.lsp.enable('hls') afterwards |
| 2025-12-01 23:10:24 +0100 | <tomsmeding> | merijn: https://paste.tomsmeding.com/iS6vrndp |
| 2025-12-01 23:03:57 +0100 | <haskellbridge> | https://play.haskell.org/saved/9XWoHwsD |
| 2025-12-01 23:03:57 +0100 | <haskellbridge> | <zoil> i think this version should be interactive |
| 2025-12-01 23:02:27 +0100 | michalz | (~michalz@185.246.207.193) (Remote host closed the connection) |
| 2025-12-01 23:02:06 +0100 | <haskellbridge> | <zoil> i thought the ide would allow to share and edit and compile, but it makes it readonly |
| 2025-12-01 23:02:00 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-01 23:01:47 +0100 | <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 23:01:47 +0100 | <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 23:00:37 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/vssawUkriMdYrWhgxHeCbFgP/6JDVkeGWpLw (3 lines) |
| 2025-12-01 23:00:37 +0100 | <haskellbridge> | <zoil> data Transfers (xs :: Nonempty *) where |
| 2025-12-01 22:59:54 +0100 | <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:59:36 +0100 | <haskellbridge> | <zoil> https://kf8nh.com/_heisenbridge/media/matrix.org/GPGBChpFvPQwIjAnsVOZLpwr/D5DpfDeh0w0/image.png |
| 2025-12-01 22:58:03 +0100 | <merijn> | bad new, it's giving me stupid refactor instructions >.> |
| 2025-12-01 22:57:59 +0100 | <haskellbridge> | <zoil> so, on line 96 there is this terrifying constraint |
| 2025-12-01 22:57:42 +0100 | <merijn> | good news I got hls working |
| 2025-12-01 22:57:37 +0100 | <merijn> | hmm |
| 2025-12-01 22:57:34 +0100 | <haskellbridge> | <zoil> https://paste.tomsmeding.com/Z84KWqJO |
| 2025-12-01 22:57:33 +0100 | <haskellbridge> | <zoil> heres a paste if thats not easy to interface with |
| 2025-12-01 22:57:19 +0100 | rekahsoft | (~rekahsoft@70.51.99.245) (Ping timeout: 246 seconds) |
| 2025-12-01 22:57:13 +0100 | <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 22:54:58 +0100 | trickard_ | trickard |
| 2025-12-01 22:54:35 +0100 | <haskellbridge> | <zoil> can anyone see this? https://onlinegdb.com/mqdS1he_N |
| 2025-12-01 22:50:08 +0100 | <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 22:47:21 +0100 | <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 22:47:03 +0100 | <merijn> | What am I missing? |
| 2025-12-01 22:46:55 +0100 | <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 22:46:35 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2025-12-01 22:37:55 +0100 | <haskellbridge> | <zoil> i have enough time today to put together a working example |
| 2025-12-01 22:37:28 +0100 | <haskellbridge> | <zoil> they were saying something about having a type witness, eta something, and singletons |
| 2025-12-01 22:37:01 +0100 | <haskellbridge> | <zoil> (nets that have regularizers reweighting internal branches at neurons) |
| 2025-12-01 22:36:58 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-12-01 22:36:43 +0100 | <haskellbridge> | <zoil> i have time today, i got my code to compile |
| 2025-12-01 22:36:33 +0100 | <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 22:36:33 +0100 | <haskellbridge> | <zoil> can anyone help me understand this? |
| 2025-12-01 22:31:21 +0100 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) Anarchos |
| 2025-12-01 22:31:21 +0100 | <jreicher> | How did I miss that. I wonder if the grammars I built are the same. |
| 2025-12-01 22:30:40 +0100 | <tomsmeding> | jreicher: from the .js files in the grammar/ directory |
| 2025-12-01 22:30:30 +0100 | <jreicher> | What's the json generated from? I thought the json was written. |
| 2025-12-01 22:30:25 +0100 | <merijn> | I can't make heads of tails of that grammar and I wrote and graded quite a few |
| 2025-12-01 22:30:08 +0100 | <merijn> | tomsmeding: That's what *I* would do, but I certainly would make it more readable than that :p |
| 2025-12-01 22:30:02 +0100 | <tomsmeding> | the keys in operator.js for example make me think of the haskell grammar |
| 2025-12-01 22:29:42 +0100 | <tomsmeding> | merijn: I dunno, but wouldn't they just have faithfully implemented the haskell2010 grammar plus extensions? |
| 2025-12-01 22:29:13 +0100 | <tomsmeding> | I know _that_ much about treesitter :p |
| 2025-12-01 22:28:58 +0100 | <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 22:28:42 +0100 | <merijn> | That, yeah |
| 2025-12-01 22:28:38 +0100 | <tomsmeding> | no, it's javascript that is compiled to the json |
| 2025-12-01 22:28:36 +0100 | <merijn> | jreicher: The json isn't the grammar |
