Logs: liberachat/#haskell
| 2025-09-09 07:34:14 | → | merijn joins (~merijn@77.242.116.146) |
| 2025-09-09 07:46:51 | → | ZLima12_ joins (~zlima12@user/meow/ZLima12) |
| 2025-09-09 07:49:54 | × | ZLima12 quits (~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds) |
| 2025-09-09 08:00:47 | → | mari-estel joins (~mari-este@user/mari-estel) |
| 2025-09-09 08:03:12 | × | mari85725 quits (~mari-este@user/mari-estel) (Ping timeout: 256 seconds) |
| 2025-09-09 08:03:20 | × | craunts7 quits (~craunts@152.32.99.194) (Quit: The Lounge - https://thelounge.chat) |
| 2025-09-09 08:13:45 | <ggVGc> | We have a book club at work, and our main development languages are Scala and TS. The others don't have that much experience in general with strong typing and powerful type systems, and only me and one other person really knows Scala "well". I would like propose a book which tackles type system things and basic type theory, without being too hardcore for the book club. Any advice? |
| 2025-09-09 08:14:26 | <ggVGc> | Haskell based book would be fine, as long as it doesn't start with "let's discuss a monad" |
| 2025-09-09 08:15:02 | <ggVGc> | I'm thinking something like SICP but for type systems, I guess |
| 2025-09-09 08:16:04 | <sm> | maybe one of these: https://www.extrema.is/articles/haskell-books > design ? |
| 2025-09-09 08:17:39 | <merijn> | ggVGc: How hardcore do you wanna go? |
| 2025-09-09 08:19:00 | <sm> | tcard__ it's confusing having Author: Travis Cardwell on every book page, right above the book's published date, additional to the actual book authors on the left |
| 2025-09-09 08:20:08 | <merijn> | oh, wait, you wanted "not to hardcore" |
| 2025-09-09 08:20:44 | <sm> | (and/or one of these: https://www.extrema.is/articles/haskell-books > implementation) |
| 2025-09-09 08:21:33 | → | chele joins (~chele@user/chele) |
| 2025-09-09 08:25:19 | <sm> | pretty good reviews for this one: https://www.goodreads.com/book/show/112252.Types_and_Programming_Languages |
| 2025-09-09 08:28:41 | <merijn> | I was gonna say TaPL, but I would call that rather hardcore :p |
| 2025-09-09 08:40:48 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 252 seconds) |
| 2025-09-09 08:47:13 | × | Googulator51 quits (~Googulato@2a01-036d-0106-217b-fd1e-c506-2528-080c.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-09-09 08:47:20 | <[exa]> | ggVGc: /me votes for girard |
| 2025-09-09 08:47:35 | → | Googulator51 joins (~Googulato@2a01-036d-0106-217b-fd1e-c506-2528-080c.pool6.digikabel.hu) |
| 2025-09-09 08:50:35 | <ggVGc> | merijn: yeah, as not-hardcore as possible basically, while still being not-crap :) |
| 2025-09-09 08:50:39 | <ggVGc> | thanks for the suggestions! |
| 2025-09-09 08:53:28 | × | mari-estel quits (~mari-este@user/mari-estel) (Remote host closed the connection) |
| 2025-09-09 09:05:25 | <ski> | hm, there's one "Thinking with Types: Type-Level Programming Haskell" by Sandy Maguire in 2019-01-10 at <https://thinkingwithtypes.com/>,<https://leanpub.com/thinking-with-types/> |
| 2025-09-09 09:05:46 | <ski> | (i haven't read it) |
| 2025-09-09 09:07:27 | <haskellbridge> | <sm> https://www.extrema.is/articles/haskell-books/thinking-with-types - maybe that one should have the design tag tcard__ ? |
| 2025-09-09 09:09:05 | xxhine | is now known as sshine |
| 2025-09-09 09:09:24 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2025-09-09 09:11:25 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2025-09-09 09:12:16 | <ski> | ggVGc : "Polymorphic Type Inference" by Michael I. Schwartzbach in 1995-03 at <https://cs.au.dk/~amoeller/mis/typeinf.pdf> might be worth checking out (not a book, though, just a paper (intended to be more introductory/tutorial). with some exercises) |
| 2025-09-09 09:12:48 | <ski> | there's also "On Understanding Types, Data Abstraction, and Polymorphism" by Luca Cardelli,Peter Wegner in 1985-12 at <http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf>, and "On Understanding Data Abstraction, Revisited" by William R. Cook in 2009-10 at <https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf> |
| 2025-09-09 09:13:20 | <merijn> | ggVGc: Also, Scala 2 or 3? |
| 2025-09-09 09:15:29 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 2025-09-09 09:18:49 | <ggVGc> | merijn: 3, fortunately, but unfortunately the existing code uses Akka without really undrstanding/liking actors, so it's basically just used as a http router |
| 2025-09-09 09:19:08 | <ggVGc> | while other concurrency stuff is done in good ol java way, but in scala |
| 2025-09-09 09:19:17 | <ggVGc> | with locking queues etc |
| 2025-09-09 09:19:27 | <Franciman> | [exa]: i'm studying automated deduction for ontologies. which book by girard? |
| 2025-09-09 09:19:34 | <Franciman> | (two unrelated things) |
| 2025-09-09 09:20:01 | <ggVGc> | Franciman: so.... rdf? |
| 2025-09-09 09:20:12 | <Franciman> | rdf and OWL |
| 2025-09-09 09:20:27 | → | ZLima12 joins (~zlima12@user/meow/ZLima12) |
| 2025-09-09 09:20:27 | <ggVGc> | sounds a lot like my job :) |
| 2025-09-09 09:21:24 | <Franciman> | what's your job? |
| 2025-09-09 09:22:39 | × | ZLima12_ quits (~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds) |
| 2025-09-09 09:23:30 | × | tromp quits (~textual@2001:1c00:3487:1b00:298e:6063:53dd:ee4e) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-09-09 09:23:36 | <ski> | i wonder about "The Little Typer" by Daniel P. Friedman,David Thrane Christiansen in 2018 at <https://thelittletyper.com/>,<https://www.amazon.com/Little-Typer-MIT-Press/dp/0262536439>,<https://mitpress.mit.edu/9780262536431/the-little-typer/>,<https://felleisen.org/matthias/BTypist-index.html> |
| 2025-09-09 09:24:28 | <ggVGc> | Franciman: Basically building this, https://data.icos-cp.eu/portal/. I started fairly recently (dec last year), and have been on parental leave since May, and am back on 20% since last month, so have not been part of much of what's there yet. But, there's a lot of work to be done :) https://github.com/ICOS-Carbon-Portal/meta |
| 2025-09-09 09:24:50 | <ggVGc> | Franciman: my main goal right now is to replace out RDF datastore with SQL+Ontop, actually. |
| 2025-09-09 09:25:26 | <ggVGc> | because right now we have a custom index, and custom SPQRQL query rewriting, and it's a bit of a mess imo, and seems to currently also have consistency issues. |
| 2025-09-09 09:25:35 | <ski> | Franciman : perhaps "Proofs and Types" by Jean-Yves Girard (Translated and with appendices by Paul Taylor,Yves Lafont) in 1989,1990,2003 at <https://www.paultaylor.eu/stable/prot.pdf> |
| 2025-09-09 09:25:50 | <tcard__> | sm: Regarding the author confusion, thanks for the feedback. I am making a note. I implemented that Haskell books content using my articles system, but it is indeed not a great match. I hope to improve it in the future. |
| 2025-09-09 09:26:33 | <ggVGc> | ski: you bring up a good idea of suggesting to the book club that we can sometimes read shorter papers and discuss them. Will try to see if that flies |
| 2025-09-09 09:26:47 | <ggVGc> | I would almost prefer a "paper group" rather than a book club, I think |
| 2025-09-09 09:27:02 | <ggVGc> | smaller investment, covering more ground |
| 2025-09-09 09:27:03 | <ski> | ggVGc : i'd think the Schwartzbach paper, at least, would be worth looking into |
| 2025-09-09 09:27:40 | <ski> | it includes some info that most papers on type systems assumes, but does not state outright |
| 2025-09-09 09:28:13 | <merijn> | ggVGc: At least 3 has rank2 types :> |
| 2025-09-09 09:28:29 | <ggVGc> | haha, oh man, I'd heard about The little typer, but starting to talk about dependent types seems a bit too soon for this group |
| 2025-09-09 09:28:35 | <ggVGc> | I may want to read it personally though... |
| 2025-09-09 09:28:47 | <ski> | yea, i haven't seen "The Little Typer", either |
| 2025-09-09 09:28:48 | <ggVGc> | But I have 4mo old twins now, so maybe in... 10 years? |
| 2025-09-09 09:30:31 | <ski> | but that series (see <https://felleisen.org/matthias/BTLS-index.html>. also apparently <https://www.thelittlelearner.com/>) has an interesting didactive approach, with examples and exercises |
| 2025-09-09 09:30:52 | <ggVGc> | merijn: yeah, but it also has this, https://docs.scala-lang.org/scala3/reference/other-new-features/indentation.html. So, you know, win some lose some. |
| 2025-09-09 09:31:27 | <ski> | if the "Thinking with Types" is not too advanced (not sure), might be useful as well |
| 2025-09-09 09:31:47 | <ggVGc> | I know that is a controversial statement in #haskell (about significant indentation). But, I think it works very poorly in Scala. |
| 2025-09-09 09:31:50 | <ggVGc> | being added on like that |
| 2025-09-09 09:31:55 | <ski> | merijn : but not higher rank ? |
| 2025-09-09 09:32:30 | <ggVGc> | actually not a huge fan of significant whitespace in Haskell either, but it works out alright most of the time |
| 2025-09-09 09:32:41 | <ggVGc> | without the type system it would be a disaster |
| 2025-09-09 09:33:06 | <merijn> | ski: I'm not sure if it supports higher rank, I'm still in the business of migrating us from 2 to 3 :) |
| 2025-09-09 09:33:17 | <merijn> | And I've only needed/wanted rank2 so far |
| 2025-09-09 09:33:55 | <ski> | mm, looks like it introduces layout block, more generally, than just after a few keywords (as in Haskell) ? |
| 2025-09-09 09:34:01 | ski | nods |
| 2025-09-09 09:34:04 | <Franciman> | ggVGc: can I pm you? |
| 2025-09-09 09:34:05 | <ggVGc> | yeah |
| 2025-09-09 09:34:08 | <ggVGc> | Franciman: sure |
| 2025-09-09 09:34:21 | <ski> | ggVGc : hm, i'm not seeing how the types are related to layout ? |
| 2025-09-09 09:34:30 | <ggVGc> | ski: I definitely do not like it, but the person who wrote most of the code I'm currently working on does like it. |
| 2025-09-09 09:34:55 | <ski> | i guess, if you don't get the nesting structure you intend, you're more likely to get a type (or scope) error ? |
| 2025-09-09 09:35:28 | <ggVGc> | ski: yo umean about my statement regarding haskell? I mean that, with a powerful language like Haskell where you can write very terse code, if you don't also have the type system helping you out, things subtle indentation errors can become major difficulties |
| 2025-09-09 09:35:40 | <ski> | ggVGc : it kinda reminds me of the various SRFIs for indentation-based nesting syntax, for Scheme (which, afaik, none has really caught on much at all) |
| 2025-09-09 09:36:00 | <ski> | ggVGc : "without the type system it would be a disaster" specifically |
| 2025-09-09 09:36:02 | <arahael> | merijn: Hey, I am curious about the code in posix-pty, why is it not possible to get the pty's Fd? |
| 2025-09-09 09:36:15 | <arahael> | merijn: (It's not important, I'm just curious) |
| 2025-09-09 09:37:11 | <ggVGc> | ski: well, I've had situations in Haskell where I get a type error I find super odd and can't easily see why it's happening, and then I realise it's because I've messed up an application of something, sometimes because of messed up indentation |
| 2025-09-09 09:37:25 | <merijn> | arahael: because it's code I wrote in 2013 when I barely new Haskell and never gotten around to actually using it for what I wrote it :p |
| 2025-09-09 09:37:27 | <ggVGc> | and if I didn't have the type system, I'd get some strange runtime error instead |
| 2025-09-09 09:37:29 | <ggVGc> | which would be a lot worse |
| 2025-09-09 09:37:34 | <arahael> | merijn: Heh, fair enough! |
| 2025-09-09 09:37:35 | <ggVGc> | could* |
| 2025-09-09 09:37:47 | <merijn> | arahael: So there wasn't much specific thought going into it |
| 2025-09-09 09:38:06 | <arahael> | merijn: Nice, so you were probably trying to do data/implementation hiding and all that good stuff. |
| 2025-09-09 09:38:08 | <merijn> | arahael: I think it's mostly to prevent construction of Pty from random Fd |
| 2025-09-09 09:38:14 | × | trickard quits (~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-09-09 09:38:24 | <merijn> | But I didn't think to need to project the Fd |
| 2025-09-09 09:38:28 | → | trickard_ joins (~trickard@cpe-53-98-47-163.wireline.com.au) |
| 2025-09-09 09:38:38 | <arahael> | Ah, and I was trying to get the Fd from the Pty, so that I could ask it to see if there was data without blocking on it. |
| 2025-09-09 09:38:43 | <ggVGc> | ski: but, what I very much dislike about the Scala3 significant indentation is that 'foo:\n\t123' means foo(123). |
| 2025-09-09 09:38:46 | <ggVGc> | that is horrible |
All times are in UTC.