2025/12/01

Newest at the top

2025-12-01 23:20:48 +0100Anarchos(~Anarchos@91-161-254-16.subs.proxad.net) (Quit: Vision[]: i've been blurred!)
2025-12-01 23:20:26 +0100 <haskellbridge> <zoil> idk what im supposed to do next
2025-12-01 23:19:52 +0100takuan(~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection)
2025-12-01 23:15:47 +0100 <haskellbridge> <zoil> i got to take a break for a bit now, that kind of used up my available programming energy
2025-12-01 23:15:19 +0100 <haskellbridge> <zoil> glguy also put this which might help; https://paste.tomsmeding.com/UEfrQUiN
2025-12-01 23:14:06 +0100 <haskellbridge> https://play.haskell.org/saved/9XWoHwsD
2025-12-01 23:14:06 +0100 <haskellbridge> <zoil> i put the extra bit for the refactoring;
2025-12-01 23:13:38 +0100 <merijn> tomsmeding: Yeah, I got it working, just need to figure out which stupid linters to turn on
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 +0100michalz(~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 +0100humasect(~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 +0100rekahsoft(~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 +0100trickard_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 +0100humasect(~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 +0100target_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 +0100Anarchos(~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