Logs: liberachat/#haskell
| 2025-10-09 16:27:42 | → | gustrb joins (~gustrb@191.243.134.87) |
| 2025-10-09 16:30:00 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 2025-10-09 16:30:40 | → | Googulator3 joins (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) |
| 2025-10-09 16:30:43 | × | Googulator37 quits (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-09 16:33:17 | → | GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano) |
| 2025-10-09 16:33:29 | × | GdeVolpiano quits (~GdeVolpia@user/GdeVolpiano) (Client Quit) |
| 2025-10-09 16:38:45 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-10-09 16:43:38 | × | trickard_ quits (~trickard@cpe-52-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-09 16:43:52 | → | trickard_ joins (~trickard@cpe-52-98-47-163.wireline.com.au) |
| 2025-10-09 16:47:16 | → | ulysses4ever joins (~artem@2601:249:4380:2400:1772:84b0:3058:898) |
| 2025-10-09 16:52:17 | × | gustrb quits (~gustrb@191.243.134.87) (Remote host closed the connection) |
| 2025-10-09 16:53:00 | → | GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano) |
| 2025-10-09 16:55:35 | → | Square2 joins (~Square@user/square) |
| 2025-10-09 16:59:19 | × | Square quits (~Square4@user/square) (Ping timeout: 240 seconds) |
| 2025-10-09 17:02:13 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 260 seconds) |
| 2025-10-09 17:11:19 | × | trickard_ quits (~trickard@cpe-52-98-47-163.wireline.com.au) (Ping timeout: 244 seconds) |
| 2025-10-09 17:11:45 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 2025-10-09 17:11:48 | → | trickard joins (~trickard@cpe-52-98-47-163.wireline.com.au) |
| 2025-10-09 17:15:34 | <dminuoso> | yin: Type tetris is not a well defined term, but usually refers to some act where you shuffle/turn things until they type check, much like you would rotate pieces in tetris until they fit. |
| 2025-10-09 17:15:44 | → | Googulator63 joins (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) |
| 2025-10-09 17:15:44 | × | Googulator3 quits (~Googulato@2a01-036d-0106-03fa-5967-6f2a-1e2d-f05a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-09 17:16:24 | <dminuoso> | Some people use them in different cases, but they all usually somehow revolve around making things fit to please the type checker, sometimes (but not always) without even knowing why or how it worked. |
| 2025-10-09 17:16:55 | <dminuoso> | In some silly sense programming can be a kind of computer game in this way. |
| 2025-10-09 17:17:07 | <dminuoso> | You win once your program type checks. |
| 2025-10-09 17:17:25 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 264 seconds) |
| 2025-10-09 17:19:06 | <EvanR> | tetris is too hard |
| 2025-10-09 17:19:13 | <EvanR> | much prefer making types fit |
| 2025-10-09 17:19:46 | <EvanR> | a master of tetris might feel like he's playing type theory |
| 2025-10-09 17:20:29 | <dminuoso> | I think it's most notable when you're relatively early in the haskell career (or early into stepping into more complicatedly typed libraries), where you dont really understand what you're doing, but sometimes if it type checks, its more likely to be correct than not. |
| 2025-10-09 17:20:42 | <APic> | But the epic Alexei Paschitnow brought it to us in the 1984! |
| 2025-10-09 17:22:23 | <EvanR> | I have noticed that in a complicated but well design library, just getting the types to check without knowing wtf you're doing "somehow works" |
| 2025-10-09 17:23:16 | <EvanR> | 1984 corresponds to the development of martin-lof type theory |
| 2025-10-09 17:23:23 | <EvanR> | coincidence? I think not |
| 2025-10-09 17:23:30 | <dminuoso> | Personally I think it's an indicator of poor documentation or over complication, if the only way for you to interact is to randomly slap things together until they fit. |
| 2025-10-09 17:24:06 | <EvanR> | for some highly algebraic systems, I do not envy anyone trying to use it or invent it without types |
| 2025-10-09 17:24:13 | <dminuoso> | Imagine this is how you had to assemble anything, say a model car. |
| 2025-10-09 17:24:29 | <EvanR> | which is why you see typeless system devolve into the dumbest common denominator "write the rest yourself" |
| 2025-10-09 17:24:33 | <dminuoso> | Certainly good to waste ones time like puzzling, but I dont think people write Haskell to waste time. |
| 2025-10-09 17:25:10 | <EvanR> | it really wins when the only sensible ways to combine things is the algebraically correct way |
| 2025-10-09 17:25:24 | <EvanR> | without types, that's just hazardous |
| 2025-10-09 17:25:30 | <dminuoso> | EvanR: It's good for robustness, but it shouldn't be the way we guide programmers to the conclusion. |
| 2025-10-09 17:25:55 | <dminuoso> | Imagine Airbus had their engineers assemble helicopters this way. |
| 2025-10-09 17:26:01 | <dminuoso> | "Slap things until they fit, it will be alright" |
| 2025-10-09 17:26:04 | <EvanR> | whether any of this is actually good for programming might just reflect what we think programming even is |
| 2025-10-09 17:26:15 | <dminuoso> | Even *if* it worked, it would be horrible in terms of efficiency. |
| 2025-10-09 17:26:34 | <EvanR> | is it writing a random script to get some job done as fast as possible, or is it proving a theorem in a way that a computer could check it |
| 2025-10-09 17:26:49 | <EvanR> | or many other scenarios |
| 2025-10-09 17:27:19 | × | dyno quits (dyno@user/dyno) (Ping timeout: 260 seconds) |
| 2025-10-09 17:27:25 | × | karenw quits (~karenw@user/karenw) (Ping timeout: 256 seconds) |
| 2025-10-09 17:29:57 | <dminuoso> | Here's a fun set of interfaces: |
| 2025-10-09 17:30:22 | <dminuoso> | f1 :: T r r -> T r' r; f2 :: ((a -> r) -> T r r) -> T r a |
| 2025-10-09 17:30:59 | <dminuoso> | Now the type signatures pretty much tell you all there is to know. It's a terribly confusing API. |
| 2025-10-09 17:32:23 | <dminuoso> | Now `T ~ Cont` of course. |
| 2025-10-09 17:33:28 | <EvanR> | it doens't seem that confusing |
| 2025-10-09 17:33:47 | <EvanR> | this mistakes one letter variable names with "intrinsically confusing" |
| 2025-10-09 17:34:00 | <EvanR> | science and math works using them regardless |
| 2025-10-09 17:34:22 | <shapr> | @quote |
| 2025-10-09 17:34:22 | <lambdabot> | mueval-core says: <lambdabot> mueval-core: Time limit exceeded <mueval-core> lambdabot: stfu |
| 2025-10-09 17:34:25 | <EvanR> | if someone doesn't know the subject matter then yeah they might be confused, personally |
| 2025-10-09 17:34:28 | <shapr> | ow, burn |
| 2025-10-09 17:34:55 | <tomsmeding> | lol shapr |
| 2025-10-09 17:34:59 | <dminuoso> | EvanR: Dunno, I find the interface (and all of the resulting program structure) of delimited continuations pure confusion. |
| 2025-10-09 17:35:02 | <shapr> | howdy tomsmeding, how's code? |
| 2025-10-09 17:35:08 | <EvanR> | I can't argue with that |
| 2025-10-09 17:35:26 | <shapr> | I've been playing with the TUI graph library granite, having fun recreating the graphs from Thinking in Systems by Donella Meadows |
| 2025-10-09 17:35:27 | <tomsmeding> | code is okay, phd thesis is also okay |
| 2025-10-09 17:35:38 | <shapr> | oh nice, self education |
| 2025-10-09 17:35:39 | <tomsmeding> | the latter will be handed in somewhere the coming few months |
| 2025-10-09 17:35:44 | <shapr> | w00! what did you write about? |
| 2025-10-09 17:35:49 | <tomsmeding> | automatic differentiation! |
| 2025-10-09 17:35:53 | <[exa]> | oh cool |
| 2025-10-09 17:36:07 | <shapr> | nice! any papers I can read? |
| 2025-10-09 17:36:08 | tomsmeding | looks up granite |
| 2025-10-09 17:36:22 | <shapr> | I'm doing this kind of thing: https://github.com/mchav/granite?tab=readme-ov-file#line-graph |
| 2025-10-09 17:36:34 | <tomsmeding> | oh that thing, didn't that appear in the HWN at some point? |
| 2025-10-09 17:36:41 | <tomsmeding> | yeah that's snazzy |
| 2025-10-09 17:36:49 | <dminuoso> | Even with plain continuations with things like callCC it gets rather confusing. In C-world something like setjmp/longjmp is just far easier to conceptualize, and it feels easier when reading programs. |
| 2025-10-09 17:37:03 | <shapr> | I dunno, I just found it last week or so |
| 2025-10-09 17:37:06 | <dminuoso> | Just because you can express it with a function does not mean its the best of ideas. :-) |
| 2025-10-09 17:37:24 | <[exa]> | granite was somewhat popular on discourse recently no? |
| 2025-10-09 17:37:45 | <EvanR> | yes "everything is a function" is as dumb as "everything's an object" |
| 2025-10-09 17:37:58 | <EvanR> | or everything is a set |
| 2025-10-09 17:38:04 | <[exa]> | EvanR: ENTITY. |
| 2025-10-09 17:38:05 | <dminuoso> | The "everything is an object" at least is introspectable easily. |
| 2025-10-09 17:38:21 | <tomsmeding> | shapr: I'll do you a better one, here is an extremely-hot-off-the-press current draft of the entire bloody thing https://tomsmeding.com/vang/EZ5CNw/thesis-2025-10-09.pdf |
| 2025-10-09 17:38:26 | <shapr> | w00! |
| 2025-10-09 17:38:35 | <EvanR> | is it |
| 2025-10-09 17:38:45 | <EvanR> | then introspect functions, which are objects, because everything is |
| 2025-10-09 17:39:04 | <EvanR> | actually you can do this in idris, or at least you used to |
| 2025-10-09 17:39:07 | <tomsmeding> | shapr: warning: it's long lol |
| 2025-10-09 17:39:34 | <[exa]> | tomsmeding: man that's LOONG |
| 2025-10-09 17:39:38 | <shapr> | tomsmeding: I think you gotta `unset SOURCE_DATE_EPOCH` |
| 2025-10-09 17:39:53 | <tomsmeding> | [exa]: it is, send help |
| 2025-10-09 17:39:57 | <tomsmeding> | shapr: hm? |
| 2025-10-09 17:40:16 | <shapr> | mind you, my Dutch is terrible, is "geboren op 21 februari 1998" supposed to be the date you built the document? |
| 2025-10-09 17:40:16 | <tomsmeding> | [exa]: note that this is B5 paper size, not A4 |
| 2025-10-09 17:40:25 | <tomsmeding> | shapr: "geboren" means "born" |
| 2025-10-09 17:40:28 | <tomsmeding> | ;) |
| 2025-10-09 17:40:34 | <shapr> | jaså, tack! |
| 2025-10-09 17:40:37 | jgart | is now known as whereiseveryone |
All times are in UTC.