2023-06-27 00:04:47 +0200 | misterfish | (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 264 seconds) |
2023-06-27 00:05:06 +0200 | mxs | (~mxs@user/mxs) |
2023-06-27 00:07:50 +0200 | Guest9511 | (~finn@rul16-h01-176-151-21-224.dsl.sta.abo.bbox.fr) (Ping timeout: 246 seconds) |
2023-06-27 00:09:30 +0200 | hyiltiz | (~user@2620:149:13d1:100::5df) (Ping timeout: 240 seconds) |
2023-06-27 00:12:21 +0200 | wroathe | (~wroathe@user/wroathe) |
2023-06-27 00:13:19 +0200 | falafel | (~falafel@2607:fb91:86c:d890:e762:f9b2:9119:4b00) |
2023-06-27 00:15:53 +0200 | danse-nr3 | (~francesco@151.35.32.192) (Ping timeout: 246 seconds) |
2023-06-27 00:18:36 +0200 | hippoid | (~hippoid@c-98-213-162-40.hsd1.il.comcast.net) (Changing host) |
2023-06-27 00:18:36 +0200 | hippoid | (~hippoid@user/hippoid) |
2023-06-27 00:18:58 +0200 | misterfish | (~misterfis@84-53-85-146.bbserv.nl) |
2023-06-27 00:19:21 +0200 | threedognite | (~ThreeDogN@user/ThreeDogNite) |
2023-06-27 00:20:07 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
2023-06-27 00:27:12 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
2023-06-27 00:27:14 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
2023-06-27 00:28:08 +0200 | Midjak | (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
2023-06-27 00:37:14 +0200 | nick3 | (~nick@98.186.198.197) |
2023-06-27 00:38:48 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2023-06-27 00:41:48 +0200 | misterfish | (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 250 seconds) |
2023-06-27 00:47:08 +0200 | falafel | (~falafel@2607:fb91:86c:d890:e762:f9b2:9119:4b00) (Ping timeout: 240 seconds) |
2023-06-27 00:47:26 +0200 | foul_owl | (~kerry@45.143.82.40) (Ping timeout: 250 seconds) |
2023-06-27 00:49:48 +0200 | threedognite | (~ThreeDogN@user/ThreeDogNite) (Quit: Leaving) |
2023-06-27 00:51:34 +0200 | hsw_ | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
2023-06-27 00:52:30 +0200 | nick3 | (~nick@98.186.198.197) (Ping timeout: 240 seconds) |
2023-06-27 00:52:42 +0200 | JSharp | (sid4580@id-4580.lymington.irccloud.com) (Ping timeout: 255 seconds) |
2023-06-27 00:53:00 +0200 | JSharp | (sid4580@id-4580.lymington.irccloud.com) |
2023-06-27 00:53:28 +0200 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Read error: Connection reset by peer) |
2023-06-27 00:53:36 +0200 | geekosaur[m] | (~geekosaur@xmonad/geekosaur) (Ping timeout: 255 seconds) |
2023-06-27 00:53:36 +0200 | Null_A[m] | (~jasonjckn@2001:470:69fc:105::bb85) (Ping timeout: 255 seconds) |
2023-06-27 00:53:36 +0200 | bgamari[m] | (~bgamari@2001:470:69fc:105::c7b9) (Ping timeout: 255 seconds) |
2023-06-27 00:53:37 +0200 | DustinStiles[m] | (~duwstiles@2001:470:69fc:105::3:699b) (Ping timeout: 255 seconds) |
2023-06-27 00:53:37 +0200 | hellwolf[m] | (~hellwolfm@2001:470:69fc:105::3:6a4) (Ping timeout: 255 seconds) |
2023-06-27 00:53:37 +0200 | lilpotent_jlemen | (~lilpotent@2001:470:69fc:105::3:6eb6) (Ping timeout: 255 seconds) |
2023-06-27 00:53:37 +0200 | oak- | (~oak-@2001:470:69fc:105::fcd) (Ping timeout: 255 seconds) |
2023-06-27 00:53:37 +0200 | joyfulmantis[m] | (~joyfulman@2001:470:69fc:105::3:400a) (Ping timeout: 255 seconds) |
2023-06-27 00:53:37 +0200 | VarikValefor[m] | (~varikvale@2001:470:69fc:105::a5d) (Ping timeout: 255 seconds) |
2023-06-27 00:54:03 +0200 | hsiktas[m] | (~hsiktasm]@2001:470:69fc:105::30d4) (Ping timeout: 255 seconds) |
2023-06-27 00:54:04 +0200 | peddie | (~peddie@2001:470:69fc:105::25d) (Ping timeout: 255 seconds) |
2023-06-27 00:54:04 +0200 | Guillaum[m] | (~guiboumat@2001:470:69fc:105::1:72ac) (Ping timeout: 255 seconds) |
2023-06-27 00:54:04 +0200 | jean-paul[m] | (~jean-paul@2001:470:69fc:105::d1ab) (Ping timeout: 255 seconds) |
2023-06-27 00:54:04 +0200 | SeanKing[m] | (~seankingm@2001:470:69fc:105::cf9c) (Ping timeout: 255 seconds) |
2023-06-27 00:54:04 +0200 | Deide | (~deide@user/deide) (Ping timeout: 255 seconds) |
2023-06-27 00:54:04 +0200 | end^ | (~end^@user/end/x-0094621) (Ping timeout: 255 seconds) |
2023-06-27 00:54:04 +0200 | shapr[m] | (~shaprcofr@2001:470:69fc:105::2:d107) (Ping timeout: 255 seconds) |
2023-06-27 00:54:04 +0200 | earthy | (~arthurvl@2a02-a469-f5e2-1-83d2-ca43-57a2-dc81.fixed6.kpn.net) (Ping timeout: 255 seconds) |
2023-06-27 00:54:21 +0200 | earthy | (~arthurvl@2a02-a469-f5e2-1-83d2-ca43-57a2-dc81.fixed6.kpn.net) |
2023-06-27 00:54:30 +0200 | supersven[m] | (~supersven@2001:470:69fc:105::31b6) (Ping timeout: 255 seconds) |
2023-06-27 00:55:34 +0200 | foul_owl | (~kerry@71.212.137.212) |
2023-06-27 00:56:18 +0200 | hellwolf[m] | (~hellwolfm@2001:470:69fc:105::3:6a4) |
2023-06-27 00:57:24 +0200 | Null_A[m] | (~jasonjckn@2001:470:69fc:105::bb85) |
2023-06-27 00:57:45 +0200 | ddellacosta | (~ddellacos@146.70.171.100) (Quit: WeeChat 3.8) |
2023-06-27 00:57:50 +0200 | oak- | (~oak-@2001:470:69fc:105::fcd) |
2023-06-27 00:58:32 +0200 | acidjnk | (~acidjnk@p200300d6e7072f355d50cb0f60b9d9c7.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
2023-06-27 01:00:27 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
2023-06-27 01:00:48 +0200 | <segfaultfizzbuzz> | what is there other than algebraic data types? are there uh, non-algebraic data types? |
2023-06-27 01:00:57 +0200 | Deide | (~deide@user/deide) |
2023-06-27 01:01:02 +0200 | dcoutts_ | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 246 seconds) |
2023-06-27 01:01:12 +0200 | <geekosaur> | C's, for example |
2023-06-27 01:01:27 +0200 | <segfaultfizzbuzz> | C? |
2023-06-27 01:01:53 +0200 | gnalzo | (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
2023-06-27 01:02:07 +0200 | <segfaultfizzbuzz> | oh like C as in the programming language,...? |
2023-06-27 01:02:32 +0200 | <segfaultfizzbuzz> | i mean as a way of gluing together "basic types" or "atomic types" by the way |
2023-06-27 01:02:45 +0200 | <geekosaur> | "algebraic" means they're designed around an algebraic view of types. basically sums and products, but there are others as well which may not be supported by some algebraic-type languages; for example, haskell doesn't support quotient types |
2023-06-27 01:03:02 +0200 | oo_miguel | (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) (Ping timeout: 250 seconds) |
2023-06-27 01:03:09 +0200 | <segfaultfizzbuzz> | ah interesting,... is there a larger list of these types of types? |
2023-06-27 01:03:09 +0200 | Guillaum[m] | (~guiboumat@2001:470:69fc:105::1:72ac) |
2023-06-27 01:03:14 +0200 | m5zs7k_ | (aquares@web10.mydevil.net) |
2023-06-27 01:03:33 +0200 | <geekosaur> | and the notion of sums and products is based on basic algebra but elevated to types, and can be thought of as representing the number of inhabitants of a type |
2023-06-27 01:04:07 +0200 | <segfaultfizzbuzz> | right |
2023-06-27 01:04:08 +0200 | m5zs7k | (aquares@web10.mydevil.net) (Quit: m5zs7k) |
2023-06-27 01:04:24 +0200 | <geekosaur> | so Bool has value 2, Maybe a is a + 1 (Nothing), sum types you add the values together, product types you multiply them, etc. |
2023-06-27 01:04:38 +0200 | <segfaultfizzbuzz> | so there's product, sum, and quotient, and that's it? |
2023-06-27 01:04:50 +0200 | SeanKing[m] | (~seankingm@2001:470:69fc:105::cf9c) |
2023-06-27 01:05:09 +0200 | <geekosaur> | there's more. we were discussing Conor McBride's paper about derivatives of types in here earlier, for example |
2023-06-27 01:06:00 +0200 | <geekosaur> | sums and products are just the easiest ones to consider |
2023-06-27 01:06:10 +0200 | <c_wraith> | functions are exponents |
2023-06-27 01:06:35 +0200 | <segfaultfizzbuzz> | right |
2023-06-27 01:06:57 +0200 | <segfaultfizzbuzz> | wild |
2023-06-27 01:07:22 +0200 | shapr[m] | (~shaprcofr@2001:470:69fc:105::2:d107) |
2023-06-27 01:08:01 +0200 | mncheck-m | (~mncheck@193.224.205.254) |
2023-06-27 01:08:08 +0200 | <segfaultfizzbuzz> | so the derivative of a type can require its own uh, not sure what to call this-- type-type? like a derivative of an algebraic data type should probably also be algebraic (?) or can it escape algebraicity? |
2023-06-27 01:08:34 +0200 | <geekosaur> | it's only meaningful in a system of algebraic types |
2023-06-27 01:09:48 +0200 | <geekosaur> | (well, presumably someone could come up with a different context in which it has meaning, but when we talk about it we're working in a system of algebraic data types so the result will also be an algebraic data type) |
2023-06-27 01:09:56 +0200 | Muon | (~muon@2a09:bac5:bec4:1923::281:6b) (Quit: Leaving) |
2023-06-27 01:10:37 +0200 | <segfaultfizzbuzz> | ...so in haskell, if you are not doing FFI, then there are only algebraic data types? |
2023-06-27 01:10:37 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 245 seconds) |
2023-06-27 01:10:38 +0200 | mncheck | (~mncheck@193.224.205.254) (Ping timeout: 245 seconds) |
2023-06-27 01:11:23 +0200 | <geekosaur> | yes |
2023-06-27 01:11:31 +0200 | <segfaultfizzbuzz> | that is very clarifying, thanks |
2023-06-27 01:11:48 +0200 | <geekosaur> | I'd ague even with FFI you only have types which can be represented by algebraic data types |
2023-06-27 01:11:55 +0200 | <segfaultfizzbuzz> | and so the entirety of haskell types are then the fundamental types (Int32, Char, etc), algebraic data types, and then weird FFI stuff? |
2023-06-27 01:12:31 +0200 | <geekosaur> | we can't do C unions, for example, unless we can treat them as tagged unions in which case we can model them as sum types |
2023-06-27 01:12:44 +0200 | <ncf> | segfaultfizzbuzz: there's also functions! and polymorphism! |
2023-06-27 01:12:51 +0200 | m5zs7k_ | m5zs7k |
2023-06-27 01:13:00 +0200 | <segfaultfizzbuzz> | by the way you are describing this it sounds like memory layout and type are the same or somehow deeply linked? |
2023-06-27 01:13:12 +0200 | <ncf> | "algebraic data type" isn't really a meaningful concept semantically afaik |
2023-06-27 01:13:44 +0200 | <ncf> | it just refers to the syntax you can use to make product and sum types (but these are just ways of combining old types into new types) |
2023-06-27 01:14:23 +0200 | <segfaultfizzbuzz> | ncf: i can construct a "composite type" from operations linking "fundamental types" (not sure of the right jargon here), and so an algebraic data type allows you to construct a composite type from sum and product |
2023-06-27 01:14:36 +0200 | hsiktas[m] | (~hsiktasm]@2001:470:69fc:105::30d4) |
2023-06-27 01:16:26 +0200 | jargon | (~jargon@184.101.72.124) |
2023-06-27 01:17:44 +0200 | cafkafk | (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
2023-06-27 01:19:59 +0200 | end^ | (~end^@user/end/x-0094621) |
2023-06-27 01:20:32 +0200 | <ncf> | (oh and i guess they also abstract over fixed points) |
2023-06-27 01:21:35 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
2023-06-27 01:23:59 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 264 seconds) |
2023-06-27 01:25:02 +0200 | Tuplanolla | (~Tuplanoll@91.159.68.236) (Quit: Leaving.) |
2023-06-27 01:26:00 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 255 seconds) |
2023-06-27 01:33:20 +0200 | tbidne[m] | (~tbidnemat@2001:470:69fc:105::3:6d42) (Server closed connection) |
2023-06-27 01:33:32 +0200 | tbidne[m] | (~tbidnemat@2001:470:69fc:105::3:6d42) |
2023-06-27 01:35:30 +0200 | cafkafk | (~cafkafk@fsf/member/cafkafk) |
2023-06-27 01:36:33 +0200 | aaronv | (~aaronv@user/aaronv) (Server closed connection) |
2023-06-27 01:36:47 +0200 | aaronv | (~aaronv@user/aaronv) |
2023-06-27 01:37:43 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) |
2023-06-27 01:37:44 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
2023-06-27 01:37:44 +0200 | wroathe | (~wroathe@user/wroathe) |
2023-06-27 01:38:45 +0200 | Nokurn | (~jeremiah@cpe-76-86-186-227.socal.res.rr.com) |
2023-06-27 01:44:49 +0200 | <monochrom> | I like "newtype D a = MkD (D a -> a)". It may or may not count as an algebraic data type. |
2023-06-27 01:45:16 +0200 | <monochrom> | And yeah polymorphism too, "newtype I a = MkI (forall r. (a -> r) -> r)" |
2023-06-27 01:45:30 +0200 | <segfaultfizzbuzz> | hmm |
2023-06-27 01:46:22 +0200 | mauke_ | (~mauke@user/mauke) |
2023-06-27 01:48:06 +0200 | mauke | (~mauke@user/mauke) (Ping timeout: 250 seconds) |
2023-06-27 01:48:06 +0200 | mauke_ | mauke |
2023-06-27 01:53:11 +0200 | pavonia | (~user@user/siracusa) |
2023-06-27 01:56:54 +0200 | meinside | (uid24933@id-24933.helmsley.irccloud.com) |
2023-06-27 01:57:18 +0200 | Umeaboy | (~Umeaboy@94-255-145-133.cust.bredband2.com) |
2023-06-27 01:59:08 +0200 | <Umeaboy> | Hi! gprbuild is necessary to port GHC to a new distro, but one of its dependencies are xmlada-sources according to the spec file for Fedora 39, but that package does NOT exist. Is it safe to delete the need of that package or should I comment it out? |
2023-06-27 02:01:11 +0200 | mei | (~mei@user/mei) (Ping timeout: 264 seconds) |
2023-06-27 02:05:44 +0200 | <dolio> | You need some particular models for D to be an algebra. |
2023-06-27 02:06:14 +0200 | oac | (~oac@141.157.210.244) (Quit: oac) |
2023-06-27 02:06:30 +0200 | oac | (~oac@pool-141-157-210-244.nycmny.fios.verizon.net) |
2023-06-27 02:06:35 +0200 | <dolio> | Aside from a = 1, of course. |
2023-06-27 02:07:02 +0200 | oac | (~oac@pool-141-157-210-244.nycmny.fios.verizon.net) (Remote host closed the connection) |
2023-06-27 02:11:56 +0200 | kleenestar[m] | (~kleenesta@2001:470:69fc:105::3:6d78) (Server closed connection) |
2023-06-27 02:12:08 +0200 | kleenestar[m] | (~kleenesta@2001:470:69fc:105::3:6d78) |
2023-06-27 02:13:30 +0200 | gurkenglas | (~gurkengla@dynamic-046-114-164-153.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-06-27 02:14:11 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 246 seconds) |
2023-06-27 02:16:59 +0200 | waleee | (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 246 seconds) |
2023-06-27 02:18:16 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-06-27 02:18:22 +0200 | Daniel[m]1 | (~danieltan@2001:470:69fc:105::3:6e5e) (Server closed connection) |
2023-06-27 02:18:34 +0200 | Daniel[m]1 | (~danieltan@2001:470:69fc:105::3:6e5e) |
2023-06-27 02:19:38 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-06-27 02:23:55 +0200 | <EvanR> | segfaultfizzbuzz, some types could be implemented with algebraic data types but aren't because efficiency, e.g. Array |
2023-06-27 02:24:21 +0200 | <geekosaur> | Umeaboy, you should probably contact the Fedora maintainer for GHC. what you asked means ~nothing to most people here |
2023-06-27 02:24:48 +0200 | somerandomnick[m | (~somerando@2001:470:69fc:105::3:4f2e) (Server closed connection) |
2023-06-27 02:25:00 +0200 | somerandomnick[m | (~somerando@2001:470:69fc:105::3:4f2e) |
2023-06-27 02:25:20 +0200 | <segfaultfizzbuzz> | hmmm,... yeah i suppose you have to worry about equivalence here as well,... |
2023-06-27 02:25:34 +0200 | <EvanR> | there are bits and bobs like MVar and IORef which are based on runtime primitives not ADTs |
2023-06-27 02:29:16 +0200 | kupi | (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
2023-06-27 02:29:22 +0200 | <EvanR> | perhaps there are transcendental data types analogous to transcendental numbers? xD |
2023-06-27 02:30:00 +0200 | sumpwa | (~sumpwa@172.59.120.233) |
2023-06-27 02:30:54 +0200 | <segfaultfizzbuzz> | well yeah ,... and maybe there are taylor series? this language around programs is very strange and interesting |
2023-06-27 02:31:26 +0200 | <EvanR> | we already have infinite series |
2023-06-27 02:31:54 +0200 | <EvanR> | 1 + x + x*x + x*x*x + ... i.e. [x] |
2023-06-27 02:32:35 +0200 | <geekosaur> | now, what's an irrational number? |
2023-06-27 02:32:35 +0200 | <hpc> | segfaultfizzbuzz: you can define a taylor series as a recurrence relation |
2023-06-27 02:32:37 +0200 | <hpc> | EvanR |
2023-06-27 02:32:58 +0200 | <hpc> | EvanR's example becomes f(x) = 1 + x * f(x) |
2023-06-27 02:33:15 +0200 | <segfaultfizzbuzz> | "type approximation"? fourier transform of a type? how far does this stuff go? lol |
2023-06-27 02:33:30 +0200 | <hpc> | it definitely gets up to calculus |
2023-06-27 02:33:47 +0200 | <hpc> | at least, for useful results |
2023-06-27 02:33:48 +0200 | <EvanR> | value approximation is basically domain theory |
2023-06-27 02:33:53 +0200 | <segfaultfizzbuzz> | e^doom2 |
2023-06-27 02:34:16 +0200 | <EvanR> | exponential is function type |
2023-06-27 02:34:58 +0200 | <hpc> | working out that functions and exponentials are the same is a good exercise, if you want to work it out yourself |
2023-06-27 02:35:18 +0200 | <segfaultfizzbuzz> | right... okay so something related to this i had been considering was the phenomenon of irrational numbers like pi,... perhaps it is best to consider pi an equivalence class of recurrence relations? |
2023-06-27 02:38:10 +0200 | <EvanR> | Pi types, you just discovered dependent types |
2023-06-27 02:38:39 +0200 | EvanR | cargo cultist |
2023-06-27 02:39:23 +0200 | <jackdk> | You can take the partial derivative of an ADT with respect to a type variable and get a one-hole context for that type. |
2023-06-27 02:39:35 +0200 | <segfaultfizzbuzz> | what? ha ok well that's generous of you, but i guess you are saying that a dependent type is an equivalence class of recurrence relations on types or somesuch? |
2023-06-27 02:39:48 +0200 | segfaultfizzbuzz | hasn't encountered holes,... |
2023-06-27 02:41:41 +0200 | <EvanR> | no I was kidding |
2023-06-27 02:41:56 +0200 | <EvanR> | the Pi in Pi types stands for depedent product, not pi |
2023-06-27 02:42:07 +0200 | <segfaultfizzbuzz> | ok |
2023-06-27 02:42:48 +0200 | Guest79 | (~Guest79@2600:4040:5413:bb00:e851:635c:5e93:78ea) |
2023-06-27 02:43:20 +0200 | <geekosaur> | right, sigma and pi = sum and product on a higher level |
2023-06-27 02:43:41 +0200 | <segfaultfizzbuzz> | 🤯 |
2023-06-27 02:45:02 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 252 seconds) |
2023-06-27 02:45:49 +0200 | bratwurst | (~dfadsva@2604:3d09:207f:f650::3f28) |
2023-06-27 02:45:55 +0200 | Guest79 | (~Guest79@2600:4040:5413:bb00:e851:635c:5e93:78ea) (Client Quit) |
2023-06-27 02:46:04 +0200 | threedognite | (~threedogn@user/ThreeDogNite) |
2023-06-27 02:46:20 +0200 | <jackdk> | segfaultfizzbuzz: take a two-tuple of `a`, and remove one of the `a`s. You will want to know "which" `a` you removed as well as the "other" `a` you left behind. So you'll have a product type consisting of a two-valued type (tracking which `a` was removed) as well as an `a`(the other one left behind) |
2023-06-27 02:47:23 +0200 | <jackdk> | segfaultfizzbuzz: a two-tuple of `a` is `a * a` or `a ^ 2` (consider the isomorphism `Bool -> a` <=> `(a, a)`). The partial derivative of `a^2` with respect to `a` is `2 * a` |
2023-06-27 02:47:46 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2023-06-27 02:49:38 +0200 | nasrudin__ | (~nasrudin_@45.152.182.251) (Ping timeout: 250 seconds) |
2023-06-27 02:51:56 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 240 seconds) |
2023-06-27 02:52:27 +0200 | <segfaultfizzbuzz> | oh wow and so it's Integer * a, with the Integer being an index |
2023-06-27 02:53:49 +0200 | <segfaultfizzbuzz> | 🤯🤯🤯🤯🤯 lol ok what is a rational type then |
2023-06-27 02:54:26 +0200 | <segfaultfizzbuzz> | ... and then ... galois theory of types, so if you want to figure out the type you can't represent it or something |
2023-06-27 02:57:28 +0200 | bratwurst | (~dfadsva@2604:3d09:207f:f650::3f28) (Quit: Leaving) |
2023-06-27 02:58:37 +0200 | Sciencentistguy9 | (~sciencent@hacksoc/ordinary-member) |
2023-06-27 03:00:48 +0200 | Sciencentistguy | (~sciencent@hacksoc/ordinary-member) (Ping timeout: 252 seconds) |
2023-06-27 03:00:48 +0200 | Sciencentistguy9 | Sciencentistguy |
2023-06-27 03:01:51 +0200 | <jackdk> | Not quite. `2` is just standing for a two-valued type (isomorphic to `Bool`) |
2023-06-27 03:02:59 +0200 | <segfaultfizzbuzz> | but if you had a 3-tuple, you would have Int * a * a where that int would be 1..3 |
2023-06-27 03:03:46 +0200 | <jackdk> | You would have some kind of three-valued type, like `data Three = One | Two | Three`. I tend not to think of it as a restricted Int but I guess...? |
2023-06-27 03:03:49 +0200 | <ski> | not `Int', but `3', which is `1 + 1 + 1' |
2023-06-27 03:05:36 +0200 | <ski> | d (a * a * a) / d a = 1 * a * a + a * 1 * a + a * a * 1 = (1 + 1 + 1) * a * a = 3 * a * a |
2023-06-27 03:06:12 +0200 | <hpc> | if you really wanted to, you could think of '2' as mod-2 |
2023-06-27 03:06:22 +0200 | <segfaultfizzbuzz> | lol type groups? |
2023-06-27 03:06:32 +0200 | <hpc> | type Word1 = Bool |
2023-06-27 03:06:36 +0200 | <hpc> | :P |
2023-06-27 03:06:58 +0200 | <segfaultfizzbuzz> | monster type group |
2023-06-27 03:06:59 +0200 | <ski> | in terms of set theory, you can think of `3' as `{0,1,2}' |
2023-06-27 03:08:27 +0200 | <segfaultfizzbuzz> | right 3 is the cardinality of the underlying type and if i am speaking this language correctly refers to any type which is isomorphic to like integers mod 3 or something like that |
2023-06-27 03:08:29 +0200 | EvanR_ | (~EvanR@user/evanr) |
2023-06-27 03:08:34 +0200 | EvanR | (~EvanR@user/evanr) (Read error: Connection reset by peer) |
2023-06-27 03:08:55 +0200 | <ski> | yea ("up to isomorphism/bijection") |
2023-06-27 03:09:34 +0200 | <segfaultfizzbuzz> | type rings? type fields? |
2023-06-27 03:10:18 +0200 | <segfaultfizzbuzz> | the circle type... types equidistant from a point? this gets weird fast |
2023-06-27 03:10:58 +0200 | <segfaultfizzbuzz> | ok i have a good one: a limit type? |
2023-06-27 03:11:31 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
2023-06-27 03:12:36 +0200 | <ski> | segfaultfizzbuzz : see "Seven trees in one" by Andreas Blass in 1995 at <https://dept.math.lsa.umich.edu/~ablass/cat.html>,"Objects of Categories as Complex Numbers" by Marcelo Fiore,Tom Leinster in 2002-12-30 at <https://arxiv.org/abs/math/0212377>,"This Week's Finds in Mathematical Physics (Week 202)" by John Baez in 2004-02-21 at <https://math.ucr.edu/home/baez/week202.html> |
2023-06-27 03:14:15 +0200 | <segfaultfizzbuzz> | non-analytic types haha |
2023-06-27 03:16:38 +0200 | <segfaultfizzbuzz> | "The arithmetic of such objects is a challenge because there is usually no subtraction." |
2023-06-27 03:17:12 +0200 | <segfaultfizzbuzz> | ok you made my day with a paper starting off saying "Consider the following absurd argument ..." |
2023-06-27 03:17:38 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
2023-06-27 03:19:19 +0200 | <segfaultfizzbuzz> | i am not really familiar with the relationship between categories and types and i have failed several times to learn the very basics of categories ... they dont feel like a natural structure and it is hard to make my subconscious pay attention |
2023-06-27 03:20:43 +0200 | <geekosaur> | weren't you the one who wanted to be "completely abstract" a couple months back? categories are about as close to that as you get |
2023-06-27 03:21:18 +0200 | <segfaultfizzbuzz> | yeah i try to chase abstraction now and then and see where it goes |
2023-06-27 03:21:36 +0200 | <ski> | "The Two Dualities of Computation: Negative and Fractional Types" by Roshan P. James,Amr Sabry at <https://legacy.cs.indiana.edu/~sabry/papers/rational.pdf>,"Fractional Types" by Roshan P. James,Zachary Sparks,Jacques Carette,Amr Sabry at <https://www.cas.mcmaster.ca/~carette/PiFractional/frac.pdf>,<https://legacy.cs.indiana.edu/~sabry/papers/fractionals.pdf>,"Information Effects" by Roshan P. James,Amr |
2023-06-27 03:21:37 +0200 | <segfaultfizzbuzz> | and yeah i wanted a mathematician's vm |
2023-06-27 03:21:42 +0200 | <ski> | Sabry at <https://legacy.cs.indiana.edu/~sabry/papers/information-effects.pdf> |
2023-06-27 03:22:53 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
2023-06-27 03:24:10 +0200 | <segfaultfizzbuzz> | From James and Sabry: "Intuitively, alues of negative types are values that flow “backwards” to satisfy demands and values of fractional types are values that impose constraints on their context. " |
2023-06-27 03:24:45 +0200 | werneta | (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
2023-06-27 03:26:13 +0200 | nasrudin__ | (~nasrudin_@ip72-197-77-4.sd.sd.cox.net) |
2023-06-27 03:27:00 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 240 seconds) |
2023-06-27 03:27:12 +0200 | <segfaultfizzbuzz> | on a related note how does one read a paper like this |
2023-06-27 03:28:10 +0200 | <segfaultfizzbuzz> | what are you retaining, what do you have perfect recall of |
2023-06-27 03:28:47 +0200 | <segfaultfizzbuzz> | at some point i have seen so many definitions that the other ones i have previously seen fall out of my head |
2023-06-27 03:29:22 +0200 | geranim0 | (~geranim0@modemcable182.140-177-173.mc.videotron.ca) (Ping timeout: 245 seconds) |
2023-06-27 03:44:02 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
2023-06-27 03:45:25 +0200 | xff0x | (~xff0x@ai098135.d.east.v6connect.net) (Ping timeout: 240 seconds) |
2023-06-27 03:57:40 +0200 | <segfaultfizzbuzz> | deep learning/multilayer-perceptron on types/sgd on types |
2023-06-27 03:57:42 +0200 | segfaultfizzbuzz | ducks |
2023-06-27 03:59:19 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-06-27 04:01:18 +0200 | polykernel[m] | (~polykerne@user/polykernel) (Server closed connection) |
2023-06-27 04:01:32 +0200 | polykernel[m] | (~polykerne@user/polykernel) |
2023-06-27 04:01:38 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 246 seconds) |
2023-06-27 04:07:08 +0200 | <segfaultfizzbuzz> | oh wow scattering amplitudes, seriously? |
2023-06-27 04:09:24 +0200 | <segfaultfizzbuzz> | the james and sabry paper discusses an identity where the type is T = planar binary trees (see https://arxiv.org/pdf/2011.14413.pdf), showing that T = T^2 + 1 implies T = T^7 |
2023-06-27 04:16:11 +0200 | falafel | (~falafel@2607:fb91:86c:d890:6a4c:34f0:4ae7:ccb3) |
2023-06-27 04:16:34 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-06-27 04:17:37 +0200 | threedognite | (~threedogn@user/ThreeDogNite) (Quit: Quit) |
2023-06-27 04:18:53 +0200 | <EvanR_> | segfaultfizzbuzz, a category is "just" a set of objects, which could be anything, and for each pair of objects a,b a set of arrows, and an operation to compose arrows if 'b' of one matches 'a' of the other |
2023-06-27 04:19:44 +0200 | <EvanR_> | magic legos |
2023-06-27 04:19:54 +0200 | <segfaultfizzbuzz> | right, i think of it as just the study of associativity... but if you read anything past the basics it looks like some kind of awkwardly restricted graph theory |
2023-06-27 04:20:21 +0200 | <segfaultfizzbuzz> | and then it's like why not just study graphs then |
2023-06-27 04:21:57 +0200 | <EvanR_> | a graph is a kind of category |
2023-06-27 04:22:51 +0200 | <EvanR_> | rather, for any graph, there's a well-behaved recipe (a functor) to turn it into a category |
2023-06-27 04:23:53 +0200 | <segfaultfizzbuzz> | categories are strictly more general? |
2023-06-27 04:24:05 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
2023-06-27 04:24:05 +0200 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
2023-06-27 04:24:05 +0200 | finn_elija | FinnElija |
2023-06-27 04:24:25 +0200 | <EvanR_> | for any category you can forget enough information to get an underlying graph, though this might be a rather insane graph |
2023-06-27 04:25:16 +0200 | <segfaultfizzbuzz> | it feels a little like the my turing machine is better than your turing machine problem in programming,... |
2023-06-27 04:25:22 +0200 | <mauke> | are you allowed to have a graph with this many nodes? |
2023-06-27 04:25:25 +0200 | <segfaultfizzbuzz> | it feels like picking up sand with two fingers |
2023-06-27 04:25:37 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2023-06-27 04:28:17 +0200 | fweht | (uid404746@id-404746.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2023-06-27 04:28:56 +0200 | td_ | (~td@i53870921.versanet.de) (Ping timeout: 246 seconds) |
2023-06-27 04:29:04 +0200 | <EvanR_> | I may be misunderstand the turing machine analogy, but don't you have an actual hierarchy of turing machines, with universal ones at the top xD |
2023-06-27 04:29:14 +0200 | <EvanR_> | so the contest could make sense |
2023-06-27 04:30:02 +0200 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
2023-06-27 04:30:15 +0200 | teo | (~teo@user/teo) (Server closed connection) |
2023-06-27 04:30:56 +0200 | td_ | (~td@i5387090F.versanet.de) |
2023-06-27 04:31:01 +0200 | teo | (~teo@user/teo) |
2023-06-27 04:34:40 +0200 | <segfaultfizzbuzz> | uh sorry i don't know turing machine hierarchy, i meant that brainfuck and lisp are both turing complete |
2023-06-27 04:34:53 +0200 | bontaq | (~user@ool-45779b84.dyn.optonline.net) (Ping timeout: 246 seconds) |
2023-06-27 04:35:42 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
2023-06-27 04:36:27 +0200 | <EvanR_> | it's more like an interface vs implementation thing. If I write a program or develop a theory that uses a category with maybe additional features, then if you can explain how thing X satisfies that description, the program will work with it or the theory applies to it. And I don't have to know the details |
2023-06-27 04:36:52 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 252 seconds) |
2023-06-27 04:37:19 +0200 | <EvanR_> | if I work with "some graph" instead, that might work too. Or it might be too specific |
2023-06-27 04:38:49 +0200 | <segfaultfizzbuzz> | i have this difficulty with algebra more generally actually,... i feel like things like group and ring are more "artificial" or "unnatural" as compared to the number 2 or pi or something,... categories have this same feeling |
2023-06-27 04:39:59 +0200 | <EvanR_> | category is really this interface, while "the number" 2 is more of a concrete piece of data |
2023-06-27 04:42:00 +0200 | <EvanR_> | the numbers can be seen as a category, e.g. there's an object for each number and an arrow from n to m if n <= m. |
2023-06-27 04:43:09 +0200 | <monochrom> | Anthropologists found a tribe whose language has only "one, two many". To them, three is unnatural. |
2023-06-27 04:43:21 +0200 | <monochrom> | err "one, two, many". |
2023-06-27 04:45:14 +0200 | <monochrom> | People 200 years ago would find that IRC would be unnatural, "why don't you just meet at the pub in-person?" |
2023-06-27 04:45:22 +0200 | nick3 | (~nick@2600:8807:9084:7800:f8b8:b1f7:7d88:9e2d) |
2023-06-27 04:45:35 +0200 | <monochrom> | People 200 years later would find that in-person pub meetups unnatural, "why don't you just IRC?" |
2023-06-27 04:46:01 +0200 | <EvanR_> | if you think group and ring are unusually selected among the zillion possible interfaces you could dream up, maybe you'd like the subject of universal algebra xD |
2023-06-27 04:46:20 +0200 | Ross[m] | (~zhichuche@2001:470:69fc:105::3:584b) (Server closed connection) |
2023-06-27 04:46:24 +0200 | <EvanR_> | which will lead you directly to category theory |
2023-06-27 04:46:32 +0200 | Ross[m] | (~zhichuche@2001:470:69fc:105::3:584b) |
2023-06-27 04:46:33 +0200 | <monochrom> | In fact, COVID lockdowns uncovered that a lot of people (for example rural ones) find virtual online meetings unnatural. |
2023-06-27 04:47:07 +0200 | <monochrom> | The overraching moral is that "unnatural" is subjective. |
2023-06-27 04:47:58 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2023-06-27 04:48:04 +0200 | <EvanR_> | natural transformations feel attacked |
2023-06-27 04:48:23 +0200 | <monochrom> | Meanwhle, said lockdowns also uncovered that IT professionals find work-at-home natural, and now they are refusing to come back to offices for in-person meetings. |
2023-06-27 04:48:58 +0200 | <monochrom> | So right, even this year, right now, half of the people find online meetups unnatural and the other half are the opposite. |
2023-06-27 04:49:12 +0200 | <monochrom> | So, why is "natural" and "unnatural" important again? |
2023-06-27 04:49:35 +0200 | nick3 | (~nick@2600:8807:9084:7800:f8b8:b1f7:7d88:9e2d) (Ping timeout: 246 seconds) |
2023-06-27 04:49:36 +0200 | <EvanR_> | unpopular opinion, math is artificial |
2023-06-27 04:49:46 +0200 | <EvanR_> | generally |
2023-06-27 04:49:51 +0200 | <monochrom> | Given that humanity can't even agree on what it means. |
2023-06-27 04:50:07 +0200 | smalltalkman | (uid545680@id-545680.hampstead.irccloud.com) |
2023-06-27 04:50:28 +0200 | <monochrom> | Even more unpopular opinion: All of knowledge is artificial. |
2023-06-27 04:51:30 +0200 | <monochrom> | Ultimate unpopular opinion: Nature doesn't care what you feel about "natural". |
2023-06-27 04:51:42 +0200 | <EvanR_> | your mom is artificial |
2023-06-27 04:52:23 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 246 seconds) |
2023-06-27 04:53:00 +0200 | phma | (~phma@host-67-44-208-160.hnremote.net) (Read error: Connection reset by peer) |
2023-06-27 04:53:27 +0200 | phma | (phma@2001:5b0:211f:2f08:4bbe:e2d4:6776:1d19) |
2023-06-27 05:00:55 +0200 | <Nosrep> | sick burn |
2023-06-27 05:01:44 +0200 | cafkafk | (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
2023-06-27 05:04:07 +0200 | cafkafk | (~cafkafk@fsf/member/cafkafk) |
2023-06-27 05:06:32 +0200 | <segfaultfizzbuzz> | haha,... a "proof" of the "unnaturalness" of the concept of group is that the restriction to use the abstract characteristics of group in performing proofs lead one to drag the monster group into every group-related proof,... and it's hard to imagine that the monster group is anything other than a mathematical curiousity |
2023-06-27 05:06:55 +0200 | <monochrom> | Oh not that again. |
2023-06-27 05:07:04 +0200 | <segfaultfizzbuzz> | ha ok |
2023-06-27 05:07:38 +0200 | <monochrom> | Why don't you instead complain that every time someone uses the real numbers they're dragging the undecidability of the continuum hypothesis into every usage? |
2023-06-27 05:07:55 +0200 | <segfaultfizzbuzz> | i mean, i don't really believe that real numbers exist :-P |
2023-06-27 05:08:08 +0200 | <monochrom> | Or that every time someone uses natural numbers they're dragging in the existence of non-standard models. |
2023-06-27 05:08:09 +0200 | <EvanR_> | if your proof is polymorphic over groups, it can't use any particular aspect of e.g. the monster group example |
2023-06-27 05:08:25 +0200 | <monochrom> | IMO either one is more monstrous than merely monster groups. |
2023-06-27 05:08:36 +0200 | <EvanR_> | like how forall a . a -> a functions can't use aspects of the potential Int or Char argument |
2023-06-27 05:08:55 +0200 | <monochrom> | Or is it just because you have vastly underinformed opinions. |
2023-06-27 05:10:29 +0200 | <monochrom> | I am saying all this because I'm tired of this drivel. It has already been debunked last time. |
2023-06-27 05:11:21 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Quit: segfaultfizzbuzz) |
2023-06-27 05:12:59 +0200 | falafel | (~falafel@2607:fb91:86c:d890:6a4c:34f0:4ae7:ccb3) (Ping timeout: 240 seconds) |
2023-06-27 05:13:35 +0200 | <jackdk> | "why don't you just meet at the pub in-person?" <- this is a great idea, I should call up some mates. Thanks monochrom! |
2023-06-27 05:15:00 +0200 | <monochrom> | :) |
2023-06-27 05:15:34 +0200 | <monochrom> | Endian wars are the most inspiring wars. >:) |
2023-06-27 05:16:58 +0200 | ec_ | ec |
2023-06-27 05:17:38 +0200 | hyvoid | (~hyenavoid@222-0-178-69.static.gci.net) (Quit: WeeChat 3.8) |
2023-06-27 05:18:42 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 250 seconds) |
2023-06-27 05:19:06 +0200 | <monochrom> | But I know that there are people having the opposite idea because a friend teaching at a university legit got students saying they don't want to come to in-person classes because they have much better chairs, computers, screens at home, understandably much more comfy and versatile. |
2023-06-27 05:20:11 +0200 | <jackdk> | I have seen every combination of remote-friendliness vs. not between managers/staff, academics/students, techies/not, etc |
2023-06-27 05:20:46 +0200 | <EvanR_> | soon the "movie tavern" crazy which greatly reduces theater seats and replaces them with recliners and table serve will come to university |
2023-06-27 05:20:54 +0200 | <EvanR_> | table service |
2023-06-27 05:22:23 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
2023-06-27 05:24:26 +0200 | hyvoid | (~hyenavoid@222-0-178-69.static.gci.net) |
2023-06-27 05:31:03 +0200 | aforemny_ | (~aforemny@2001:9e8:6cc7:2c00:369b:8740:ed39:83be) |
2023-06-27 05:31:11 +0200 | <Axman6> | I do love the premium lounge at the cinema... more of the world should offer alternatives like that |
2023-06-27 05:32:04 +0200 | Umeaboy | (~Umeaboy@94-255-145-133.cust.bredband2.com) (Quit: Leaving) |
2023-06-27 05:32:08 +0200 | aforemny | (~aforemny@i59F516C6.versanet.de) (Ping timeout: 250 seconds) |
2023-06-27 05:46:32 +0200 | nasrudin__ | (~nasrudin_@ip72-197-77-4.sd.sd.cox.net) (Ping timeout: 252 seconds) |
2023-06-27 05:48:31 +0200 | <maerwald[m]> | The worst that covid did to us was remote culture |
2023-06-27 05:49:08 +0200 | <maerwald[m]> | Also, seamless transition to AI. Won't even notice your coworkers aren't humans anymore. |
2023-06-27 05:50:04 +0200 | danse-nr3 | (~francesco@151.37.73.145) |
2023-06-27 05:51:11 +0200 | <monochrom> | "Good riddance" >:) |
2023-06-27 05:51:50 +0200 | <maerwald[m]> | Or your teachers |
2023-06-27 05:58:34 +0200 | biberu | (~biberu@user/biberu) (Read error: Connection reset by peer) |
2023-06-27 06:01:56 +0200 | biberu | (~biberu@user/biberu) |
2023-06-27 06:06:13 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
2023-06-27 06:11:16 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
2023-06-27 06:13:11 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 264 seconds) |
2023-06-27 06:19:38 +0200 | chromoblob | (~user@37.113.180.121) |
2023-06-27 06:29:25 +0200 | <hyvoid> | pre 2020: being indoors and isolated from others is unhealthy go touch grass. 2023: Experience the world and work with apple VR, let chatgpt talk to your friends and coworkers for you, use AI to fake eye contact with your webcam |
2023-06-27 06:31:05 +0200 | falafel | (~falafel@2607:fb91:86c:d890:6f90:5b78:de45:ecfa) |
2023-06-27 06:36:32 +0200 | michalz | (~michalz@185.246.207.203) |
2023-06-27 06:44:44 +0200 | jsomedon | (uid606872@id-606872.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
2023-06-27 06:46:44 +0200 | falafel | (~falafel@2607:fb91:86c:d890:6f90:5b78:de45:ecfa) (Ping timeout: 240 seconds) |
2023-06-27 06:51:10 +0200 | mei | (~mei@user/mei) |
2023-06-27 06:54:41 +0200 | dipper | (~dipper@203.168.26.139) |
2023-06-27 06:54:51 +0200 | puke | (~puke@user/puke) (Remote host closed the connection) |
2023-06-27 06:55:45 +0200 | danse-nr3 | (~francesco@151.37.73.145) (Ping timeout: 240 seconds) |
2023-06-27 06:56:26 +0200 | witcher | (~witcher@wiredspace.de) () |
2023-06-27 07:01:55 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2023-06-27 07:11:08 +0200 | jackdk | (sid373013@cssa/jackdk) (Server closed connection) |
2023-06-27 07:11:21 +0200 | jackdk | (sid373013@cssa/jackdk) |
2023-06-27 07:11:51 +0200 | danse-nr3 | (~francesco@151.37.73.145) |
2023-06-27 07:20:19 +0200 | phma | (phma@2001:5b0:211f:2f08:4bbe:e2d4:6776:1d19) (Read error: Connection reset by peer) |
2023-06-27 07:21:03 +0200 | phma | (~phma@host-67-44-208-154.hnremote.net) |
2023-06-27 07:28:05 +0200 | acidjnk | (~acidjnk@p200300d6e7072f30f5f19602a84c17f0.dip0.t-ipconnect.de) |
2023-06-27 07:42:21 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
2023-06-27 07:42:24 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
2023-06-27 07:45:57 +0200 | titibandit | (~titibandi@user/titibandit) |
2023-06-27 07:46:00 +0200 | gurkenglas | (~gurkengla@dynamic-046-114-167-060.46.114.pool.telefonica.de) |
2023-06-27 07:47:05 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 08:04:24 +0200 | jespada | (~jespada@207.188.139.183) |
2023-06-27 08:10:20 +0200 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
2023-06-27 08:13:15 +0200 | <Axman6> | Why doesit bring me such joy when reading through the source of GHC to find comments which start like "Now the biggest nightmare---calls". |
2023-06-27 08:16:40 +0200 | trev | (~trev@user/trev) |
2023-06-27 08:22:55 +0200 | <Axman6> | GHC's source really feels like so much of it was written to communicate with othewr humans, and I, as a human, appreciate that a lot |
2023-06-27 08:23:35 +0200 | jespada_ | (~jespada@207.188.139.183) |
2023-06-27 08:24:15 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-06-27 08:25:25 +0200 | nut | (~nut@rul16-h01-176-151-21-224.dsl.sta.abo.bbox.fr) |
2023-06-27 08:26:13 +0200 | jespada | (~jespada@207.188.139.183) (Ping timeout: 258 seconds) |
2023-06-27 08:27:17 +0200 | <danse-nr3> | although it is not great to find nightmares in the code ^^; |
2023-06-27 08:27:45 +0200 | <jackdk> | It turns out that the calls were coming from within the thunk itself |
2023-06-27 08:28:08 +0200 | <Axman6> | Nah, they were coming from deep in the C |
2023-06-27 08:30:34 +0200 | fendor | (~fendor@2a02:8388:1640:be00:7aca:a77a:4a28:631a) |
2023-06-27 08:31:52 +0200 | YuutaW | (~YuutaW@2404:f4c0:f9c3:502::100:17b7) (Ping timeout: 245 seconds) |
2023-06-27 08:33:07 +0200 | werneta | (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 245 seconds) |
2023-06-27 08:34:53 +0200 | YuutaW | (~YuutaW@mail.yuuta.moe) |
2023-06-27 08:35:04 +0200 | werneta | (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
2023-06-27 08:44:21 +0200 | raym | (~ray@user/raym) (Remote host closed the connection) |
2023-06-27 08:46:06 +0200 | mauke | (~mauke@user/mauke) (Ping timeout: 255 seconds) |
2023-06-27 08:49:47 +0200 | nut | (~nut@rul16-h01-176-151-21-224.dsl.sta.abo.bbox.fr) (Ping timeout: 245 seconds) |
2023-06-27 08:51:52 +0200 | titibandit | (~titibandi@user/titibandit) (Ping timeout: 240 seconds) |
2023-06-27 08:58:50 +0200 | titibandit | (~titibandi@user/titibandit) |
2023-06-27 08:59:58 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:608e:6048:fd86:cbd7) |
2023-06-27 09:01:55 +0200 | srk | (~sorki@user/srk) (Remote host closed the connection) |
2023-06-27 09:02:14 +0200 | srk | (~sorki@user/srk) |
2023-06-27 09:02:18 +0200 | michalz | (~michalz@185.246.207.203) (Ping timeout: 250 seconds) |
2023-06-27 09:02:59 +0200 | michalz | (~michalz@185.246.207.221) |
2023-06-27 09:03:51 +0200 | dipper | (~dipper@203.168.26.139) (Ping timeout: 260 seconds) |
2023-06-27 09:06:56 +0200 | PotatoGim_ | (sid99505@id-99505.lymington.irccloud.com) (Server closed connection) |
2023-06-27 09:07:32 +0200 | PotatoGim_ | (sid99505@id-99505.lymington.irccloud.com) |
2023-06-27 09:15:09 +0200 | accord | (uid568320@id-568320.hampstead.irccloud.com) |
2023-06-27 09:15:59 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-06-27 09:20:52 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
2023-06-27 09:28:32 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 245 seconds) |
2023-06-27 09:30:26 +0200 | misterfish | (~misterfis@87.215.131.102) |
2023-06-27 09:39:03 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
2023-06-27 09:41:29 +0200 | oo_miguel | (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) |
2023-06-27 09:42:56 +0200 | hisa386 | (~hisa38@104-181-102-238.lightspeed.wepbfl.sbcglobal.net) |
2023-06-27 09:44:20 +0200 | danse-nr3 | (~francesco@151.37.73.145) (Ping timeout: 250 seconds) |
2023-06-27 09:44:30 +0200 | hisa38 | (~hisa38@104-181-102-238.lightspeed.wepbfl.sbcglobal.net) (Ping timeout: 240 seconds) |
2023-06-27 09:44:30 +0200 | hisa386 | hisa38 |
2023-06-27 09:46:02 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-06-27 09:46:09 +0200 | danse-nr3 | (~francesco@151.37.73.145) |
2023-06-27 09:47:28 +0200 | nschoe | (~q@141.101.51.197) |
2023-06-27 09:48:24 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-06-27 09:51:08 +0200 | danse-nr3_ | (~francesco@151.43.55.109) |
2023-06-27 09:52:52 +0200 | califax | (~califax@user/califx) (Quit: ZNC 1.8.2 - https://znc.in) |
2023-06-27 09:53:14 +0200 | califax | (~califax@user/califx) |
2023-06-27 09:54:01 +0200 | danse-nr3 | (~francesco@151.37.73.145) (Ping timeout: 260 seconds) |
2023-06-27 09:54:35 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
2023-06-27 09:59:47 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-06-27 10:00:19 +0200 | chele | (~chele@user/chele) |
2023-06-27 10:03:27 +0200 | titibandit | (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
2023-06-27 10:05:26 +0200 | dcoutts_ | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
2023-06-27 10:08:45 +0200 | titibandit | (~titibandi@user/titibandit) |
2023-06-27 10:09:08 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 10:11:36 +0200 | <dminuoso> | Couldn't match type: Servant.Server.Internal.ServerT (Servant.API.Generic.GToServant (GHC.Generics.Rep (OdinAPI AsApi))) Hander with: Servant.API.Generic.GToServant (GHC.Generics.Rep (OdinAPI AsServer)) |
2023-06-27 10:11:48 +0200 | <dminuoso> | The cause? Missing Generic instance on OdinAPI. |
2023-06-27 10:12:11 +0200 | <dminuoso> | Im subtly baffled here. How can a missing instance lead to this "couldnt match type"? |
2023-06-27 10:12:21 +0200 | <dminuoso> | Not necessarily in this particular example, but in general |
2023-06-27 10:12:39 +0200 | Tuplanolla | (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
2023-06-27 10:13:05 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
2023-06-27 10:13:27 +0200 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
2023-06-27 10:15:39 +0200 | nschoe | (~q@141.101.51.197) (Quit: Switching off) |
2023-06-27 10:18:06 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2023-06-27 10:18:09 +0200 | puke | (~puke@user/puke) |
2023-06-27 10:18:31 +0200 | puke | (~puke@user/puke) (Max SendQ exceeded) |
2023-06-27 10:19:50 +0200 | puke | (~puke@user/puke) |
2023-06-27 10:20:32 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
2023-06-27 10:21:04 +0200 | puke | (~puke@user/puke) (Client Quit) |
2023-06-27 10:21:23 +0200 | puke | (~puke@user/puke) |
2023-06-27 10:22:08 +0200 | puke | (~puke@user/puke) (Remote host closed the connection) |
2023-06-27 10:23:08 +0200 | danse-nr3_ | (~francesco@151.43.55.109) (Ping timeout: 258 seconds) |
2023-06-27 10:23:31 +0200 | puke | (~puke@user/puke) |
2023-06-27 10:23:59 +0200 | sumpwa- | (~sumpwa@2607:fb90:d9a5:44d7:be5f:f4ff:fe2c:d91f) |
2023-06-27 10:24:06 +0200 | sumpwa | (~sumpwa@172.59.120.233) (Ping timeout: 252 seconds) |
2023-06-27 10:24:22 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
2023-06-27 10:26:20 +0200 | APic | (apic@apic.name) |
2023-06-27 10:27:16 +0200 | <eugenrh> | Just found an interesting (for me) pronunciation of 'Haskell' used by Graham Hutton in his video courses: https://www.youtube.com/playlist?list=PLF1Z-APd9zK7usPMx3LGMZEHrECUGodd3 |
2023-06-27 10:27:32 +0200 | wizardng | (uid599328@id-599328.hampstead.irccloud.com) |
2023-06-27 10:27:56 +0200 | <eugenrh> | it sounds /rythms like 'Pascal' |
2023-06-27 10:30:12 +0200 | <eugenrh> | I always thought that 'Haskell' should rythms with something like 'pickle' |
2023-06-27 10:31:02 +0200 | kuribas | (~user@ptr-17d51en9xtkf09xoa6h.18120a2.ip6.access.telenet.be) |
2023-06-27 10:31:44 +0200 | bastelfreak | (bastelfrea@libera/staff/VoxPupuli.bastelfreak) (Quit: WeeChat 3.8) |
2023-06-27 10:33:18 +0200 | chromoblob | (~user@37.113.180.121) (Ping timeout: 250 seconds) |
2023-06-27 10:33:20 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
2023-06-27 10:34:31 +0200 | <eugenrh> | It's /ˈhæskəl/ -- from wikipedia. |
2023-06-27 10:34:32 +0200 | <dminuoso> | He's Scottish. |
2023-06-27 10:35:15 +0200 | <dminuoso> | Perhaps that influences his pronunciation? |
2023-06-27 10:35:53 +0200 | <lortabac> | I have never heard "Pascal" pronounced that way |
2023-06-27 10:36:04 +0200 | <eugenrh> | nice. but that make me check on how it supposed to be. |
2023-06-27 10:36:29 +0200 | <lortabac> | I thought Pascal had a stress on the second syllable |
2023-06-27 10:36:41 +0200 | gnalzo | (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
2023-06-27 10:36:45 +0200 | <dminuoso> | lortabac: It's the French pronunciation. |
2023-06-27 10:37:18 +0200 | <dminuoso> | Or rather, in French pronunciation its /pas.kal/' |
2023-06-27 10:37:51 +0200 | <dminuoso> | Judging from wiktionary, its suggested that in the UK you stress the first syllable, but in the US and French you would stress the second. |
2023-06-27 10:38:03 +0200 | <lortabac> | oh ok |
2023-06-27 10:39:13 +0200 | <dminuoso> | Plus in case of Graham Hutton, he's a Scot living in Nottingham |
2023-06-27 10:39:21 +0200 | <jade[m]> | in french the pronunciation is always on the last syllable if I remember correctly |
2023-06-27 10:39:23 +0200 | <jade[m]> | https://youtu.be/dUnGvH8fUUc |
2023-06-27 10:39:45 +0200 | dcoutts_ | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 240 seconds) |
2023-06-27 10:39:57 +0200 | <geekosaur> | and in both cases they're pronouncing Hebrew words transliterated via Greek 😛 |
2023-06-27 10:40:18 +0200 | <lortabac> | haha |
2023-06-27 10:42:12 +0200 | bastelfreak | (bastelfrea@libera/staff/VoxPupuli.bastelfreak) |
2023-06-27 10:43:00 +0200 | <lortabac> | anyway, I'm not a native English speaker but as far as I can hear the pronunciation of unstressed syllable is somehow "fluid" in English |
2023-06-27 10:43:20 +0200 | <geekosaur> | schwas do that |
2023-06-27 10:43:36 +0200 | <lortabac> | sometimes they become schwas, sometimes they become more like "i"s |
2023-06-27 10:43:55 +0200 | <lortabac> | sometimes the full vowel is pronounced |
2023-06-27 10:44:48 +0200 | <ncf> | jade[m]: there's not really a concept of stress in french |
2023-06-27 10:45:00 +0200 | dcoutts_ | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
2023-06-27 10:45:00 +0200 | <lortabac> | Graham Hutton says something like /ˈhæskel/ |
2023-06-27 10:45:21 +0200 | <lortabac> | the second vowel does not become a schwa |
2023-06-27 10:45:53 +0200 | <jade[m]> | ncf: yeah exactly |
2023-06-27 10:47:21 +0200 | <dminuoso> | Sometimes people also pronounce things the way they do it because they like it. MySQL is formally pronounced /ˌmaɪˌɛsˌkjuːˈɛl/ - but some people pronounce it /ˌmaɪˈsiˌkwɛl/ or some such mostly because they enjoy it. |
2023-06-27 10:47:22 +0200 | <ncf> | so it's not really accurate either to say that the last sentence is always stressed |
2023-06-27 10:47:34 +0200 | chromoblob | (~user@37.113.180.121) |
2023-06-27 10:47:42 +0200 | <ncf> | it might sound that way to english speakers but... it's not universal, and we don't think of it this way at all |
2023-06-27 10:47:45 +0200 | <dminuoso> | This is sometimes influenced by who you know. If you interact with people that adopt a particular pronunciation, it sometimes rubs off. |
2023-06-27 10:48:36 +0200 | fnurglewitz | (uid263868@id-263868.lymington.irccloud.com) |
2023-06-27 10:48:54 +0200 | <eugenrh> | but maybe a professor should use the formal pronunciation. |
2023-06-27 10:49:14 +0200 | <geekosaur> | I've been pronouncing "{SQL" as "sequel" for a couple decades. I blame IBM ("SEQUEL II") |
2023-06-27 10:49:30 +0200 | <dminuoso> | eugenrh: "formal" is a difficult notion, as most languages are not properly standardized. |
2023-06-27 10:49:57 +0200 | <Rembane> | Nobody has ever gotten fired for blaming IBM. I'm in that pronounciation camp too, unless I speak swedish then it's Ess Ku Ell |
2023-06-27 10:50:36 +0200 | <eugenrh> | dminuoso: formal as used by the founders of Haskell, I guess. |
2023-06-27 10:50:36 +0200 | titibandit | (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
2023-06-27 10:50:52 +0200 | <dminuoso> | eugenrh: "founders of Haskell" - they are not the inventors of the name Haskell though. |
2023-06-27 10:51:03 +0200 | <geekosaur> | (for those not up on RDBMS history, SEQUEL II is the proprietary language that was formalized as SQL) |
2023-06-27 10:51:15 +0200 | <dminuoso> | eugenrh: But you have a point. |
2023-06-27 10:51:41 +0200 | <dminuoso> | The original authors of Haskell are the authority on how they perceive the name of the language they created should be pronounced. |
2023-06-27 10:51:52 +0200 | <Rembane> | How did Curry Haskell pronounce his last name? |
2023-06-27 10:51:52 +0200 | <geekosaur> | it's a bit late to ask Haskell Curry how to pronounce his name… |
2023-06-27 10:52:05 +0200 | <ncf> | you mean Haskell Curry wasn't conceived in vitro at the FP lab in Nottingham? disappointing |
2023-06-27 10:52:16 +0200 | <dminuoso> | Rembane: Haskell Curry pronounced his last name Curry the same way you would order a curry in an indian restaurant./ |
2023-06-27 10:52:23 +0200 | <lortabac> | this implies that the original authors would be able to agree on a pronunciation, which is not so sure :D |
2023-06-27 10:52:37 +0200 | <merijn> | Considering the Haskell Committee asked Haskell Curry's widow for permission to use the name, I would assume they know the "right" pronounciation |
2023-06-27 10:52:42 +0200 | <eugenrh> | Haskell Brooks Curry (/ˈhæskəl/; September 12, 1900 – September 1, 1982) --wikipedia |
2023-06-27 10:53:49 +0200 | <dminuoso> | We're just lucky the Language wasn't named Schönfinkel, otherwise you'd hear clear mispronounciations by mostly everybody. |
2023-06-27 10:54:01 +0200 | danse-nr3_ | (~francesco@151.43.55.109) |
2023-06-27 10:54:08 +0200 | <lortabac> | if I drive 100 km from the city where I was born, people pronounce my name differently, but it's still my name |
2023-06-27 10:54:22 +0200 | <lortabac> | these things are never black and white |
2023-06-27 10:54:31 +0200 | <dminuoso> | Black holes are pretty black! |
2023-06-27 10:54:35 +0200 | <lortabac> | :) |
2023-06-27 10:55:19 +0200 | <geekosaur> | actually they look pretty white from all the radiation outside the event horizon 😛 |
2023-06-27 10:55:32 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 10:55:53 +0200 | <Rembane> | dminuoso: Good stuff. |
2023-06-27 10:56:18 +0200 | titibandit | (~titibandi@user/titibandit) |
2023-06-27 10:58:05 +0200 | shriekingnoise | (~shrieking@186.137.175.87) (Ping timeout: 240 seconds) |
2023-06-27 10:58:30 +0200 | <dminuoso> | geekosaur: Mmm so thats an interesting definition problem. Asking about the color of a black hole requires some mutual agreement on what a black hole is. Is it just the event horizon? The event horizon plus a bit so hawking radiation would be included? Or maybe we consider the accretion disk as part of the black hole? |
2023-06-27 10:59:13 +0200 | <dminuoso> | Clearly the worlds newspapers published papers of "the blackhole" some years ago, despite it being pictures of the mass surrounding the blackhole. But maybe we consider that matter as "part of that stellar object" too. |
2023-06-27 10:59:44 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 250 seconds) |
2023-06-27 11:01:24 +0200 | titiband1t | (~titibandi@user/titibandit) |
2023-06-27 11:05:53 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
2023-06-27 11:09:16 +0200 | <merijn> | dminuoso: So earth is part of the sun? ;) |
2023-06-27 11:12:35 +0200 | Nokurn | (~jeremiah@cpe-76-86-186-227.socal.res.rr.com) (Ping timeout: 264 seconds) |
2023-06-27 11:13:56 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
2023-06-27 11:14:02 +0200 | <geekosaur> | eventually… |
2023-06-27 11:14:21 +0200 | <geekosaur> | right now the sun's blowing out, not accreting in |
2023-06-27 11:15:44 +0200 | <geekosaur> | oh, hm, matrix is receiving but not sending for some reason |
2023-06-27 11:15:47 +0200 | <dminuoso> | I mean there is further interesting debate about what we consider things like color or appearance. For instance, most people would agree that strawberries are red. But is air red or blue? If I stare at the sky, it looks pretty blue to me. |
2023-06-27 11:16:13 +0200 | <dminuoso> | Things reflect or emit light in particular ways due to physical interactions |
2023-06-27 11:16:42 +0200 | <dminuoso> | (And the sky looks orange to red during sunset) |
2023-06-27 11:17:25 +0200 | <geekosaur> | (a) Hawking radiation from any black hole we can spot is pretty minimal (b) we spot them by the radiation from the accretion disk and from jets from the poles, so from a practical angle that's "part of" the black hole |
2023-06-27 11:17:32 +0200 | <Axman6> | ZuriHac videos are up: https://youtube.com/playlist?list=PLOvRW_utVPVmzDGGOJ2amgVBK168Vemke |
2023-06-27 11:18:30 +0200 | <dminuoso> | geekosaur: Sure. At the end its just us humans that try to classify things in ways that make sense to most people. Nature itself doesnt appear to have any inherent classification system. |
2023-06-27 11:18:32 +0200 | michals | (~user@cfeld-pcx40162.desy.de) |
2023-06-27 11:18:36 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 260 seconds) |
2023-06-27 11:18:40 +0200 | <dminuoso> | That is, black holes dont have some "object type" tag attached to them |
2023-06-27 11:18:49 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 11:19:15 +0200 | <dminuoso> | If including the accretion disk to the definition of a black hole is useful to most people.. |
2023-06-27 11:19:50 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
2023-06-27 11:19:59 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
2023-06-27 11:20:00 +0200 | puke | (~puke@user/puke) (Quit: puke) |
2023-06-27 11:20:36 +0200 | oljenkins | (~philipp@p5dec4bb3.dip0.t-ipconnect.de) (Quit: leaving) |
2023-06-27 11:20:51 +0200 | <dminuoso> | Or well, the above is not entirely correct. Particle physics is certainly involved with objects that appear to be very definable with very discrete properties. |
2023-06-27 11:21:11 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-06-27 11:21:20 +0200 | Lord_of_Life_ | Lord_of_Life |
2023-06-27 11:21:44 +0200 | puke | (~puke@user/puke) |
2023-06-27 11:22:06 +0200 | puke | (~puke@user/puke) (Max SendQ exceeded) |
2023-06-27 11:23:04 +0200 | puke | (~puke@user/puke) |
2023-06-27 11:23:16 +0200 | <geekosaur> | don't get me started. https://www.dropbox.com/s/pacf2bd39s7xgra/planets.txt?dl=0 |
2023-06-27 11:23:51 +0200 | <geekosaur> | (after a delay arguing woth dropbox over plans…) |
2023-06-27 11:24:07 +0200 | puke | (~puke@user/puke) (Max SendQ exceeded) |
2023-06-27 11:25:02 +0200 | puke | (~puke@user/puke) |
2023-06-27 11:25:17 +0200 | ft | (~ft@p508db151.dip0.t-ipconnect.de) (Quit: leaving) |
2023-06-27 11:28:28 +0200 | delyan_ | (sid523379@id-523379.hampstead.irccloud.com) (Server closed connection) |
2023-06-27 11:28:45 +0200 | delyan_ | (sid523379@id-523379.hampstead.irccloud.com) |
2023-06-27 11:31:45 +0200 | <geekosaur> | "with very discrete properties" — until it's not (neutrinos, for example) |
2023-06-27 11:36:16 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
2023-06-27 11:44:48 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 250 seconds) |
2023-06-27 11:56:46 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-06-27 11:58:52 +0200 | ubert | (~Thunderbi@2a02:8109:abc0:6434:b4a0:e511:3874:b91) |
2023-06-27 12:09:32 +0200 | <eugenrh> | re: ZuriHac videos - I see a Category Theory Track there. Nice! I'll sure check it out! |
2023-06-27 12:11:02 +0200 | catch22 | (~catch22@2406:3400:418:d7e0:67c:16ff:fe3e:b769) (Quit: Leaving) |
2023-06-27 12:13:07 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 245 seconds) |
2023-06-27 12:14:46 +0200 | jargon | (~jargon@184.101.72.124) (Remote host closed the connection) |
2023-06-27 12:15:20 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
2023-06-27 12:19:50 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 260 seconds) |
2023-06-27 12:21:06 +0200 | <dminuoso> | geekosaur: What do you mean by neutrinos? |
2023-06-27 12:21:45 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
2023-06-27 12:21:47 +0200 | <geekosaur> | electron, muon, and tau neutrinos used to be considered distinct. they're not; neutrinos oscillate between them |
2023-06-27 12:22:47 +0200 | nut | (~nut@176-151-21-224.abo.bbox.fr) |
2023-06-27 12:23:33 +0200 | <geekosaur> | and then there's the whole double slit experiment brouhaha |
2023-06-27 12:23:42 +0200 | <geekosaur> | which gets weirder the more they look into it |
2023-06-27 12:24:36 +0200 | <jade[m]> | quantum mechanics is either really fun or really painful to understand |
2023-06-27 12:24:46 +0200 | <jade[m]> | the ultimate superposition |
2023-06-27 12:24:57 +0200 | <geekosaur> | "or"? |
2023-06-27 12:25:05 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
2023-06-27 12:25:12 +0200 | <jade[m]> | should be and, yeah |
2023-06-27 12:25:25 +0200 | <jade[m]> | until you try it out, which will collapse the superposition |
2023-06-27 12:25:33 +0200 | <jade[m]> | it will probably be painful |
2023-06-27 12:28:43 +0200 | mc47 | (~mc47@xmonad/TheMC47) |
2023-06-27 12:31:00 +0200 | __monty__ | (~toonn@user/toonn) |
2023-06-27 12:36:45 +0200 | wizardng | (uid599328@id-599328.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
2023-06-27 12:42:08 +0200 | cafkafk | (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
2023-06-27 12:44:02 +0200 | <chromoblob> | > lines "" |
2023-06-27 12:44:03 +0200 | <lambdabot> | [] |
2023-06-27 12:44:06 +0200 | <chromoblob> | > lines "x" |
2023-06-27 12:44:08 +0200 | <lambdabot> | ["x"] |
2023-06-27 12:44:13 +0200 | <chromoblob> | > lines "x\n" |
2023-06-27 12:44:15 +0200 | <lambdabot> | ["x"] |
2023-06-27 12:44:18 +0200 | geranim0 | (~geranim0@modemcable182.140-177-173.mc.videotron.ca) |
2023-06-27 12:44:19 +0200 | <chromoblob> | yuck |
2023-06-27 12:44:57 +0200 | titiband1t | (~titibandi@user/titibandit) (Remote host closed the connection) |
2023-06-27 12:45:17 +0200 | <chromoblob> | i want a lines where lines "" = [""] and lines "x\n" = ["x", ""] |
2023-06-27 12:45:40 +0200 | <chromoblob> | > lines "x\n\n" |
2023-06-27 12:45:41 +0200 | <lambdabot> | ["x",""] |
2023-06-27 12:45:44 +0200 | mmhat | (~mmh@p200300f1c722e4efee086bfffe095315.dip0.t-ipconnect.de) |
2023-06-27 12:45:48 +0200 | <ncf> | [zurihac] i like how by "beyond haskell" SPJ means "metaverse" and Conal Elliott means "dependent types" |
2023-06-27 12:45:54 +0200 | <ncf> | choose your fighter |
2023-06-27 12:46:01 +0200 | <geekosaur> | > splitOn "\n" "x\n" |
2023-06-27 12:46:02 +0200 | <lambdabot> | ["x",""] |
2023-06-27 12:46:16 +0200 | <chromoblob> | > splitOn undefined "" |
2023-06-27 12:46:18 +0200 | <lambdabot> | [""] |
2023-06-27 12:46:21 +0200 | cafkafk | (~cafkafk@fsf/member/cafkafk) |
2023-06-27 12:46:22 +0200 | <chromoblob> | ah thank you.. |
2023-06-27 12:46:37 +0200 | mmhat | (~mmh@p200300f1c722e4efee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
2023-06-27 12:46:39 +0200 | <geekosaur> | (Data.List.Split in the split package) |
2023-06-27 12:46:51 +0200 | <chromoblob> | oh i thought it was in base |
2023-06-27 12:47:37 +0200 | <geekosaur> | and lines behaves as it does because technically lines are ended by \n, not separated by it |
2023-06-27 12:48:21 +0200 | <chromoblob> | yeah, but what about files/strings that don't end in \n |
2023-06-27 12:48:45 +0200 | <geekosaur> | technically illegal but lines gives it to you as the remainder |
2023-06-27 12:49:00 +0200 | <geekosaur> | rather than losing data by discarding it |
2023-06-27 12:50:06 +0200 | <chromoblob> | "illegal" by which authority? |
2023-06-27 12:54:16 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 12:55:52 +0200 | PotatoGim_ | (sid99505@id-99505.lymington.irccloud.com) (Quit: Updating details, brb) |
2023-06-27 12:56:13 +0200 | PotatoGim | (sid99505@id-99505.lymington.irccloud.com) |
2023-06-27 12:56:27 +0200 | <ncf> | POSIX |
2023-06-27 12:58:18 +0200 | TheCatCollective | (NyaaTheKit@user/calculuscat) (Quit: Meow Meow Meow Meow Meow Meow Meow Meow) |
2023-06-27 12:58:21 +0200 | <ncf> | https://pubs.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap03.html defines "line" as a sequence of characters terminated by a newline character; a "text file" as a sequence of zero or more lines; and an "incomplete line" as a sequence of one or more non-newline characters at the end of a file |
2023-06-27 12:59:27 +0200 | TheCatCollective | (NyaaTheKit@user/calculuscat) |
2023-06-27 13:01:47 +0200 | nut | (~nut@176-151-21-224.abo.bbox.fr) (Ping timeout: 264 seconds) |
2023-06-27 13:02:21 +0200 | priesvitne_sklo | (~priesvitn@192.216.99.34.bc.googleusercontent.com) |
2023-06-27 13:03:17 +0200 | <dminuoso> | geekosaur: Sure neutrino oscillation is a thing, but not in conflict with the standard model. |
2023-06-27 13:04:02 +0200 | <dminuoso> | While its debatable which configuration of atoms constitutes a "house", there's certainly no debate what constitutes an electron neutrino. |
2023-06-27 13:06:53 +0200 | <chromoblob> | ncf: i wonder why have that |
2023-06-27 13:07:16 +0200 | xff0x | (~xff0x@ai098135.d.east.v6connect.net) |
2023-06-27 13:09:58 +0200 | <dminuoso> | chromoblob: Because it makes sense to have a standardized format for these things. |
2023-06-27 13:10:12 +0200 | <geekosaur> | because (a) ed and sed among others work that way (b) it makes exchange of data between record-based systems (think IBM minis and mainframes) easier, which mattered a lot in the early days |
2023-06-27 13:10:35 +0200 | <Lears> | It also helps distinguish complete from incomplete output. |
2023-06-27 13:13:12 +0200 | <dminuoso> | Part of the underlying issue is that ASCII is originally a terminal control protocol, which historically has been reused. Originally \n isnt as much a "line separator", as it is rather a terminal command to move the cursor. |
2023-06-27 13:13:44 +0200 | <dminuoso> | POSIX gives at least some specification how these terminal control codes are used for text encoding. |
2023-06-27 13:14:37 +0200 | yahb2 | (~yahb2@2a01:4f8:c0c:5c7b::2) (Server closed connection) |
2023-06-27 13:14:48 +0200 | accord | (uid568320@id-568320.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
2023-06-27 13:14:48 +0200 | <hpc> | specifically iirc, \n is "move the cursor down" and \r is "move the cursor all the way left" |
2023-06-27 13:14:54 +0200 | <hpc> | which is how windows newlines got to be a thing |
2023-06-27 13:14:58 +0200 | <dminuoso> | Indeed. |
2023-06-27 13:14:59 +0200 | yahb2 | (~yahb2@2a01:4f8:c0c:5c7b::2) |
2023-06-27 13:16:26 +0200 | <ncf> | maybe another reason for newline-terminated lines instead of -separated is so that `cat` behaves as you'd expect without having to insert newlines between files |
2023-06-27 13:16:40 +0200 | <ncf> | i don't know the specific hysterical raisins |
2023-06-27 13:17:09 +0200 | <dminuoso> | ncf: Its the same reason, but yeah. |
2023-06-27 13:17:32 +0200 | <dminuoso> | This type of coupling is very convenient, especially in an era where space and processing power was extremely limited. |
2023-06-27 13:17:40 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-06-27 13:18:42 +0200 | <dminuoso> | The zoo of all combinations is still observable if you check `man stty` |
2023-06-27 13:19:04 +0200 | <dminuoso> | Which has various conversion flags like -icrnl, -inlcr -ocrnl -onlcr -onlret |
2023-06-27 13:21:39 +0200 | <hpc> | oh, as another added bonus - terminals were special hardware didn't all have the same interface |
2023-06-27 13:22:06 +0200 | <hpc> | which explains the word "terminal emulator" (a piece of software that implements the interface of a terminal) |
2023-06-27 13:22:11 +0200 | <dminuoso> | hpc: ASCII codepoints were particulary chosen according to the electrical layout of terminals. |
2023-06-27 13:22:18 +0200 | <hpc> | and some of the more random options you might find in putty or whatever - https://en.wikipedia.org/wiki/VT100 |
2023-06-27 13:22:23 +0200 | <dminuoso> | Or in tandem with them. |
2023-06-27 13:22:42 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
2023-06-27 13:23:02 +0200 | <hpc> | yeah, there was a lot of electrical convenience going on in the early days of standardization |
2023-06-27 13:23:09 +0200 | <hpc> | you can see a bit of it in ethernet too |
2023-06-27 13:23:26 +0200 | <geekosaur> | some terminals. every line of terminals had its own weirdshit |
2023-06-27 13:23:37 +0200 | <dminuoso> | So the shift key would for example directly set the 6th bit |
2023-06-27 13:24:12 +0200 | <dminuoso> | The binary encoding of 'a' is 1000001, and for 'A' its 1100001 |
2023-06-27 13:24:13 +0200 | <geekosaur> | like ANSI standardized the DEC VTxxx line (as distinct from VT52, or various non-DEC terminals) |
2023-06-27 13:24:16 +0200 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) (Server closed connection) |
2023-06-27 13:24:26 +0200 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) |
2023-06-27 13:25:18 +0200 | <dminuoso> | And similarly control just cut off the wires for bits 6 and 7 |
2023-06-27 13:25:29 +0200 | <dminuoso> | Which explains the common key combinations that are still emulated today |
2023-06-27 13:26:01 +0200 | <hpc> | oh wow, i never really put that together |
2023-06-27 13:26:14 +0200 | <dminuoso> | So `\a' is named this way |
2023-06-27 13:26:38 +0200 | sap | (~sap@169.84-49-96.nextgentel.com) |
2023-06-27 13:26:39 +0200 | <hpc> | i knew ^A, ^B, ... were a sequence, but in retrospect it's obvious it was done electrically |
2023-06-27 13:26:47 +0200 | <dminuoso> | Ah yes. |
2023-06-27 13:27:13 +0200 | <dminuoso> | hpc: Some of these combinations are *still* in place |
2023-06-27 13:27:33 +0200 | sap | (~sap@169.84-49-96.nextgentel.com) (Client Quit) |
2023-06-27 13:28:23 +0200 | <hpc> | quite a few of them are, just scrolling through an ascii table |
2023-06-27 13:29:25 +0200 | <dminuoso> | Ctrl+J will move the line down. Observe 'j' -> 1101010 and '\n' -> 0001010 |
2023-06-27 13:29:30 +0200 | <dminuoso> | Works in most terminal emulators |
2023-06-27 13:30:39 +0200 | <dminuoso> | Funny story, a long while ago I was debugging something on a server where a program produces some garbage binary data and dumped it into a log file. I connected via `ssh` and ran just `tail` on the log file. Then my machine froze up, and a few seconds later a stack of thousands of print dialogs appeared. |
2023-06-27 13:31:00 +0200 | <dminuoso> | That was the day when I learned my terminal emulator had support for escape sequences that would open the system print dialog. |
2023-06-27 13:31:25 +0200 | <hpc> | i once set my motd to resize my putty terminal the way i like it |
2023-06-27 13:31:27 +0200 | <dminuoso> | The server produces the binary output of that exact sequence in very rapid succession. |
2023-06-27 13:31:44 +0200 | <hpc> | there's also codes for moving windows around, even though that wasn't a concept at all way back when |
2023-06-27 13:32:04 +0200 | bontaq | (~user@ool-45779b84.dyn.optonline.net) |
2023-06-27 13:32:12 +0200 | <hpc> | er, bashrc |
2023-06-27 13:32:16 +0200 | <hpc> | i don't know why i said motd :D |
2023-06-27 13:40:58 +0200 | <dminuoso> | https://gist.github.com/dminuoso/df2ed99722fffd3cf367767f28e04e9a |
2023-06-27 13:41:04 +0200 | <dminuoso> | Why does GHC demand the constructor of `IO`? |
2023-06-27 13:41:49 +0200 | <dminuoso> | To coerce between `newtype Handler a = Handler { runHandler' :: ExceptT ServerError IO a }` and `IO (Either ServerError a)`, why would GHC even care about the constructor of IO? |
2023-06-27 13:42:07 +0200 | <merijn> | dminuoso: You using coerce? |
2023-06-27 13:42:28 +0200 | <dminuoso> | Yes. |
2023-06-27 13:42:54 +0200 | <merijn> | dminuoso: coerce can only operate on newtypes who'se constructo is in scope. Maybe it's inferring the wrong type for coerce? |
2023-06-27 13:43:15 +0200 | <geekosaur> | the error message shows it trying to coerce AppM to IO |
2023-06-27 13:43:16 +0200 | <int-e> | It seems to say that without considering the type |
2023-06-27 13:44:01 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-06-27 13:44:09 +0200 | <dminuoso> | geekosaur: Mmm, pretty sure not. The inferred type of coerce is ‘IO (Either ServerError a) -> Handler a’ |
2023-06-27 13:44:23 +0200 | <int-e> | it's not wrong... the only way to coerce a to IO b would be to coerce a to the wrapped thing. You don't need the type of the wrapped thing to see that. |
2023-06-27 13:45:23 +0200 | <dminuoso> | Bringing the IO constructor into scope is not helpful, because then it produces https://gist.github.com/dminuoso/c9ce4e6c2af81b77e9b7f6536c87e6ce |
2023-06-27 13:45:32 +0200 | <dminuoso> | Ah hold on. |
2023-06-27 13:46:20 +0200 | <dminuoso> | Okay GHC diagnostics have gone wild. |
2023-06-27 13:46:25 +0200 | <int-e> | But you can see that it used the knowledge of the constructor's type to find types that don't match. |
2023-06-27 13:46:28 +0200 | <dminuoso> | It was really just missing the data constructor of ExceptT. |
2023-06-27 13:46:30 +0200 | <dminuoso> | But asked for IO instead. |
2023-06-27 13:46:38 +0200 | <dminuoso> | Im smelling a subtle GHC bug in the diagnostic generation here |
2023-06-27 13:46:48 +0200 | <int-e> | "it's not wrong" -- it's still a pretty awful error message |
2023-06-27 13:47:14 +0200 | <dminuoso> | int-e: The wild thing is, if I naively do what GHC asks of me, it |
2023-06-27 13:47:17 +0200 | <dminuoso> | makes progress |
2023-06-27 13:47:24 +0200 | <dminuoso> | both in the sense what it really needs, and in the wrong way |
2023-06-27 13:47:25 +0200 | <int-e> | But there is a perspective from which it makessense. Just think like a type checker. |
2023-06-27 13:47:29 +0200 | <dminuoso> | https://gist.github.com/dminuoso/c9ce4e6c2af81b77e9b7f6536c87e6ce |
2023-06-27 13:47:56 +0200 | <int-e> | you already posted that |
2023-06-27 13:48:10 +0200 | <dminuoso> | Oh sorry |
2023-06-27 13:48:27 +0200 | raym | (~ray@user/raym) |
2023-06-27 13:49:04 +0200 | <dminuoso> | int-e: I lack the mind model to understand how it tries to look for the IO constructor. |
2023-06-27 13:50:12 +0200 | <dminuoso> | I suppose what GHC tries is to deconstruct the layering of newtypes as much as it can, and then check for whether their representation matches? |
2023-06-27 13:50:20 +0200 | <dminuoso> | And if it cant, it will just bark on one side randomly? |
2023-06-27 13:50:30 +0200 | <int-e> | my mental model (supported by the errors) is that it looks for IO's constructor *before* it can turn `IO a` into `State# RealWorld -> (# State# RealWorld, a #)` while checking coercibility. |
2023-06-27 13:51:14 +0200 | danse-nr3__ | (~francesco@151.35.69.156) |
2023-06-27 13:52:03 +0200 | <dminuoso> | It would be better if it said something along the lines of "You're missing the data constructor of IO, or of Handler and ExceptT` |
2023-06-27 13:52:05 +0200 | danse-nr3_ | (~francesco@151.43.55.109) (Read error: Connection reset by peer) |
2023-06-27 13:52:28 +0200 | <dminuoso> | But I guess this goes into the general problem that GHC generally does a poor job at error slicing |
2023-06-27 13:52:32 +0200 | <int-e> | But apparently, without seeing the constructor, it also can't refute the idea that `IO (Either ServerError a)` might actually be `Handler a` under the hood, so to speak. |
2023-06-27 13:52:40 +0200 | <dminuoso> | Right I see. |
2023-06-27 13:53:37 +0200 | <int-e> | If you stick to lines 2-4 of https://gist.github.com/dminuoso/df2ed99722fffd3cf367767f28e04e9a and ignore the rest you actually have a pretty decent error message. |
2023-06-27 13:53:45 +0200 | <dminuoso> | So when I provide it with IO, its then at the bottom of newtypes, and without the constructor of Handler it cant say whether `State# RealWorld -> (# State# RealWorld, Either ServerError a #)` is the same as `Handler a` |
2023-06-27 13:53:58 +0200 | <dminuoso> | Which is as detailed as it can possibly get |
2023-06-27 13:54:23 +0200 | <int-e> | yeah |
2023-06-27 13:58:16 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 250 seconds) |
2023-06-27 13:59:46 +0200 | <dminuoso> | I suppose part of the issue is that Coercible constraints are generated on the fly, rather than preexisting. |
2023-06-27 14:01:01 +0200 | <dminuoso> | If by merely writing `newtype Foo a = Foo (IO a)` it automatically generated approriate `instance Coercible ...`, then it wouldnt have to do this representation checking |
2023-06-27 14:01:03 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
2023-06-27 14:01:11 +0200 | <dminuoso> | Since the instance would be in scope |
2023-06-27 14:02:16 +0200 | theonlytails | (~theonlyta@2a06:c701:4c92:6100:5a1:eccb:cb8d:8b34) |
2023-06-27 14:03:11 +0200 | Guest11 | (~Guest0@2a06:c701:4c92:6100:5a1:eccb:cb8d:8b34) |
2023-06-27 14:03:21 +0200 | Guest11 | (~Guest0@2a06:c701:4c92:6100:5a1:eccb:cb8d:8b34) (Client Quit) |
2023-06-27 14:03:26 +0200 | theonlytails | (~theonlyta@2a06:c701:4c92:6100:5a1:eccb:cb8d:8b34) (Client Quit) |
2023-06-27 14:04:49 +0200 | waleee | (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
2023-06-27 14:06:05 +0200 | maxfan8_ | (~max@2a01:4f8:192:5356::2) (Server closed connection) |
2023-06-27 14:06:29 +0200 | maxfan8_ | (~max@2a01:4f8:192:5356::2) |
2023-06-27 14:07:56 +0200 | CiaoSen | (~Jura@2a05:5800:2c6:6900:664b:f0ff:fe37:9ef) |
2023-06-27 14:10:10 +0200 | jargon | (~jargon@184.101.72.124) |
2023-06-27 14:11:43 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 14:16:00 +0200 | ceoltb^ | (~ceoltb@24.125.210.85) (Remote host closed the connection) |
2023-06-27 14:16:49 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
2023-06-27 14:18:35 +0200 | acidjnk | (~acidjnk@p200300d6e7072f30f5f19602a84c17f0.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
2023-06-27 14:21:11 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 258 seconds) |
2023-06-27 14:22:42 +0200 | dsrt^ | (~dsrt@24.125.210.85) (Remote host closed the connection) |
2023-06-27 14:23:13 +0200 | fweht | (uid404746@id-404746.lymington.irccloud.com) |
2023-06-27 14:29:00 +0200 | Buggys- | (Buggys@shelltalk.net) (Ping timeout: 240 seconds) |
2023-06-27 14:29:46 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
2023-06-27 14:35:06 +0200 | Guest82 | (~Guest82@138.248.202.42) |
2023-06-27 14:40:49 +0200 | titibandit | (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
2023-06-27 14:45:26 +0200 | infinity0 | (~infinity0@pwned.gg) (Remote host closed the connection) |
2023-06-27 14:46:51 +0200 | titibandit | (~titibandi@user/titibandit) |
2023-06-27 14:47:34 +0200 | infinity0 | (~infinity0@pwned.gg) |
2023-06-27 14:47:42 +0200 | mc47 | (~mc47@xmonad/TheMC47) (Ping timeout: 245 seconds) |
2023-06-27 14:52:47 +0200 | danse-nr3__ | (~francesco@151.35.69.156) (Ping timeout: 264 seconds) |
2023-06-27 14:54:32 +0200 | nut | (~nut@176-151-21-224.abo.bbox.fr) |
2023-06-27 14:54:44 +0200 | ddellacosta | (~ddellacos@146.70.171.100) |
2023-06-27 14:59:26 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-06-27 15:10:41 +0200 | mechap | (~mechap@user/mechap) (Quit: WeeChat 3.8) |
2023-06-27 15:11:24 +0200 | <carbolymer> | https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/libraries/version-historyis this the best place to check ghc vs base version matching? seems a little bit outdated |
2023-06-27 15:13:19 +0200 | ripspin | (~chatzilla@1.145.158.48) |
2023-06-27 15:13:32 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
2023-06-27 15:22:46 +0200 | <ddellacosta> | carbolymer: I usually check the docs here https://downloads.haskell.org/~ghc/9.6.2/docs/libraries/index.html https://downloads.haskell.org/~ghc/9.6.2/docs/users_guide/9.6.1-notes.html#included-libraries |
2023-06-27 15:22:59 +0200 | <ddellacosta> | obviously change whatever version to match |
2023-06-27 15:23:32 +0200 | michals | (~user@cfeld-pcx40162.desy.de) (Quit: ERC (IRC client for Emacs 26.3)) |
2023-06-27 15:25:21 +0200 | tessier | (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (Server closed connection) |
2023-06-27 15:25:44 +0200 | tessier | (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) |
2023-06-27 15:27:57 +0200 | <carbolymer> | ddellacosta: thanks, seems to be the best option |
2023-06-27 15:28:52 +0200 | titibandit | (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
2023-06-27 15:31:15 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) |
2023-06-27 15:31:15 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
2023-06-27 15:31:15 +0200 | wroathe | (~wroathe@user/wroathe) |
2023-06-27 15:31:43 +0200 | grfn | aspen |
2023-06-27 15:31:57 +0200 | aspen | aspn |
2023-06-27 15:32:15 +0200 | aspn | (sid449115@id-449115.helmsley.irccloud.com) (Quit: Updating details, brb) |
2023-06-27 15:32:27 +0200 | aspn | (sid449115@id-449115.helmsley.irccloud.com) |
2023-06-27 15:34:24 +0200 | titibandit | (~titibandi@user/titibandit) |
2023-06-27 15:35:07 +0200 | ystael | (~ystael@user/ystael) |
2023-06-27 15:35:14 +0200 | acidjnk | (~acidjnk@p200300d6e7072f30f5f19602a84c17f0.dip0.t-ipconnect.de) |
2023-06-27 15:35:48 +0200 | <ddellacosta> | carbolymer: sure thing |
2023-06-27 15:36:10 +0200 | ystael | (~ystael@user/ystael) (Client Quit) |
2023-06-27 15:37:29 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-06-27 15:39:35 +0200 | extor | (~extor@ns3018124.ip-149-202-82.eu) |
2023-06-27 15:41:48 +0200 | Midjak | (~Midjak@82.66.147.146) |
2023-06-27 15:46:55 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 15:48:23 +0200 | fnurglewitz | (uid263868@id-263868.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2023-06-27 15:48:32 +0200 | ystael | (~ystael@user/ystael) |
2023-06-27 15:48:57 +0200 | hisa387 | (~hisa38@104-181-102-238.lightspeed.wepbfl.sbcglobal.net) |
2023-06-27 15:51:01 +0200 | hisa38 | (~hisa38@104-181-102-238.lightspeed.wepbfl.sbcglobal.net) (Ping timeout: 260 seconds) |
2023-06-27 15:51:01 +0200 | hisa387 | hisa38 |
2023-06-27 15:53:52 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
2023-06-27 15:54:06 +0200 | Guest82 | (~Guest82@138.248.202.42) (Quit: Client closed) |
2023-06-27 16:03:28 +0200 | mechap | (~mechap@user/mechap) |
2023-06-27 16:04:30 +0200 | enoq | (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) |
2023-06-27 16:04:48 +0200 | aspn | aspen |
2023-06-27 16:06:44 +0200 | enoq | (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) () |
2023-06-27 16:09:34 +0200 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 250 seconds) |
2023-06-27 16:11:07 +0200 | reach | (~reach@74.12.129.40) |
2023-06-27 16:11:32 +0200 | swistak | (~swistak@185.21.216.141) (Server closed connection) |
2023-06-27 16:11:43 +0200 | swistak | (~swistak@185.21.216.141) |
2023-06-27 16:17:29 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat) |
2023-06-27 16:25:46 +0200 | nut | (~nut@176-151-21-224.abo.bbox.fr) (Ping timeout: 258 seconds) |
2023-06-27 16:25:46 +0200 | Lears | (~Leary]@user/Leary/x-0910699) (Remote host closed the connection) |
2023-06-27 16:25:54 +0200 | Buggys | (Buggys@Buggy.shelltalk.net) |
2023-06-27 16:25:56 +0200 | reach | (~reach@74.12.129.40) (Ping timeout: 240 seconds) |
2023-06-27 16:26:02 +0200 | [Leary] | (~Leary]@user/Leary/x-0910699) |
2023-06-27 16:27:43 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:608e:6048:fd86:cbd7) (Quit: WeeChat 2.8) |
2023-06-27 16:29:22 +0200 | waleee | (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 245 seconds) |
2023-06-27 16:34:03 +0200 | dminuoso | (~dminuoso@user/dminuoso) (Server closed connection) |
2023-06-27 16:34:54 +0200 | dminuoso | (~dminuoso@user/dminuoso) |
2023-06-27 16:36:19 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 16:38:14 +0200 | nick3 | (~nick@2600:8807:9084:7800:f8b8:b1f7:7d88:9e2d) |
2023-06-27 16:42:44 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 16:43:03 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 16:44:03 +0200 | gnalzo | (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
2023-06-27 16:47:31 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) |
2023-06-27 16:47:39 +0200 | segfaultfizzbuzz | (~segfaultf@12.172.217.142) (Client Quit) |
2023-06-27 16:49:36 +0200 | zmt01 | (~zmt00@user/zmt00) |
2023-06-27 16:51:00 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
2023-06-27 16:52:41 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Ping timeout: 246 seconds) |
2023-06-27 16:52:42 +0200 | swamp_ | (~zmt00@user/zmt00) (Ping timeout: 245 seconds) |
2023-06-27 16:53:34 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 16:58:53 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
2023-06-27 16:59:13 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 17:01:25 +0200 | shriekingnoise | (~shrieking@186.137.175.87) |
2023-06-27 17:02:59 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Ping timeout: 264 seconds) |
2023-06-27 17:03:53 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 17:06:26 +0200 | [Leary] | (~Leary]@user/Leary/x-0910699) (Remote host closed the connection) |
2023-06-27 17:06:42 +0200 | [Leary] | (~Leary]@user/Leary/x-0910699) |
2023-06-27 17:07:56 +0200 | <tomsmeding> | carbolymer: ghcup list -t ghc |
2023-06-27 17:10:14 +0200 | <carbolymer> | tomsmeding: awesome, thx |
2023-06-27 17:11:09 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 17:11:31 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 17:13:18 +0200 | priesvitne_sklo | (~priesvitn@192.216.99.34.bc.googleusercontent.com) (Ping timeout: 258 seconds) |
2023-06-27 17:17:36 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 17:18:06 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 17:19:21 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-06-27 17:22:28 +0200 | mauke | (~mauke@user/mauke) |
2023-06-27 17:23:57 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
2023-06-27 17:28:47 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
2023-06-27 17:37:42 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Ping timeout: 245 seconds) |
2023-06-27 17:39:01 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 17:43:46 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
2023-06-27 17:50:26 +0200 | nick3 | (~nick@2600:8807:9084:7800:f8b8:b1f7:7d88:9e2d) (Ping timeout: 246 seconds) |
2023-06-27 17:50:30 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
2023-06-27 17:51:21 +0200 | Sgeo | (~Sgeo@user/sgeo) |
2023-06-27 17:52:30 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
2023-06-27 17:53:40 +0200 | werneta | (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Remote host closed the connection) |
2023-06-27 17:54:32 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 17:54:54 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 17:56:14 +0200 | CiaoSen | (~Jura@2a05:5800:2c6:6900:664b:f0ff:fe37:9ef) (Ping timeout: 258 seconds) |
2023-06-27 17:56:25 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2023-06-27 17:58:06 +0200 | [Leary] | (~Leary]@user/Leary/x-0910699) (Remote host closed the connection) |
2023-06-27 17:58:27 +0200 | mc47 | (~mc47@xmonad/TheMC47) |
2023-06-27 17:58:39 +0200 | [Leary] | (~Leary]@user/Leary/x-0910699) |
2023-06-27 18:00:27 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 258 seconds) |
2023-06-27 18:01:58 +0200 | mechap | (~mechap@user/mechap) (Quit: WeeChat 4.0.0) |
2023-06-27 18:02:54 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 18:03:15 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 18:07:47 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Remote host closed the connection) |
2023-06-27 18:12:34 +0200 | nick3 | (~nick@98.186.194.182) |
2023-06-27 18:12:59 +0200 | gurkenglas | (~gurkengla@dynamic-046-114-167-060.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-06-27 18:16:47 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
2023-06-27 18:17:07 +0200 | bilegeek | (~bilegeek@2600:1008:b09c:efb7:b7bf:5045:f083:53f7) |
2023-06-27 18:17:11 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 18:17:32 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 18:18:15 +0200 | kuribas | (~user@ptr-17d51en9xtkf09xoa6h.18120a2.ip6.access.telenet.be) (Read error: Connection reset by peer) |
2023-06-27 18:19:01 +0200 | nut | (~nut@176-151-21-224.abo.bbox.fr) |
2023-06-27 18:19:24 +0200 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
2023-06-27 18:20:14 +0200 | img | (~img@user/img) |
2023-06-27 18:21:35 +0200 | nick3 | (~nick@98.186.194.182) (Ping timeout: 264 seconds) |
2023-06-27 18:22:29 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
2023-06-27 18:23:17 +0200 | ripspin | (~chatzilla@1.145.158.48) (Remote host closed the connection) |
2023-06-27 18:23:55 +0200 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
2023-06-27 18:24:38 +0200 | nick3 | (~nick@98.186.194.182) |
2023-06-27 18:25:44 +0200 | cafkafk | (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
2023-06-27 18:28:30 +0200 | cafkafk | (~cafkafk@fsf/member/cafkafk) |
2023-06-27 18:28:35 +0200 | gensyst | (~gensyst@user/gensyst) |
2023-06-27 18:30:00 +0200 | nick3 | (~nick@98.186.194.182) (Ping timeout: 246 seconds) |
2023-06-27 18:30:00 +0200 | <gensyst> | While running my program with +RTS -hc (memory profiling), top shows me steadily increasing % memory use. I was already at 10% when I terminated the program. For my 64GB RAM, that should be 3.2GB RAM in use. |
2023-06-27 18:30:31 +0200 | <gensyst> | However the GHC profiling info (PS file) shows a steady graph. There are multiple saws that go to 1 GB max before collapsing again. |
2023-06-27 18:30:39 +0200 | <gensyst> | why? |
2023-06-27 18:31:08 +0200 | <gensyst> | i.e. top shows steadily increasing RAM, but the GHC profiling image shows saws that come and go, the max steady at 1 GB or so |
2023-06-27 18:32:16 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 18:32:37 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 18:34:19 +0200 | thegeekinside | (~thegeekin@189.217.90.138) (Remote host closed the connection) |
2023-06-27 18:34:32 +0200 | thegeekinside | (~thegeekin@189.217.90.138) |
2023-06-27 18:34:51 +0200 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
2023-06-27 18:35:33 +0200 | fendor | (~fendor@2a02:8388:1640:be00:7aca:a77a:4a28:631a) (Remote host closed the connection) |
2023-06-27 18:36:33 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
2023-06-27 18:40:20 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2023-06-27 18:44:22 +0200 | dcoutts_ | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 245 seconds) |
2023-06-27 18:44:32 +0200 | nick__ | (~nick@2600:8807:9084:7800:700f:eda2:f145:7a7) |
2023-06-27 18:46:34 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 18:46:55 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 18:48:20 +0200 | titibandit | (~titibandi@user/titibandit) (Ping timeout: 240 seconds) |
2023-06-27 18:48:29 +0200 | <ghostbuster> | anyone heard anything about this book? (also disregard the url, lol) https://www.amazon.ca/MOXIC-Abstract-Rectangular-Children-Anti-Slip/dp/3030769070/ |
2023-06-27 18:49:47 +0200 | jespada_ | (~jespada@207.188.139.183) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2023-06-27 18:51:02 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
2023-06-27 18:52:37 +0200 | __monty__ | (~toonn@user/toonn) |
2023-06-27 18:53:33 +0200 | gurkenglas | (~gurkengla@dynamic-046-114-167-060.46.114.pool.telefonica.de) |
2023-06-27 18:58:48 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 18:59:07 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 19:05:12 +0200 | ubert | (~Thunderbi@2a02:8109:abc0:6434:b4a0:e511:3874:b91) (Quit: ubert) |
2023-06-27 19:12:24 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 19:12:45 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 19:13:41 +0200 | thegeekinside | (~thegeekin@189.217.90.138) (Remote host closed the connection) |
2023-06-27 19:17:33 +0200 | EvanR | (~EvanR@user/evanr) |
2023-06-27 19:18:18 +0200 | EvanR_ | (~EvanR@user/evanr) (Read error: Connection reset by peer) |
2023-06-27 19:20:19 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2023-06-27 19:22:49 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 19:23:10 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 19:24:56 +0200 | <sm> | that url is strange |
2023-06-27 19:28:17 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Remote host closed the connection) |
2023-06-27 19:31:44 +0200 | <jade[m]> | lmao |
2023-06-27 19:32:06 +0200 | <Hecate> | what jade[m] said |
2023-06-27 19:32:29 +0200 | <jade[m]> | I feel honored somehow |
2023-06-27 19:33:16 +0200 | <jade[m]> | I'm having trouble with state monad again |
2023-06-27 19:33:23 +0200 | <jade[m]> | still haven't fully wrapped my head around it |
2023-06-27 19:37:49 +0200 | <nick__> | I used a name with capital letters using the record syntax of a data constructor. I got a parse error on input for that name/value pair (presumably because it was capitalized). Where can I find out more rules about what is valid in Haskell. This should be easy to find, but I just can't find an exhaustive list. |
2023-06-27 19:38:22 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 19:38:38 +0200 | dcoutts_ | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
2023-06-27 19:38:42 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 19:39:09 +0200 | <jade[m]> | the report should have that listed along with the BNF |
2023-06-27 19:39:18 +0200 | <mauke> | nick__: https://www.haskell.org/onlinereport/haskell2010/haskellch2.html#x7-180002.4 ? |
2023-06-27 19:39:22 +0200 | <jade[m]> | it might be a little annoying to navigate though |
2023-06-27 19:41:18 +0200 | <mauke> | https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-680004.2 |
2023-06-27 19:44:11 +0200 | <sm> | and for a cheat sheet, https://jutge.org/doc/haskell-cheat-sheet.pdf looks nice |
2023-06-27 19:44:18 +0200 | <sm> | or an intro, https://andrew.gibiansky.com/blog/haskell/haskell-syntax/ |
2023-06-27 19:50:39 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 19:50:58 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 19:51:20 +0200 | dcoutts_ | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 252 seconds) |
2023-06-27 19:51:31 +0200 | thegeekinside | (~thegeekin@189.217.90.138) |
2023-06-27 19:59:44 +0200 | <nick__> | thanks for all the resources. This was what I was looking for thank you. |
2023-06-27 20:01:20 +0200 | dcoutts_ | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
2023-06-27 20:02:57 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 20:03:20 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 20:03:50 +0200 | waleee | (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
2023-06-27 20:07:32 +0200 | dcoutts_ | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 240 seconds) |
2023-06-27 20:10:57 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
2023-06-27 20:11:06 +0200 | gensyst | (~gensyst@user/gensyst) (Quit: Leaving) |
2023-06-27 20:14:50 +0200 | hpc | (~juzz@ip98-169-35-163.dc.dc.cox.net) (Ping timeout: 250 seconds) |
2023-06-27 20:16:15 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 20:16:35 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 20:16:41 +0200 | hpc | (~juzz@ip98-169-35-163.dc.dc.cox.net) |
2023-06-27 20:17:55 +0200 | jade[m] | uploaded an image: (10KiB) < https://libera.ems.host/_matrix/media/v3/download/the-apothecary.club/RhhyFnBBjaNdIBUQwuIKzjHl/ima… > |
2023-06-27 20:17:56 +0200 | <jade[m]> | I seem to have done it |
2023-06-27 20:18:50 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
2023-06-27 20:22:15 +0200 | hpc | (~juzz@ip98-169-35-163.dc.dc.cox.net) (Ping timeout: 260 seconds) |
2023-06-27 20:23:56 +0200 | hpc | (~juzz@ip98-169-35-163.dc.dc.cox.net) |
2023-06-27 20:29:40 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 20:30:01 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 20:30:43 +0200 | <EvanR> | jade[m], the state monad strings together 'actions' of the form s -> (a,s) which compute something with the option to look at an initial state and report an updated state |
2023-06-27 20:31:31 +0200 | <jade[m]> | yeah I get the gist of it - my main issues are around the transformer, lifting stuff into the state monad and some of the functions which are confusing to me |
2023-06-27 20:31:33 +0200 | <jade[m]> | but thank you |
2023-06-27 20:31:47 +0200 | <EvanR> | oh yeah, mtl |
2023-06-27 20:31:55 +0200 | <EvanR> | is another level up |
2023-06-27 20:32:34 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
2023-06-27 20:33:06 +0200 | <mauke> | StateT m s a ~ s -> m (a,s) |
2023-06-27 20:34:32 +0200 | <jade[m]> | yeah, I usually get the larger picture, but the details are tricky sometimes haha |
2023-06-27 20:35:00 +0200 | bontaq | (~user@ool-45779b84.dyn.optonline.net) (Remote host closed the connection) |
2023-06-27 20:35:01 +0200 | <mauke> | lift m ~ \s -> fmap (,s) m |
2023-06-27 20:35:24 +0200 | <EvanR> | @unmtl StateT m s a |
2023-06-27 20:35:24 +0200 | <lambdabot> | m -> s (a, m) |
2023-06-27 20:35:36 +0200 | <EvanR> | oh no |
2023-06-27 20:36:04 +0200 | <geekosaur> | @unmtl StateT s m a |
2023-06-27 20:36:04 +0200 | <lambdabot> | s -> m (a, s) |
2023-06-27 20:36:11 +0200 | <jade[m]> | mauke: this is helpful, thanks a lot |
2023-06-27 20:36:14 +0200 | <EvanR> | it can't be unseen |
2023-06-27 20:36:40 +0200 | <mauke> | oh, wrong parameter order :-) |
2023-06-27 20:36:53 +0200 | <geekosaur> | you have been alpha-equivalenced 😛 |
2023-06-27 20:36:53 +0200 | <EvanR> | m -> m (m, m) |
2023-06-27 20:37:30 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 20:37:33 +0200 | <mauke> | @unmtl StateT StateT StateT StateT |
2023-06-27 20:37:33 +0200 | <lambdabot> | err: `StateT' is not applied to enough arguments, giving `/\A B C. A -> B (C, A)' |
2023-06-27 20:38:53 +0200 | <EvanR> | /\A B C . A -> B (C, A) -- settling the issue explicitly |
2023-06-27 20:43:42 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 20:44:04 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 20:44:57 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Remote host closed the connection) |
2023-06-27 20:47:51 +0200 | EvanR_ | (~EvanR@user/evanr) |
2023-06-27 20:48:05 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
2023-06-27 20:48:30 +0200 | EvanR | (~EvanR@user/evanr) (Ping timeout: 240 seconds) |
2023-06-27 20:52:35 +0200 | <jade[m]> | does one deal with `StateT s IO ()` often as something that simply transforms a state and accumuates side effects on the way? |
2023-06-27 20:52:36 +0200 | <jade[m]> | `StateT s m ()` seems kind of redundant because `s -> m ((), s)` for all intents and purposes is just `s -> m s` which is chained `>>=` calls, right? |
2023-06-27 20:53:58 +0200 | <jade[m]> | so it's just a slightly easier way to have repeated bind |
2023-06-27 20:54:01 +0200 | <jade[m]> | s |
2023-06-27 20:54:23 +0200 | <EvanR_> | result type () basically means the point is side effects (rather, intended effects) |
2023-06-27 20:54:43 +0200 | <jade[m]> | yep |
2023-06-27 20:56:24 +0200 | <EvanR_> | using a "useless" type there is useful since the action still fits in with the monad library machinery like replicateM |
2023-06-27 20:56:43 +0200 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
2023-06-27 20:56:44 +0200 | <EvanR_> | even if s -> m s could work |
2023-06-27 20:57:38 +0200 | <EvanR_> | like zero ohm resistors exist so the assembler robot doesn't have to know how to handle non-resistors (or something) |
2023-06-27 20:58:38 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
2023-06-27 21:00:31 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 21:00:53 +0200 | <ncf> | jade[m]: in the same way that State s () is redundant "because it's just composite chains of s -> s": the value is in not having to handle the input/output bookkeeping explicitly |
2023-06-27 21:00:53 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 21:01:14 +0200 | <jade[m]> | yep exactly |
2023-06-27 21:01:20 +0200 | <jade[m]> | yeah this is cool, thanks |
2023-06-27 21:01:33 +0200 | <jade[m]> | god I fucking love haskell |
2023-06-27 21:01:45 +0200 | <EvanR_> | composite chain of s -> s would be fairly easy though, if that's actually what you had xD |
2023-06-27 21:02:09 +0200 | <EvanR_> | foldr (.) id |
2023-06-27 21:02:30 +0200 | gehmehgeh | (~user@user/gehmehgeh) (Quit: Leaving) |
2023-06-27 21:02:34 +0200 | <jade[m]> | it might still be useful or interestinf to have stuff like modify |
2023-06-27 21:02:53 +0200 | <jade[m]> | actually nevermind |
2023-06-27 21:03:43 +0200 | <EvanR_> | :t appEndo . mconcat . map Endo |
2023-06-27 21:03:45 +0200 | <lambdabot> | [a -> a] -> a -> a |
2023-06-27 21:04:15 +0200 | <mauke> | mappendo patronum |
2023-06-27 21:04:18 +0200 | <jade[m]> | I need to learn about the Endo shit |
2023-06-27 21:04:25 +0200 | <jade[m]> | I think it just means "within" or something |
2023-06-27 21:04:42 +0200 | <ncf> | EvanR_: yeah, i guess "programmable semicolons" are only really useful when they stand for more characters than `.` |
2023-06-27 21:04:45 +0200 | <mauke> | Endo a ~ a -> a |
2023-06-27 21:04:47 +0200 | nut | (~nut@176-151-21-224.abo.bbox.fr) (Ping timeout: 264 seconds) |
2023-06-27 21:04:56 +0200 | <ncf> | (but they already do if you also use <-) |
2023-06-27 21:05:00 +0200 | <EvanR_> | Endo wraps an a -> a to treat it like a monoid in the obvious way |
2023-06-27 21:05:16 +0200 | <jade[m]> | oh that's simple |
2023-06-27 21:05:22 +0200 | <mauke> | the function stays within one set (type) |
2023-06-27 21:05:23 +0200 | <jade[m]> | thanks lol |
2023-06-27 21:05:45 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
2023-06-27 21:05:54 +0200 | <jade[m]> | mauke: that's the 'endo' of it, right? |
2023-06-27 21:06:17 +0200 | <mauke> | yes |
2023-06-27 21:06:21 +0200 | <ncf> | same endo as in endofunctor (Type -> Type) |
2023-06-27 21:06:37 +0200 | <EvanR_> | Hask -> Hask |
2023-06-27 21:09:10 +0200 | <ncf> | (well Endo stands for endomorphism) |
2023-06-27 21:10:18 +0200 | <EvanR_> | ncf, that's a good point. People complain that haskell has too many operators, it should read more like english. But wait, english has all this punctuation so there. |
2023-06-27 21:10:52 +0200 | <EvanR_> | and like english, haskell has semicolons but no one uses them anymore |
2023-06-27 21:11:49 +0200 | <jade[m]> | I like semicolons; they look fancy |
2023-06-27 21:12:18 +0200 | EvanR_ | reprograms that semicolon |
2023-06-27 21:12:24 +0200 | <mauke> | pro-gamer move: use semicolons for indentation |
2023-06-27 21:13:59 +0200 | <ncf> | ah yes, colayout |
2023-06-27 21:14:19 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 21:14:40 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 21:15:54 +0200 | EvanR_ | EvanR |
2023-06-27 21:16:48 +0200 | ubert | (~Thunderbi@p200300ecdf0b5713a8f894b1f77d0827.dip0.t-ipconnect.de) |
2023-06-27 21:18:01 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 21:20:51 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-06-27 21:25:32 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
2023-06-27 21:25:36 +0200 | ft | (~ft@p508db151.dip0.t-ipconnect.de) |
2023-06-27 21:26:02 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
2023-06-27 21:28:39 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 21:28:52 +0200 | priesvitne_sklo | (~priesvitn@2a02:8308:708d:9300:80da:5e61:c07a:8406) |
2023-06-27 21:29:00 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 21:33:06 +0200 | pavonia | (~user@user/siracusa) |
2023-06-27 21:33:27 +0200 | fweht | (uid404746@id-404746.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2023-06-27 21:34:01 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) |
2023-06-27 21:35:15 +0200 | reach | (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) |
2023-06-27 21:36:45 +0200 | thegeekinside | (~thegeekin@189.217.90.138) (Remote host closed the connection) |
2023-06-27 21:37:07 +0200 | thegeekinside | (~thegeekin@189.217.90.138) |
2023-06-27 21:38:05 +0200 | <sm> | haskell;tiny-coders;use;semicolons 👍️ |
2023-06-27 21:40:34 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 21:43:05 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 21:43:25 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 21:44:28 +0200 | mechap | (~mechap@user/mechap) |
2023-06-27 21:45:05 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
2023-06-27 21:45:26 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) |
2023-06-27 21:45:32 +0200 | Square2 | (~Square@user/square) |
2023-06-27 21:50:04 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a833:b88c:109c:523a) (Ping timeout: 258 seconds) |
2023-06-27 21:51:21 +0200 | pepeiborra | (sid443799@id-443799.ilkley.irccloud.com) (Server closed connection) |
2023-06-27 21:51:30 +0200 | pepeiborra | (sid443799@id-443799.ilkley.irccloud.com) |
2023-06-27 21:53:02 +0200 | sm[i] | (~smi]@plaintextaccounting/sm) |
2023-06-27 21:53:32 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 21:53:53 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 21:57:42 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 22:01:53 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
2023-06-27 22:04:13 +0200 | trev | (~trev@user/trev) (Quit: trev) |
2023-06-27 22:05:14 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 22:05:34 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 22:08:20 +0200 | gnalzo | (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
2023-06-27 22:10:51 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2023-06-27 22:12:42 +0200 | oo_miguel | (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) (Ping timeout: 245 seconds) |
2023-06-27 22:22:44 +0200 | taupiqueur | (~taupiqueu@2a02-8440-2441-73e5-e546-cb01-f27c-8b10.rev.sfr.net) |
2023-06-27 22:23:54 +0200 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
2023-06-27 22:23:57 +0200 | reach | (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) (Remote host closed the connection) |
2023-06-27 22:24:19 +0200 | reach | (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) |
2023-06-27 22:25:15 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 22:25:36 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 22:31:35 +0200 | sm[i] | (~smi]@plaintextaccounting/sm) (Ping timeout: 246 seconds) |
2023-06-27 22:32:16 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-06-27 22:38:24 +0200 | smoge | (~smoge@2603-7000-4b42-1100-e0fb-24a1-4145-060c.res6.spectrum.com) |
2023-06-27 22:38:46 +0200 | Techcable | (~Techcable@user/Techcable) (Remote host closed the connection) |
2023-06-27 22:40:50 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 22:40:54 +0200 | Techcable | (~Techcable@user/Techcable) |
2023-06-27 22:41:08 +0200 | priesvitne_sklo | (~priesvitn@2a02:8308:708d:9300:80da:5e61:c07a:8406) (Ping timeout: 240 seconds) |
2023-06-27 22:41:11 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 22:45:09 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 246 seconds) |
2023-06-27 22:47:08 +0200 | priesvitne_sklo | (~priesvitn@2a02:8308:708d:9300:5598:ffce:32b7:825d) |
2023-06-27 22:47:44 +0200 | ceoltb^ | (~ceoltb@24.125.210.85) |
2023-06-27 22:51:20 +0200 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
2023-06-27 22:53:57 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 22:54:17 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 22:55:06 +0200 | reach | (~reach@bras-base-toroon2643w-grc-19-74-12-129-40.dsl.bell.ca) (Ping timeout: 260 seconds) |
2023-06-27 22:59:56 +0200 | priesvitne_sklo | (~priesvitn@2a02:8308:708d:9300:5598:ffce:32b7:825d) (Ping timeout: 240 seconds) |
2023-06-27 23:01:47 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
2023-06-27 23:08:00 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 23:08:21 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 23:15:25 +0200 | <EvanR> | tiny;haskell;concert |
2023-06-27 23:16:41 +0200 | <darkling> | Where's that? :) |
2023-06-27 23:18:04 +0200 | pavonia | (~user@user/siracusa) (Read error: Connection reset by peer) |
2023-06-27 23:18:35 +0200 | taupiqueur | (~taupiqueu@2a02-8440-2441-73e5-e546-cb01-f27c-8b10.rev.sfr.net) (Ping timeout: 264 seconds) |
2023-06-27 23:20:48 +0200 | pavonia | (~user@user/siracusa) |
2023-06-27 23:21:35 +0200 | haritz | (~hrtz@user/haritz) (Ping timeout: 264 seconds) |
2023-06-27 23:21:37 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-06-27 23:23:21 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 23:23:41 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 23:24:31 +0200 | <monochrom> | Unpopular opinion: English reads like hogwash. |
2023-06-27 23:26:22 +0200 | nate2 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 250 seconds) |
2023-06-27 23:26:57 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
2023-06-27 23:27:14 +0200 | smoge | (~smoge@2603-7000-4b42-1100-e0fb-24a1-4145-060c.res6.spectrum.com) (Ping timeout: 246 seconds) |
2023-06-27 23:29:22 +0200 | mei | (~mei@user/mei) |
2023-06-27 23:31:24 +0200 | mizlan | (~mizlan@c-73-63-223-227.hsd1.ca.comcast.net) |
2023-06-27 23:31:38 +0200 | <Rembane> | monochrom: You're not wrong |
2023-06-27 23:33:01 +0200 | <probie> | Time to migrate to Lojban |
2023-06-27 23:33:02 +0200 | <geekosaur> | "…came from Norman fighters trying to pick up Saxon barmaids, and no more legitimate than the other results…" |
2023-06-27 23:33:52 +0200 | <geekosaur> | s/fighters/soldiers/ |
2023-06-27 23:34:27 +0200 | <Rembane> | Is this in 1066? |
2023-06-27 23:34:43 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
2023-06-27 23:34:48 +0200 | <geekosaur> | H. Beam Piper |
2023-06-27 23:35:38 +0200 | <geekosaur> | sadly I no longer have my copies of those books to verify which of his Federation novels it was, although I'm pretty sure it was _Fuzzies and Other People_ |
2023-06-27 23:35:51 +0200 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
2023-06-27 23:36:21 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
2023-06-27 23:37:00 +0200 | <monochrom> | To be honest and more blunt and harsh, any natural language that becomes popular, I'll still say "it reads like hogwash". Or generally any natural language. Or more focusedly any attempt at bringing natural language to programming. |
2023-06-27 23:37:11 +0200 | <darkling> | "We don't just borrow words; on occasion, English has pursued other languages down alleyways to beat them unconscious and rifle their pockets for new vocabulary." |
2023-06-27 23:37:24 +0200 | <geekosaur> | 🙂 |
2023-06-27 23:37:25 +0200 | <dolio> | Yeah, people who want to program in natural language should just be ignored. |
2023-06-27 23:37:42 +0200 | <Rembane> | darkling: Sounds like Pratchett. Who's the author of that quote? |
2023-06-27 23:38:00 +0200 | <monochrom> | And we already have COBOL for those who still want it. |
2023-06-27 23:38:01 +0200 | <darkling> | James Nicoll. |
2023-06-27 23:38:09 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
2023-06-27 23:38:09 +0200 | <Rembane> | Cool! |
2023-06-27 23:38:29 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 23:39:47 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
2023-06-27 23:39:51 +0200 | <dolio> | COBOL is a fine example. It's not anything like natural language. |
2023-06-27 23:40:56 +0200 | <monochrom> | OK, to compensate for my whining, is there anything I can help with today? :) |
2023-06-27 23:41:15 +0200 | codaraxis | (~codaraxis@user/codaraxis) (Quit: Leaving) |
2023-06-27 23:42:52 +0200 | <monochrom> | BTW in my course I decided to skip Functor, Applicative, Monad, Alternative. I'm jumping directly into parser combinators. I have "import Prelude hiding ((>>=), fmap, ...)" and define (>>=), fmap, ... with types nailed to Parser. |
2023-06-27 23:43:28 +0200 | <monochrom> | I plan to bring up FAM in the last week and reveal/confess Parser is an instance. |
2023-06-27 23:44:23 +0200 | <geekosaur> | mm, somehow I thought that was something you were already doing |
2023-06-27 23:46:13 +0200 | <monochrom> | I have also begun to teach ⊥: http://www.cs.utoronto.ca/~trebla/CSCC24-2023-Summer/partial-order-recursion.html |
2023-06-27 23:49:36 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:296e:3128:9bb:592b) |
2023-06-27 23:49:41 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 23:50:02 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 23:50:31 +0200 | <ncf> | > Each set is required to have least upper bounds for not just ascending chains, but also non-empty totally-ordered subsets. |
2023-06-27 23:50:32 +0200 | <lambdabot> | <hint>:1:78: error: parse error on input ‘,’ |
2023-06-27 23:50:36 +0200 | <ncf> | aren't those the same? |
2023-06-27 23:51:09 +0200 | <ncf> | (i think the usual definition is rather dcpos, i.e. lubs for directed subsets) |
2023-06-27 23:51:15 +0200 | <monochrom> | You may need to read the fine prints of "ascending chains". |
2023-06-27 23:51:31 +0200 | carter | (sid14827@id-14827.helmsley.irccloud.com) (Server closed connection) |
2023-06-27 23:51:48 +0200 | <monochrom> | Oh, it's me. OK, here it goes. |
2023-06-27 23:52:05 +0200 | carter | (sid14827@id-14827.helmsley.irccloud.com) |
2023-06-27 23:52:17 +0200 | <monochrom> | ascending chains are ω-chains, i.e., x0 <= x1 <= x2 <= ... |
2023-06-27 23:53:09 +0200 | <monochrom> | The integers form a non-empty totally ordered set under integer's <= but it is not an ω-chain. |
2023-06-27 23:53:40 +0200 | <monochrom> | But I also have "I still have to find out how much the difference matters." so heh |
2023-06-27 23:53:44 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:296e:3128:9bb:592b) (Ping timeout: 246 seconds) |
2023-06-27 23:53:49 +0200 | <ncf> | right. you can take any integer as your x0 and get an ω-chain with the same lub trivially though |
2023-06-27 23:54:23 +0200 | <dolio> | What about ordinals larger than ω? |
2023-06-27 23:54:37 +0200 | <monochrom> | There is an extra extra lie about directed-complete and then we need the rabbit hole of the axiom of choice... |
2023-06-27 23:54:38 +0200 | <ncf> | fair |
2023-06-27 23:55:41 +0200 | <monochrom> | I should have gone big for the real numbers... |
2023-06-27 23:55:53 +0200 | <dolio> | Yeah. |
2023-06-27 23:56:16 +0200 | <monochrom> | Now we also invoke the rabbit hole of CH... >:D |
2023-06-27 23:56:25 +0200 | <dolio> | Real numbers aren't totally ordered, though, clearly. :þ |
2023-06-27 23:56:37 +0200 | <monochrom> | :( |
2023-06-27 23:57:23 +0200 | <ncf> | the rabbit hole just fell down a rabbit hole |
2023-06-27 23:58:52 +0200 | driib | (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
2023-06-27 23:59:12 +0200 | driib | (~driib@vmi931078.contaboserver.net) |
2023-06-27 23:59:20 +0200 | <dolio> | Oh yeah, also, the reals might be countable. |
2023-06-27 23:59:27 +0200 | <dolio> | In that case there is a total order. :) |