Logs: liberachat/#haskell
| 2025-11-11 02:06:56 | <monochrom> | For students who are too used to pure math, especially the non-constructive one, I will have to bias them towards more explicit construction, even constructivism, yeah. |
| 2025-11-11 02:07:14 | <jreicher> | It cheers me even that those words might enter the classroom. |
| 2025-11-11 02:08:41 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-11 02:09:31 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-11-11 02:09:40 | <monochrom> | I teach basic Haskell and basic Curry. And some PL topics, e.g., grammars, parsing, type inference, parametricity. |
| 2025-11-11 02:10:04 | <monochrom> | Actually this! https://www.cs.utoronto.ca/~trebla/CSCC24-latest/ |
| 2025-11-11 02:12:04 | → | peterbecich joins (~Thunderbi@172.222.148.214) |
| 2025-11-11 02:12:55 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-11 02:13:28 | <jreicher> | Thanks for the link! |
| 2025-11-11 02:15:42 | → | Googulator53 joins (~Googulato@2a01-036d-0106-0180-8127-ba79-55a7-6f29.pool6.digikabel.hu) |
| 2025-11-11 02:15:46 | × | Googulator83 quits (~Googulato@2a01-036d-0106-0180-8127-ba79-55a7-6f29.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-11-11 02:24:24 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-11 02:26:35 | <jreicher> | What's the current implementation of delimited continuations in Haskell? Is it CC-delcont? |
| 2025-11-11 02:28:24 | <jreicher> | I thought there were ghc primops for them now... |
| 2025-11-11 02:28:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-11-11 02:30:20 | × | tabemann quits (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Remote host closed the connection) |
| 2025-11-11 02:30:54 | → | tabemann joins (~travisb@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 2025-11-11 02:31:17 | <geekosaur> | there are, but they have some limitations (for example, they have to be used in IO) |
| 2025-11-11 02:32:32 | <jreicher> | Do you know what happens if there's a different prompt between a control and its matching prompt? I imagine that "foreign" prompt is captured, but I wouldn't mind finding an explicit discussion of that case. |
| 2025-11-11 02:32:53 | <jreicher> | (I should rewatch Alex King's talk, probably) |
| 2025-11-11 02:32:56 | <jreicher> | Alexis |
| 2025-11-11 02:33:25 | <Leary> | Of course, it's captured. |
| 2025-11-11 02:33:48 | <monochrom> | Captured in the middle. The control searches for the matching prompt, captures everything between now and that. |
| 2025-11-11 02:34:36 | <EvanR> | jreicher, a function is not always implemented as a set in math |
| 2025-11-11 02:35:13 | <Leary> | jreicher: You might be interested in my (as yet unpublished) https://github.com/LSLeary/native-cont library; it provides a safe non-IO interface to the primops. |
| 2025-11-11 02:35:14 | <jreicher> | monochrom: yeah, that's what I expected. Can't shake the feeling it deserves explicit discussion, but maybe not. |
| 2025-11-11 02:35:41 | → | Googulator92 joins (~Googulato@2a01-036d-0106-0180-8127-ba79-55a7-6f29.pool6.digikabel.hu) |
| 2025-11-11 02:35:42 | <EvanR> | e.g. it could be implemented as a relation plus the functional condition, where relations are primitive |
| 2025-11-11 02:35:43 | × | Googulator53 quits (~Googulato@2a01-036d-0106-0180-8127-ba79-55a7-6f29.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-11-11 02:35:45 | <jreicher> | Leary: yes, thank you. |
| 2025-11-11 02:35:58 | <EvanR> | it could even be abstractified using category theory |
| 2025-11-11 02:36:21 | <jreicher> | EvanR: true, but I think even for relations I've seen more set-theoretic presentations than not. |
| 2025-11-11 02:36:31 | <EvanR> | which gives haskell room to call functions functions |
| 2025-11-11 02:36:35 | <monochrom> | Oh, type theory says functions are primitive. :) |
| 2025-11-11 02:37:27 | <jreicher> | I'm tempted to say that's because the type theory doesn't need to know the details... ;) |
| 2025-11-11 02:37:42 | <EvanR> | the structural set theory with sets elements and relations gets closer to type theory by emphasizing the domain and codomain of functions (relations) as the important part |
| 2025-11-11 02:37:56 | <EvanR> | instead of the implementation |
| 2025-11-11 02:38:58 | <EvanR> | even in "normal math" you really rarely care about what a function "really is" |
| 2025-11-11 02:39:49 | <EvanR> | even in normal programming, you rarely care about what an array "really is", hence the big O 1 array myth |
| 2025-11-11 02:40:10 | <monochrom> | Hell, s/array/hash table/g |
| 2025-11-11 02:40:25 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-11 02:40:29 | monochrom | is looking at Python and Perl. |
| 2025-11-11 02:41:38 | <EvanR> | so perl and PHP were justified in calling their hashtable "array" xD |
| 2025-11-11 02:42:31 | <geekosaur> | perl didn't call it array, @x is not %x |
| 2025-11-11 02:42:42 | <geekosaur> | they called it list |
| 2025-11-11 02:43:32 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-11-11 02:44:09 | <EvanR> | oh list is a hashtable? |
| 2025-11-11 02:44:20 | <EvanR> | even better |
| 2025-11-11 02:44:31 | <monochrom> | What have I done?! >:) |
| 2025-11-11 02:45:02 | <geekosaur> | you're still stuck somewhere insane |
| 2025-11-11 02:45:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-11-11 02:45:15 | <geekosaur> | there are three types: scalar, list, hash |
| 2025-11-11 02:46:11 | <geekosaur> | you would not normally use a hash as a list unless it's sparse |
| 2025-11-11 02:47:00 | <jreicher> | I thought the original sin belonged to awk? |
| 2025-11-11 02:47:07 | <geekosaur> | yes |
| 2025-11-11 02:47:19 | <jreicher> | Personally I'm a fan of that bad boy. |
| 2025-11-11 02:47:37 | <geekosaur> | awk doesn't have arrays/lists, so you use its "associative arrays" as if they were |
| 2025-11-11 02:47:39 | <monochrom> | No no no, the original sin belonged to BASIC and Lisp. Yes I'm putting them on the same line. |
| 2025-11-11 02:48:03 | <monochrom> | Lisp: Every name has two independent bindings: value and function. |
| 2025-11-11 02:48:16 | <monochrom> | BASIC: Every name has two independent bindings: number and string. |
| 2025-11-11 02:48:17 | <jreicher> | That's Lisp-2. Lisp-1 is not like that |
| 2025-11-11 02:48:50 | <monochrom> | Criminals. |
| 2025-11-11 02:49:14 | <EvanR> | every [capitalized] name has two independent bindings, type and constructor |
| 2025-11-11 02:49:32 | <geekosaur> | module name/qualifier |
| 2025-11-11 02:49:33 | <EvanR> | shoot |
| 2025-11-11 02:49:46 | <EvanR> | up to three |
| 2025-11-11 02:50:11 | <jreicher> | The thing that really broke my brain when I looked at Lisp (after doing functional) is that there isn't an implicit eval of an expression in head possition. |
| 2025-11-11 02:50:14 | <geekosaur> | and patsyns |
| 2025-11-11 02:50:18 | <jreicher> | Took me ages to unlearn that expectation |
| 2025-11-11 02:50:21 | <geekosaur> | typeclasses |
| 2025-11-11 02:56:56 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-11 03:01:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-11 03:02:09 | × | Sidney quits (~Sidney@2600:4040:2678:9600:b1c4:ced3:242d:1252) (Quit: Client closed) |
| 2025-11-11 03:02:30 | <EvanR> | also haskell has "infinite sets" (types with infinite inhabitants) so that's not a deal breaker |
| 2025-11-11 03:02:47 | <jreicher> | Are they only denumerable? |
| 2025-11-11 03:03:12 | <EvanR> | depends on your metatheory? |
| 2025-11-11 03:04:18 | <EvanR> | if you tried to form a list of all Sequence of Bool, you'd fail to list them all |
| 2025-11-11 03:05:08 | <EvanR> | diagonalization could be used to construct a missed sequence |
| 2025-11-11 03:05:32 | <EvanR> | I meant Stream of Bool |
| 2025-11-11 03:05:37 | × | Googulator92 quits (~Googulato@2a01-036d-0106-0180-8127-ba79-55a7-6f29.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-11-11 03:05:42 | → | Googulator68 joins (~Googulato@2a01-036d-0106-0180-8127-ba79-55a7-6f29.pool6.digikabel.hu) |
| 2025-11-11 03:06:19 | <jreicher> | That's why I was asking about what haskell is representing with these "infinite sets". |
| 2025-11-11 03:06:48 | <EvanR> | I saw a constructive notion of "uncountable" floating around called "sequence avoiding" set, maybe could be repurposed for types |
| 2025-11-11 03:07:41 | <jreicher> | It can be countable but still not recursive. That's the really surprising case IMO. |
| 2025-11-11 03:08:04 | <EvanR> | for all streams of A, say xs, there exists an x such that for all i, x "does not equal" xs !! i |
| 2025-11-11 03:08:30 | → | Square2 joins (~Square4@user/square) |
| 2025-11-11 03:09:55 | <EvanR> | then A is sequence avoiding |
| 2025-11-11 03:10:28 | → | bggd joins (~bgg@2a01:e0a:819:1510:c077:be4f:997f:e54a) |
| 2025-11-11 03:11:51 | × | Square3 quits (~Square@user/square) (Ping timeout: 256 seconds) |
| 2025-11-11 03:13:10 | <EvanR> | A = Stream Bool would satisfy this using diagonalization to prove the existence part, if you could somehow get the "does not equal" to make sense |
| 2025-11-11 03:31:25 | × | td_ quits (~td@i5387093B.versanet.de) (Ping timeout: 250 seconds) |
| 2025-11-11 03:33:12 | → | td_ joins (~td@i53870938.versanet.de) |
| 2025-11-11 03:36:08 | → | qqe joins (~qqq@185.54.21.203) |
| 2025-11-11 03:40:43 | → | Googulator96 joins (~Googulato@2a01-036d-0106-0180-8127-ba79-55a7-6f29.pool6.digikabel.hu) |
| 2025-11-11 03:40:44 | × | Googulator68 quits (~Googulato@2a01-036d-0106-0180-8127-ba79-55a7-6f29.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-11-11 03:45:38 | × | bionade24 quits (~quassel@server2.oscloud.info) (Quit: Apocalypse Incoming!) |
| 2025-11-11 03:45:49 | → | bionade24 joins (~quassel@server2.oscloud.info) |
| 2025-11-11 03:46:23 | → | deptype joins (~deptype@2406:b400:3a:73c2:87a5:b5f2:d68c:7c8) |
| 2025-11-11 03:54:50 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 2025-11-11 03:54:56 | × | peterbecich quits (~Thunderbi@172.222.148.214) (Ping timeout: 256 seconds) |
All times are in UTC.