Logs on 2023-01-30 (liberachat/#haskell)
| 00:00:33 | <monochrom> | I think I haven't heard of other people here using summoner at all in the past. |
| 00:01:18 | → | Nolrai joins (~Nolrai@c-73-240-99-98.hsd1.or.comcast.net) |
| 00:01:33 | <Nolrai> | Man it is quiet here. |
| 00:01:53 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 00:02:35 | <monochrom> | So what do they use? cabal has a "cabal init", stack has a similar command, and I also heard that some people keep around their favourite starter directory structures. |
| 00:06:31 | <geekosaur> | dunno about where you are, but it's Sunday night here and as usual for Sunday it has indeed been quiet |
| 00:08:11 | × | thyriaen quits (~thyriaen@2a01:aea0:dd4:4fa4:6245:cbff:fe9f:48b1) (Quit: Leaving) |
| 00:08:27 | <geekosaur> | and I just copy a cabal file, LICENSE, etc. from some other project to get started 🙂 |
| 00:13:04 | <jackdk> | I copy a previous project or `cabal init` |
| 00:13:47 | <yushyin> | i bet some use nix flake templates |
| 00:16:44 | → | bhall joins (~brunohall@138.199.22.99) |
| 00:17:16 | <EvanR> | can you guys keep it down in here, it's Sunday |
| 00:17:36 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 248 seconds) |
| 00:18:36 | <Nolrai> | :P |
| 00:18:45 | <Nolrai> | Anyway, thanks! |
| 00:22:23 | <jackdk> | No it's not. |
| 00:22:53 | <geekosaur> | noticed that, just ticked over 20ish minutes ago UTC |
| 00:25:26 | × | acidjnk quits (~acidjnk@p200300d6e715c427397aaa65a333c5a9.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 00:27:01 | → | freeside joins (~mengwong@103.252.202.170) |
| 00:30:59 | → | mikoto-chan joins (~mikoto-ch@2001:999:58c:394a:63de:7cd7:5e1f:8502) |
| 00:31:46 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 268 seconds) |
| 00:32:08 | × | sawilagar quits (~sawilagar@user/sawilagar) (Quit: Leaving) |
| 00:35:10 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 00:35:11 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 00:35:11 | → | wroathe joins (~wroathe@user/wroathe) |
| 00:37:37 | <sclv> | Nolrai: I just use "cabal init" and go from there |
| 00:37:37 | × | danza quits (~francesco@rm-19-52-159.service.infuturo.it) (Read error: Connection reset by peer) |
| 00:37:58 | <sclv> | i find any other scaffolding beyond that is way too specific to one or another specific type of project |
| 00:38:01 | → | danza joins (~francesco@rm-19-52-159.service.infuturo.it) |
| 00:40:21 | × | mikoto-chan quits (~mikoto-ch@2001:999:58c:394a:63de:7cd7:5e1f:8502) (Ping timeout: 252 seconds) |
| 00:43:04 | × | Inst quits (~Inst@c-98-208-218-119.hsd1.fl.comcast.net) (Ping timeout: 260 seconds) |
| 00:46:05 | × | laalyn quits (~laalyn@c-73-241-126-7.hsd1.ca.comcast.net) (Quit: Client closed) |
| 00:46:23 | × | jwiegley quits (~jwiegley@2600:1700:cf00:db0:ad33:58f8:1ff9:4d13) (Quit: ZNC - http://znc.in) |
| 00:46:23 | × | johnw quits (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Quit: ZNC - http://znc.in) |
| 00:47:14 | → | mikoto-chan joins (~mikoto-ch@2001:999:68c:b163:558d:f376:4e18:be8e) |
| 01:00:12 | → | freeside joins (~mengwong@103.252.202.170) |
| 01:01:33 | × | Nolrai quits (~Nolrai@c-73-240-99-98.hsd1.or.comcast.net) (Quit: Client closed) |
| 01:04:33 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
| 01:04:34 | × | Ranhir quits (~Ranhir@157.97.53.139) (Read error: Connection reset by peer) |
| 01:07:33 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
| 01:09:11 | × | mikoto-chan quits (~mikoto-ch@2001:999:68c:b163:558d:f376:4e18:be8e) (Quit: WeeChat 3.6) |
| 01:09:47 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 255 seconds) |
| 01:11:40 | → | Ranhir joins (~Ranhir@157.97.53.139) |
| 01:11:44 | <jean-paul[m]> | https://github.com/JonathanLorimer/templates/blob/main/template/haskell/flake.nix is nice for doing stuff like getting a compatible haskell-language-server installed and setting up formatting commit hooks |
| 01:12:18 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:14:21 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) (Remote host closed the connection) |
| 01:14:25 | <jean-paul[m]> | you still have to run cabal init yourself |
| 01:15:08 | → | freeside joins (~mengwong@103.252.202.170) |
| 01:18:26 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:19:52 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 268 seconds) |
| 01:21:13 | × | Guest75 quits (~Guest75@178.141.149.12) (Ping timeout: 260 seconds) |
| 01:25:52 | × | xff0x quits (~xff0x@2405:6580:b080:900:ccbb:e6cd:6139:338f) (Ping timeout: 248 seconds) |
| 01:29:47 | × | m1dnight quits (~christoph@78-22-0-121.access.telenet.be) (Ping timeout: 265 seconds) |
| 01:35:52 | × | cheater quits (~Username@user/cheater) (Read error: Connection reset by peer) |
| 01:40:26 | <sm> | hmm.. what tricks exist for re-exporting qualified imports, eg in a batteries-included module for beginners ? |
| 01:40:56 | <sm> | I've got the required imports down to |
| 01:40:56 | <sm> | import qualified "text" Data.Text as T |
| 01:40:56 | <sm> | import qualified "text" Data.Text.IO as T |
| 01:40:56 | <sm> | import Hledger.Cli.Script |
| 01:41:11 | <sm> | which is not quite beginner friendly |
| 01:48:41 | → | potash joins (~foghorn@user/foghorn) |
| 01:51:52 | → | m1dnight joins (~christoph@78-22-0-121.access.telenet.be) |
| 02:00:06 | × | potash quits (~foghorn@user/foghorn) (Read error: Connection reset by peer) |
| 02:00:07 | × | beteigeuze quits (~Thunderbi@bl14-81-220.dsl.telepac.pt) (Read error: Connection reset by peer) |
| 02:01:22 | → | freeside joins (~mengwong@122.11.248.245) |
| 02:04:48 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 248 seconds) |
| 02:09:04 | × | jargon quits (~jargon@184.101.188.5) (Remote host closed the connection) |
| 02:11:59 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:14:51 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) |
| 02:15:10 | × | Jeanne-Kamikaze quits (~Jeanne-Ka@142.147.89.202) (Ping timeout: 252 seconds) |
| 02:17:19 | <sm> | I notice there's ImportQualifiedPost, which makes it: |
| 02:17:19 | <sm> | import "text" Data.Text qualified as T |
| 02:17:19 | <sm> | import "text" Data.Text.IO qualified as T |
| 02:17:19 | <sm> | (less alignment-hostile) |
| 02:18:12 | oldfashionedcow | is now known as A_Cow[broke] |
| 02:18:34 | sm | wants PackageImportsPost too |
| 02:19:10 | <sm> | import Data.Text as T qualified from "text" |
| 02:19:34 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) (Ping timeout: 252 seconds) |
| 02:20:06 | A_Cow[broke] | is now known as oldfashionedcow |
| 02:20:30 | × | azimut_ quits (~azimut@gateway/tor-sasl/azimut) (Quit: ZNC - https://znc.in) |
| 02:20:59 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 02:21:03 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) |
| 02:21:06 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 02:22:08 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 02:24:31 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 248 seconds) |
| 02:26:47 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 02:30:45 | × | bontaq quits (~user@ool-45779fe5.dyn.optonline.net) (Ping timeout: 260 seconds) |
| 02:33:54 | × | opticblast quits (~Thunderbi@172.58.84.5) (Ping timeout: 260 seconds) |
| 02:38:12 | → | ddb joins (~ddb@tilde.club) |
| 02:38:16 | → | opticblast joins (~Thunderbi@172.58.85.230) |
| 02:39:26 | × | mei quits (~mei@user/mei) (Ping timeout: 268 seconds) |
| 02:40:15 | × | m1dnight quits (~christoph@78-22-0-121.access.telenet.be) (Ping timeout: 252 seconds) |
| 02:40:34 | → | razetime joins (~Thunderbi@117.193.5.58) |
| 02:42:07 | → | cheater joins (~Username@user/cheater) |
| 02:42:15 | → | m1dnight joins (~christoph@78-22-0-121.access.telenet.be) |
| 02:46:37 | ← | pragma- parts (~chaos@user/pragmatic-chaos) (Bye!) |
| 02:47:05 | × | jero98772 quits (~jero98772@2800:484:1d80:d8ce:4f4f:dc32:b9c4:cb5b) (Remote host closed the connection) |
| 02:49:28 | → | Sgeo_ joins (~Sgeo@user/sgeo) |
| 02:50:28 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 02:52:48 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 03:09:00 | × | danza quits (~francesco@rm-19-52-159.service.infuturo.it) (Read error: Connection reset by peer) |
| 03:10:01 | × | AkechiShiro quits (~licht@user/akechishiro) (Ping timeout: 252 seconds) |
| 03:11:05 | → | AkechiShiro joins (~licht@user/akechishiro) |
| 03:12:52 | × | carbolymer quits (~carbolyme@dropacid.net) (Ping timeout: 252 seconds) |
| 03:13:01 | → | carbolymer joins (~carbolyme@dropacid.net) |
| 03:14:47 | × | td_ quits (~td@i5387093F.versanet.de) (Ping timeout: 252 seconds) |
| 03:16:49 | → | td_ joins (~td@i53870926.versanet.de) |
| 03:18:33 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 03:18:42 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
| 03:24:28 | → | danza joins (~francesco@151.43.48.52) |
| 03:27:55 | × | freeside quits (~mengwong@122.11.248.245) (Ping timeout: 252 seconds) |
| 03:28:17 | → | bilegeek joins (~bilegeek@2600:1008:b049:eb4:91c5:5c6c:4cde:3554) |
| 03:35:33 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 03:35:37 | → | freeside joins (~mengwong@122.11.248.245) |
| 03:41:07 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:41:07 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:41:07 | finn_elija | is now known as FinnElija |
| 03:53:35 | × | freeside quits (~mengwong@122.11.248.245) (Ping timeout: 248 seconds) |
| 04:05:38 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 255 seconds) |
| 04:13:07 | × | danza quits (~francesco@151.43.48.52) (Read error: Connection reset by peer) |
| 04:13:31 | → | danza joins (~francesco@151.43.48.52) |
| 04:14:03 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 04:14:42 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 04:22:34 | × | h2017 quits (~h2017@bras-base-clbaon0201w-grc-20-184-144-57-44.dsl.bell.ca) (Quit: Leaving) |
| 04:24:48 | <smol-hors> | hmm, I'm trying to build a ghc to cross compile from linux to windows.. I tried `ghcup compile ghc -j 4 -b 9.0.2 -v 9.2.5 -x i686-w64-mingw32`, but I don't think that's right because I get `fatal error: windows.h: No such file or directory` |
| 04:26:26 | <Lycurgus> | why do you need a cross compile? why not compile separately? |
| 04:27:03 | <Lycurgus> | hs isn't binary portable |
| 04:27:41 | <Lycurgus> | even if it is the math java |
| 04:28:03 | <smol-hors> | as in compile on windows? I tried but I had problems linking the C++ and C parts of my program to the Haskell parts of my program |
| 04:28:28 | <Lycurgus> | cross compile isn't the solution |
| 04:29:05 | <smol-hors> | had Warning: corrupt .drectve at end of def file |
| 04:29:23 | <smol-hors> | ok |
| 04:29:50 | <Lycurgus> | yeah if you mess in hs at the ffi level bad stuff happens with ease if you're not sure of what ur doin |
| 04:31:05 | <Lycurgus> | others can say, but i'm not sure how good the ghc windows support is |
| 04:31:22 | <smol-hors> | it runs on mingw anyway :p |
| 04:31:33 | <smol-hors> | which is apparently where the above warning comes from |
| 04:31:36 | <Lycurgus> | oh yeah and there's that |
| 04:31:40 | <Lycurgus> | unix in dos |
| 04:32:05 | <smol-hors> | so what's the proper way to write a program in C++ and Haskell on Windows? |
| 04:32:20 | <Lycurgus> | only used mingw once, a contract to do a branded version of mozilla on three platforms |
| 04:32:48 | <Lycurgus> | use regular ghc for windows |
| 04:33:04 | <smol-hors> | oh, is there a native ghc for windows? |
| 04:33:07 | <Lycurgus> | and regular windows for c |
| 04:33:12 | <smol-hors> | I just used ghcup because I thought it was recommended |
| 04:33:13 | <Lycurgus> | you don't need mingw |
| 04:33:21 | <smol-hors> | oh, good |
| 04:33:47 | <Lycurgus> | ghcup is just a convenience tool |
| 04:33:58 | <smol-hors> | all right. thanks :) |
| 04:34:05 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 255 seconds) |
| 04:34:15 | <Lycurgus> | np |
| 04:34:36 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 04:35:30 | Lycurgus | checks ghc on dos |
| 04:35:37 | × | nattiestnate quits (~nate@202.138.250.37) (Quit: WeeChat 3.8) |
| 04:36:31 | oldfashionedcow | is now known as newfashionedcow |
| 04:36:43 | <Lycurgus> | yeah there's two, depending on how you wanna handle bignums |
| 04:36:49 | <smol-hors> | https://www.haskell.org/ghc/download_ghc_9_4_4.html#windows64 |
| 04:37:05 | <smol-hors> | am I in the right place? I can only see mingw |
| 04:37:09 | newfashionedcow | is now known as oldfashionedrat |
| 04:37:39 | oldfashionedrat | is now known as A_Cow |
| 04:37:42 | <Lycurgus> | the gmp would be preferable but then you gotta get gmp on windows so maybe the haskell implementation is better |
| 04:38:24 | × | razetime quits (~Thunderbi@117.193.5.58) (Ping timeout: 248 seconds) |
| 04:38:31 | <Lycurgus> | ah yeah i see now |
| 04:38:38 | <Lycurgus> | was afraid of that |
| 04:38:52 | <Lycurgus> | see ppl don't like windows |
| 04:39:13 | <Lycurgus> | and so the ghc ppl have pinned the dos impl on mingw |
| 04:39:16 | <Lycurgus> | bummer |
| 04:39:24 | <smol-hors> | rip |
| 04:39:55 | <Lycurgus> | instead of doing a proper dos port |
| 04:40:13 | <Lycurgus> | it's win32 too so ur c needs to use win32 |
| 04:40:55 | <Lycurgus> | that's what you typically find in advanced computing cultures, not just hs |
| 04:42:17 | <Lycurgus> | if possible i'd see if i could run the haskell on unix and communicate with whatever has to be on dos |
| 04:43:34 | <smol-hors> | that is why I thought of cross-compilation using mingw. I got it working with C and C++ but the -x i686-w64-mingw32 for ghcup wanted a windows.h :S |
| 04:44:29 | <Lycurgus> | yeah you'll have to hang out here or another hs channel for somebody with hs on dos experience, if such individuals exist |
| 04:44:50 | <Lycurgus> | prolly somebody will suggest F# |
| 04:44:55 | <smol-hors> | ok |
| 04:46:56 | × | jle` quits (~jle`@cpe-23-240-75-236.socal.res.rr.com) (Ping timeout: 248 seconds) |
| 04:47:02 | <Lycurgus> | windows.h will be in win32 headers |
| 04:47:27 | <Lycurgus> | installing visual studio should get it but havent' done dos dev in a while |
| 04:47:59 | <Lycurgus> | unless that means somebody elses (mingw, ghc) windows.h |
| 04:48:59 | <smol-hors> | hmm |
| 04:49:02 | → | jle` joins (~jle`@cpe-23-240-75-236.socal.res.rr.com) |
| 04:49:18 | <Lycurgus> | there days dos has a unix env but I don't know anything about it |
| 04:49:56 | <Lycurgus> | hs on windows sounds like a footgun operation |
| 04:51:24 | <Lycurgus> | s/there/these/ |
| 04:56:24 | × | Vajb quits (~Vajb@2001:999:404:9516:d621:6cbe:c71e:5686) (Read error: Connection reset by peer) |
| 04:56:47 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) |
| 04:59:09 | × | phma quits (~phma@2001:5b0:210b:94b8:7a1f:f3bb:5a0c:334d) (Read error: Connection reset by peer) |
| 05:00:02 | → | phma joins (~phma@host-67-44-208-154.hnremote.net) |
| 05:01:26 | × | A_Cow quits (~Rahul_San@user/oldfashionedcow) (Quit: WeeChat 3.8) |
| 05:02:56 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 05:02:58 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 05:03:27 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 05:05:32 | <Lycurgus> | also you might search the logs for 'windows' |
| 05:06:03 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: Exeunt: personae.ai-integration.biz) |
| 05:07:33 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 05:07:36 | → | khumba joins (~khumba@user/khumba) |
| 05:08:06 | → | Vajb joins (~Vajb@2001:999:404:9516:d621:6cbe:c71e:5686) |
| 05:11:23 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
| 05:12:00 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 05:12:42 | <Lycurgus> | also looks like there's a build from source for windows, that might be a proper port |
| 05:13:02 | <smol-hors> | o |
| 05:13:46 | × | Lycurgus quits (~juan@user/Lycurgus) (Client Quit) |
| 05:16:03 | × | Neuromancer quits (~Neuromanc@user/neuromancer) (Ping timeout: 260 seconds) |
| 05:21:48 | <smol-hors> | on ghcup there is ghcup compile ghc |
| 05:24:04 | <smol-hors> | not sure why they'd only package it with mingw if that is the case |
| 05:24:21 | <smol-hors> | but worth a try |
| 05:26:27 | <smol-hors> | hmm, I can probably just use the -x blah command line from windows... |
| 05:26:32 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 268 seconds) |
| 05:26:52 | <smol-hors> | oh, but that defeats the purpose, nvm |
| 05:27:32 | <smol-hors> | hmm |
| 05:31:04 | <smol-hors> | if this doesn't work I can just cross-compile the C/C++ parts on linux to make them mingw-y and then the Haskell parts on Windows to make them mingw-y :S |
| 05:32:01 | <smol-hors> | Fetching https://downloads.haskell.org/ghc/mingw/0.3/x86_64/mingw-w64-x86_64-mpfr-4.0.2-2-any.pkg.tar.xz => ghc-tarballs/mingw-w64/x86_64/mingw-w64-x86_64-mpfr-4.0.2-2-any.pkg.tar.xz |
| 05:32:02 | <smol-hors> | ye |
| 05:38:12 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 05:46:44 | <smol-hors> | ok, that works. I just need ghc.exe as my ghc and x86_64-w64-mingw-g{cc, ++} as my C/C++ compilers :p |
| 05:48:07 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) (Remote host closed the connection) |
| 05:48:26 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 05:48:37 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) (Read error: Connection reset by peer) |
| 05:48:59 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 248 seconds) |
| 05:50:44 | → | cyphase joins (~cyphase@user/cyphase) |
| 05:58:37 | × | mcglk quits (~mcglk@131.191.49.120) (Read error: Connection reset by peer) |
| 06:01:35 | → | mcglk joins (~mcglk@131.191.49.120) |
| 06:01:46 | → | johnw joins (~johnw@2600:1700:cf00:db0:f0d6:3852:1ef5:be75) |
| 06:01:49 | × | bilegeek quits (~bilegeek@2600:1008:b049:eb4:91c5:5c6c:4cde:3554) (Quit: Leaving) |
| 06:02:00 | → | Guest75 joins (~Guest75@178.141.149.12) |
| 06:02:21 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 252 seconds) |
| 06:04:27 | → | mechap joins (~mechap@user/mechap) |
| 06:06:20 | → | varoo joins (~varoo@122.161.91.19) |
| 06:06:56 | × | opticblast quits (~Thunderbi@172.58.85.230) (Ping timeout: 248 seconds) |
| 06:06:56 | × | jbalint quits (~jbalint@2600:6c44:117f:e98a:816a:9488:fb1:7b7) (Ping timeout: 248 seconds) |
| 06:11:04 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:14:00 | → | freeside joins (~mengwong@122.11.248.245) |
| 06:17:34 | → | jbalint joins (~jbalint@2600:6c44:117f:e98a:816a:9488:fb1:7b7) |
| 06:26:00 | × | khumba quits (~khumba@user/khumba) () |
| 06:32:15 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 06:32:15 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 06:32:15 | → | wroathe joins (~wroathe@user/wroathe) |
| 06:36:45 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
| 06:37:11 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:37:11 | → | waleee joins (~waleee@h-176-10-137-138.NA.cust.bahnhof.se) |
| 06:40:04 | → | razetime joins (~Thunderbi@117.193.5.58) |
| 06:40:13 | × | mcglk quits (~mcglk@131.191.49.120) (Quit: (seeya)) |
| 06:47:19 | × | waleee quits (~waleee@h-176-10-137-138.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 06:48:48 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 06:49:20 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:54:18 | → | trev joins (~trev@user/trev) |
| 07:00:30 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 07:03:11 | → | michalz joins (~michalz@185.246.207.197) |
| 07:03:47 | × | teddyc quits (theodorc@cassarossa.samfundet.no) (Ping timeout: 246 seconds) |
| 07:08:44 | × | danza quits (~francesco@151.43.48.52) (Read error: Connection reset by peer) |
| 07:15:22 | × | Sgeo_ quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:17:08 | → | teddyc joins (theodorc@cassarossa.samfundet.no) |
| 07:18:52 | → | mcglk joins (~mcglk@131.191.49.120) |
| 07:19:38 | × | freeside quits (~mengwong@122.11.248.245) (Ping timeout: 252 seconds) |
| 07:21:10 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 07:24:25 | → | danza joins (~francesco@151.35.92.17) |
| 07:26:44 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:30:18 | × | phma quits (~phma@host-67-44-208-154.hnremote.net) (Read error: Connection reset by peer) |
| 07:31:12 | → | phma joins (phma@2001:5b0:212a:9278:328d:f1cd:3dee:19c5) |
| 07:36:26 | → | kenran joins (~user@user/kenran) |
| 07:42:29 | → | mmhat joins (~mmh@p200300f1c707beafee086bfffe095315.dip0.t-ipconnect.de) |
| 07:43:01 | × | mmhat quits (~mmh@p200300f1c707beafee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
| 07:46:15 | → | mei joins (~mei@user/mei) |
| 08:02:09 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 08:04:31 | → | zeenk joins (~zeenk@2a02:2f04:a014:8700::7fe) |
| 08:04:36 | → | kenran` joins (~user@user/kenran) |
| 08:05:49 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:8095:1260:6fef:5d26) |
| 08:06:24 | × | kenran quits (~user@user/kenran) (Ping timeout: 248 seconds) |
| 08:12:34 | → | kuribas joins (~user@ptr-17d51emy7j9a6t4odfa.18120a2.ip6.access.telenet.be) |
| 08:16:52 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 08:17:04 | × | elkcl quits (~elkcl@broadband-37-110-27-252.ip.moscow.rt.ru) (Ping timeout: 248 seconds) |
| 08:22:49 | <kuribas> | Would it be possible to create a lightweight langage with dependent types but without the complexity of current DT language? |
| 08:23:49 | <merijn> | That depends on where you perceive the complexity of those languages to be? |
| 08:24:14 | <kuribas> | well, for example full dependence of values and types. |
| 08:24:24 | <kuribas> | requiring partial evaluation. |
| 08:24:39 | <kuribas> | instead of just allowing functions at type level. |
| 08:25:06 | <merijn> | kuribas: How would you know if something type checks with functions at the type level, but no partial evaluation? |
| 08:25:07 | <tomsmeding> | that's not "dependent types" :p |
| 08:25:15 | <kuribas> | merijn: full evaluation? |
| 08:25:30 | <merijn> | kuribas: You don't always have the data for full evaluation |
| 08:25:45 | <merijn> | kuribas: What if part of the type data is coming from runtime data? |
| 08:25:46 | → | elkcl joins (~elkcl@broadband-37-110-27-252.ip.moscow.rt.ru) |
| 08:25:47 | <kuribas> | how is dependent haskell going to do that? |
| 08:26:18 | <merijn> | kuribas: The same way as Agda and Coq, presumably |
| 08:26:22 | <tomsmeding> | doesn't ghc _already_ do symbolic evaluation at the type level with type families |
| 08:26:24 | <merijn> | (or Idris) |
| 08:26:28 | <merijn> | tomsmeding: yes |
| 08:26:29 | <kuribas> | merijn: indeed, not "real" dependent types then. |
| 08:26:39 | <merijn> | kuribas: ?? |
| 08:26:56 | <merijn> | How do agda and coq not have "real" dependent types?? |
| 08:27:03 | <tomsmeding> | kuribas: I haven't read this, but might be relevant, and sounds good given the author list http://strictlypositive.org/Easy.pdf |
| 08:27:20 | <kuribas> | merijn: I mean they have. But my hypothetical language not. |
| 08:28:51 | <tomsmeding> | also relevant: https://github.com/VictorTaelin/Formality |
| 08:29:09 | <kuribas> | hmm, but then adding unknown sized vectors gives a partial expression... |
| 08:29:25 | <kuribas> | like "Vector (n + m) Int" |
| 08:31:33 | <kuribas> | I guess partial evaluation is necessary then. |
| 08:31:58 | <tomsmeding> | (point of these two links is to show that implementing a full dependently-typed language is not super hard, apparently) |
| 08:32:14 | <tomsmeding> | (though they probably miss a couple of the niceties that other languages have) |
| 08:32:18 | <kuribas> | tomsmeding: ghc does, but I believe dependent haskell will allow you to run actual haskell functions at type level, no? |
| 08:32:25 | <tomsmeding> | kuribas: how is that different |
| 08:32:45 | <tomsmeding> | once you have partial evaluation, the "only" thing that's necessary is expanding the language on which you do so |
| 08:33:00 | <kuribas> | tomsmeding: well, the semantics of value and type functions are different in haskell. |
| 08:33:07 | <tomsmeding> | difficulty is that the current partial evaluation model is I think not suited for _efficiently_ doing so |
| 08:33:22 | <tomsmeding> | what's the difference? |
| 08:33:24 | <kuribas> | the haskell one? |
| 08:33:32 | <tomsmeding> | yeah |
| 08:33:40 | <kuribas> | tomsmeding: well, type functions are bidirectional, like in prolog. |
| 08:33:48 | → | freeside joins (~mengwong@103.252.202.170) |
| 08:33:50 | <tomsmeding> | that's just additional interpretations of existing code |
| 08:33:55 | <tomsmeding> | existing semantics doesn't change, right? |
| 08:34:17 | <tomsmeding> | it's not like those extra rules are _inconsistent_ with the existing semantics |
| 08:34:40 | <kuribas> | tomsmeding: I think idris typechecking is more efficient than haskell typelevel programming. There is normalization by evaluation which is supposedly very efficient. |
| 08:34:54 | <tomsmeding> | right, and ghc doesn't do that AFAIK |
| 08:35:19 | <kuribas> | tomsmeding: I guess not, just very tricky to implement... |
| 08:35:27 | <tomsmeding> | to a first approximation, I believe it evaluates a bit whenever it needs the information in order to continue typechecking |
| 08:35:36 | <tomsmeding> | like demand-driven evaluation, not "go for it now" |
| 08:36:48 | <tomsmeding> | previously with a weird flattening algorithm that did something special with type families, now (after richard eisenberg's recent simplifications) a less weird algorithm but one that still does something weird with type families |
| 08:37:10 | <kuribas> | type families are just very hard to reason about in haskell. |
| 08:37:18 | <kuribas> | I think dependent types are much easier. |
| 08:37:36 | <kuribas> | I don't get why so much haskell people have this conception that DT make stuff more complicated. |
| 08:37:46 | <kuribas> | stuff being type level programming of course. |
| 08:38:36 | <kuribas> | There is something to say about keeping things simple, but I don't like the clojure way of throwing away all static types. |
| 08:40:10 | <kuribas> | people at my work have been saying haskell and type system is too complicated, but I can do it because I have "a big brain". |
| 08:40:16 | <kuribas> | I am pretty sure that is not the case. |
| 08:40:25 | <kuribas> | At least not bigger than my colleages. |
| 08:41:02 | ← | nerdypepper parts (~nerdypepp@user/nerdypepper) (WeeChat 3.8) |
| 08:41:12 | <kuribas> | So I have been thinking about where the complexity is. |
| 08:41:25 | <tomsmeding> | are you sure it's not just familiarity? |
| 08:41:30 | <kuribas> | yeah indeed. |
| 08:41:37 | <kuribas> | And a lot of this knowledge builds up. |
| 08:41:49 | <kuribas> | IMO understanding DT starts with understanding curry-howard. |
| 08:42:01 | <tomsmeding> | programming experience with non-functional languages is almost useless when starting with haskell |
| 08:42:11 | <tomsmeding> | only later do you find the bits that you _can_ reuse |
| 08:42:13 | <kuribas> | well, these guys do clojure. |
| 08:42:23 | <tomsmeding> | I guess the same goes for functional but untyped languages, to a lesser extent |
| 08:42:36 | <kuribas> | But IMO clojure is closer to lisps than to static typed functional languages. |
| 08:42:46 | <kuribas> | because they use little abstraction |
| 08:43:03 | <kuribas> | instead use symbolic manipulation |
| 08:43:09 | <tomsmeding> | there is a significant jump from mostly-functional-with-a-bit-of-mutation to purely functional |
| 08:43:53 | <energizer> | isn't clojure purely functional? |
| 08:44:24 | <tomsmeding> | (I thought it used commonly used set! like lisps do, but I haven't actually used clojure, kuribas must answer this one) |
| 08:44:35 | <energizer> | i haven't either |
| 08:44:49 | <kuribas> | tomsmeding: they try to avoid mutation |
| 08:45:00 | <tomsmeding> | ah so it's better than most lisps |
| 08:45:02 | <tomsmeding> | "better" |
| 08:45:14 | <kuribas> | scheme as well. |
| 08:45:28 | <kuribas> | but common lisp is mostly imperative. |
| 08:46:08 | <kuribas> | IMO mutable in the large is worse than mutable in the small (mutating a function local variable). |
| 08:46:27 | <tomsmeding> | local mutation is not a problem, see ST |
| 08:46:50 | <kuribas> | Python in particular makes immutable hard, because it has frozen dataclasses, but no way to update a single variable. |
| 08:47:03 | <tomsmeding> | in fact I'd like a language that let me do local mutation without the ceremony that ST requires |
| 08:47:06 | → | avicenzi joins (~avicenzi@2a00:ca8:a1f:b004::c32) |
| 08:47:25 | <energizer> | aren't most languages like that? |
| 08:47:27 | <kuribas> | tomsmeding: you mean provable pure, right? |
| 08:47:40 | <tomsmeding> | in my wish language, yes |
| 08:48:04 | <tomsmeding> | that would probably need language support in the form of some additional syntax |
| 08:48:05 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
| 08:48:07 | <energizer> | are you allowed to mutate the arguments in wishlang? |
| 08:48:37 | <tomsmeding> | perhaps if we also have some form of linear types |
| 08:48:41 | <tomsmeding> | probably uniqueness types |
| 08:49:14 | <kuribas> | tomsmeding: I'd like polymorphic effects, like in flix https://flix.dev/ |
| 08:49:24 | <tomsmeding> | well, what do you mean with "mutate the arguments" |
| 08:49:46 | <tomsmeding> | that only presents problems when you mutate internals, and mutating internals is a thing that I'd need to watch out for anyway |
| 08:49:56 | <tomsmeding> | at least if you have lazy semantics, less so with strict semantics |
| 08:50:08 | <kuribas> | tomsmeding: hmm, I think flix allows local mutation. |
| 08:50:17 | <energizer> | this sounds like rust |
| 08:50:46 | <kuribas> | energizer: rust doesn't have purity annotations, does it? |
| 08:50:47 | <tomsmeding> | but then with like 10% of the boilerplate lol |
| 08:50:51 | <tomsmeding> | and that |
| 08:50:58 | <energizer> | if it's not `mut`, you're not mutating it |
| 08:51:00 | <tomsmeding> | I like haskell for its concise syntax |
| 08:51:15 | <Hecate> | oh hi tomsmeding o/ |
| 08:51:21 | <tomsmeding> | hello! |
| 08:51:33 | <Hecate> | kuribas: what I like in flix is the datalog :D |
| 08:52:57 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 08:53:15 | <dminuoso> | 09:43:53 energizer | isn't clojure purely functional? |
| 08:53:20 | <dminuoso> | What is that "purely functional" anyway? |
| 08:53:40 | <tomsmeding> | kuribas: I should look at Flix, sounds cool |
| 08:53:43 | <dminuoso> | I think in general there's different conflating ideas, some of them not well principled. |
| 08:53:59 | → | freeside joins (~mengwong@103.252.202.170) |
| 08:54:04 | <dminuoso> | And more to the point, I think `purely` and `functional` are orthoginal ideas. |
| 08:54:39 | <kuribas> | I think it typically means that functions don't perform side-effects. |
| 08:54:53 | <kuribas> | so clojure isn't "pure". |
| 08:55:33 | <dminuoso> | I think a more valuable notion lies in Haskell - i.e. distinguishing between evaluation and execution. |
| 08:55:45 | <dminuoso> | And that isnt directly linked to whatever "function" is or means |
| 08:56:17 | → | acidjnk joins (~acidjnk@p200300d6e715c47228ee5485b7272aa0.dip0.t-ipconnect.de) |
| 08:56:19 | <kuribas> | it does in the sense that a function always returns the same answer for the same inputs. |
| 08:56:20 | <dminuoso> | Because clealy we have the same notion of C routines that are effectful `putStrLn :: String -> IO ()` for instance |
| 08:56:34 | × | shriekingnoise_ quits (~shrieking@186.137.175.87) (Ping timeout: 260 seconds) |
| 08:57:20 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) (Remote host closed the connection) |
| 08:58:12 | <dminuoso> | kuribas: I think people focusing on that idea really mean to talk about referential transparencyu |
| 08:58:17 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
| 08:58:50 | <dminuoso> | Anyway |
| 08:59:01 | <dminuoso> | "purely functional" conflates "pure functions" with "functional" and I think its a bit silly |
| 08:59:13 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 08:59:25 | <energizer> | there are a whole bunch of things that pure means |
| 08:59:28 | → | bgs joins (~bgs@212-85-160-171.dynamic.telemach.net) |
| 08:59:44 | <energizer> | or, can |
| 09:00:37 | <dminuoso> | I think `pure` usually refers to functions being pure "deterministic output and lack of side effects", or expressions being pure (no non-pure functions being used in a given expression). Are there other notions? |
| 09:00:39 | <maerwald> | kuribas: what does "answer" mean? |
| 09:00:44 | <energizer> | "no side effects" seems like a stricter thing than "referentially transparent" |
| 09:02:16 | <energizer> | example, one take on "computational effects" breaks it down into various components https://bpa.st/QB4NG |
| 09:03:31 | → | nschoe joins (~q@141.101.51.197) |
| 09:03:45 | × | varoo quits (~varoo@122.161.91.19) (Read error: Connection reset by peer) |
| 09:04:05 | → | varoo joins (~varoo@122.161.91.19) |
| 09:05:04 | <Hecate> | I have no idea why we still use the terminology of "no side-effect" instead of "effect tracking" |
| 09:05:17 | <Hecate> | which seems closer to (my) reality (at least :p) |
| 09:05:37 | <dminuoso> | "effect tracking" is a bit of an exaggeration though |
| 09:06:06 | <dminuoso> | But sure, effect tracking - but that is done by separating evaluation from execution |
| 09:06:25 | <dminuoso> | Though it is ironic that in the underlying model execution happens *in* evaluation (that is we actually have an impure underlying language) |
| 09:06:48 | <dminuoso> | In the absence of unsafePerformIO, it is just an implementation detail however |
| 09:07:14 | <Hecate> | dminuoso: Certainly when you only have 'IO a' as a return type it's a bit obfuscated, but we can also have 'insertPackage :: (DB :> es) => Package -> Eff es ()' |
| 09:07:58 | <Hecate> | and tbh I have yet to see F#/C# get the same thing :D Instead they pass the implementation/handlers as function parameters |
| 09:08:12 | <dminuoso> | Hecate: Given that, enough extensions enabled, our type system is turing complete, then Haskell is anything that is expressiblie in a turing complete language. |
| 09:08:24 | <dminuoso> | Im not entirely sure whether being able to *model* it as a library is necessarily a property of the language |
| 09:10:10 | <Hecate> | dminuoso: no no don't derail the conversation, we were in the distinction between "no side-effect" and "tracking side-effects" :p |
| 09:10:22 | → | CiaoSen joins (~Jura@p200300c9573284002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 09:10:54 | <dminuoso> | Okay but then "we dont really track side-effects in the language", but rather "you could do it..." |
| 09:11:22 | <Hecate> | dminuoso: on my side it's the rigidity of the wording of "no side-effects" that bugs me |
| 09:12:08 | <Franciman> | would you prefer «no observable side-effects»? |
| 09:12:11 | <Hecate> | unless we really start from the basis that "side-effect" means "unchecked yet observable IO" |
| 09:12:45 | <Hecate> | yeah I guess should synchronise our watches here |
| 09:13:14 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 09:13:18 | <Hecate> | my usage (and understanding) of "side-effect" is that it is 1. observable and 2. in what we would customarily call "IO" |
| 09:13:39 | <Franciman> | a question: observable from who? And from where? |
| 09:13:53 | <Hecate> | from the user |
| 09:14:10 | <Hecate> | that's why FFI to C for addition is not necessarily relevant to be put in IO |
| 09:14:25 | <Hecate> | whereas FFI that can block a program's execution would be a more relevant candidate |
| 09:14:48 | <dminuoso> | Hecate: Its interesting, there is certainly notions that consider "side-effects" stuff that you cannot observe from within your domain. |
| 09:14:58 | <dminuoso> | (the term "side-effects" almost literally implies it even) |
| 09:16:07 | <Hecate> | dminuoso: yes! whereas people outside of Haskell seem to hear "no side-effect" and automatically reply "well if I can't perform side-effects what the fuck am I supposed to do with this language? add numbers until the heat death of the universe?" |
| 09:16:41 | <Hecate> | let's check Wikipedia |
| 09:16:53 | <Hecate> | > In computer science, an operation, function or expression is said to have a side effect if it modifies some state variable value(s) outside its local environment, which is to say if it has any observable effect other than its primary effect of returning a value to the invoker of the operation |
| 09:16:54 | <lambdabot> | <hint>:1:20: error: parse error on input ‘,’ |
| 09:17:07 | <Hecate> | bugger off lambdabot |
| 09:18:26 | <Hecate> | dminuoso: so I partly agree that it is "non-observable from within [a] domain" except that the domain of the user / outside world is the superset of all domains that can have effects escaping these domains unchecked :p |
| 09:18:45 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:18:46 | <Hecate> | here domain = local environment |
| 09:19:08 | <dminuoso> | What is local environment? |
| 09:19:40 | <Hecate> | dminuoso: isn't that the domain that you were talking about? |
| 09:19:47 | <Hecate> | or do you have another definition in mind? |
| 09:19:48 | <dminuoso> | Oh that domain |
| 09:19:48 | <[exa]> | Hecate: adding numbers produces a heat side effect btw :D |
| 09:19:57 | <Hecate> | [exa]: :3 |
| 09:20:18 | <dminuoso> | And adding numbers also allocates registers, using a value pollutes cache, alters timings |
| 09:20:30 | <dminuoso> | Using CPU time degrades system performance |
| 09:20:39 | <dminuoso> | So there's even non-hypothetical effects |
| 09:21:04 | <Hecate> | hence the concept of user-observability |
| 09:21:10 | <Hecate> | use 2 registers -> meh |
| 09:21:20 | <Hecate> | block the execution -> okay now that's a bit more visible |
| 09:21:20 | <dminuoso> | Maybe a good definition of `side-effects` would be that of syscalls. |
| 09:22:06 | <dminuoso> | Hecate: there's certainly code that is only correct under the assumption of certain timing properties - namely cryptographic code. |
| 09:22:28 | <Hecate> | dminuoso: and that's observable as shit yeah |
| 09:22:30 | <dminuoso> | So in that sense, even an extra register allocation from the register file can alter timings of code |
| 09:23:06 | <Hecate> | hmm |
| 09:23:11 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 09:23:13 | <Hecate> | dminuoso: have you read the article btw? |
| 09:23:15 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 09:23:19 | <Hecate> | https://en.wikipedia.org/wiki/Side_effect_(computer_science) |
| 09:23:27 | <Hecate> | temporality is talked about |
| 09:23:42 | <[exa]> | the discussion about purity seems completely skewed by the sole definition of purity being a negative (!∃) clause in an open world |
| 09:24:14 | → | akegalj joins (~akegalj@93-138-129-164.adsl.net.t-com.hr) |
| 09:24:15 | <dminuoso> | Hecate: Sure, I think one important part that is missing here is that purity has a tolerance level. |
| 09:24:29 | <dminuoso> | That is, purity is not just about altering state outside the local environment, but whether you care about that at all. |
| 09:24:40 | <dminuoso> | whether that is relevant for the correctness/meaning of your program |
| 09:25:06 | <[exa]> | ( ^ yep, you can't have purity without closing the world. ) |
| 09:25:34 | × | jespada_ quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 09:25:55 | <dminuoso> | which begs the question what "local environment" even means |
| 09:26:23 | <dminuoso> | Because if your program semantics depend upon it, isnt that part of its "environment" as well? |
| 09:26:38 | <Hecate> | it means pretty much what you need to mean to ensure that your model of purity & unchecked side-effects enabled you to write programs that are correct according to how you need them to be :P |
| 09:28:01 | <[exa]> | Hecate: that's the usual practice in programming everywhere (sometimes not wrt. purity but wrt. data consistency and other properties.) |
| 09:28:38 | <Hecate> | dminuoso: a vague, vague defintion of "local environment" is "the thing that holds your state" and then I'll refer you to idempotence :P |
| 09:28:52 | <[exa]> | you need to draw the line, and many people accept the usual line drawn (usually C-ish or math-ish) as the universal truth |
| 09:29:00 | <dminuoso> | Hecate: but clearly, if it "modifies other state" and you care about that state, then that "other state is part of your state as well" |
| 09:29:08 | <Hecate> | dminuoso: yep |
| 09:29:41 | <Hecate> | that being said I'm more in favour of bounded contexts |
| 09:30:17 | <Hecate> | and so you explicitly acknowledge boundaries between entities based on what they do, and not necessarily on what they depend on, in the sense of business operations |
| 09:30:22 | <Hecate> | (business as in domain) |
| 09:32:54 | <Hecate> | (come to my talk at FOSDEM if you want to learn more about bounded contexts) |
| 09:33:00 | <Hecate> | (#ad) |
| 09:33:09 | × | kuribas quits (~user@ptr-17d51emy7j9a6t4odfa.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 09:41:53 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 09:43:06 | → | jespada joins (~jespada@148.252.133.207) |
| 09:45:07 | × | danza quits (~francesco@151.35.92.17) (Read error: Connection reset by peer) |
| 09:45:11 | → | chele joins (~chele@user/chele) |
| 09:51:31 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 09:52:34 | → | malte joins (~malte@mal.tc) |
| 09:55:20 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 09:57:47 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) |
| 10:00:25 | → | freeside joins (~mengwong@103.252.202.170) |
| 10:02:30 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) (Ping timeout: 255 seconds) |
| 10:02:56 | → | danza joins (~francesco@151.53.27.222) |
| 10:04:43 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
| 10:08:00 | × | haritz quits (~hrtz@user/haritz) (Ping timeout: 248 seconds) |
| 10:09:02 | × | ft quits (~ft@p4fc2a257.dip0.t-ipconnect.de) (Quit: leaving) |
| 10:10:46 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:11:49 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds) |
| 10:20:16 | × | maerwald quits (~maerwald@mail.hasufell.de) (Changing host) |
| 10:20:16 | → | maerwald joins (~maerwald@user/maerwald) |
| 10:20:28 | <akegalj> | How come haskell has so much less security issues reported than other languages https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=Haskell ? Is it just that it is not used much in security contexts so nobody found problems ? |
| 10:21:10 | <akegalj> | (I mean, nobody was looking for the problems) |
| 10:22:38 | <merijn> | akegalj: I think 2 main things: 1) not a lot of user facing services, and 2) memory safety |
| 10:22:39 | <[_________]> | it's because Haskell is safe language. |
| 10:23:16 | <merijn> | akegalj: Google's Project Zero found that something, like 60% of CVEs relates to memory safety issues. So being memory safe by default rules out close to two-thirds of issues ;) |
| 10:23:44 | <maerwald> | akegalj: it's not used in security contexts |
| 10:24:26 | <maerwald> | and generally has less popular libraries/systems that are regularly screened |
| 10:24:46 | <[exa]> | the other 40% of the issues is traditionally input validation, which is also super easy to do right in haskell |
| 10:25:10 | × | talismanick quits (~talismani@2601:200:c181:4c40::1be2) (Ping timeout: 252 seconds) |
| 10:25:28 | <[exa]> | re security context, maybe hledger should count in there |
| 10:26:05 | <merijn> | I think the two main security issues with Haskell would be either 1) DOS attacks due to libraries not being battle-tested enough for that and 2) wildly unsafe crypto due to insufficient reviewing and laziness making constant time crypto computations hard |
| 10:26:25 | <maerwald> | oh, but we have types... it must be safe |
| 10:26:45 | <merijn> | [exa]: hledger is run on a local system, to exploit any bugs in hleder the user's system has to already be compromised |
| 10:26:59 | <merijn> | At which point you don't need bugs in hledger anymore |
| 10:27:10 | <[exa]> | ah true |
| 10:27:22 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 252 seconds) |
| 10:27:32 | <merijn> | And most famous Haskell things are like that |
| 10:28:17 | <merijn> | I guess bazqux and maybe shellcheck's website are the only big "public facing" Haskell services I know |
| 10:28:20 | <maerwald> | we have TUF implemented in Haskell... well, half-assed, that is |
| 10:28:28 | <maerwald> | not sure it has been reviewed |
| 10:28:34 | <maerwald> | hackage/cabal rely on it |
| 10:28:43 | <merijn> | maerwald: why half-assed? |
| 10:28:49 | <maerwald> | because it's tied to hackage |
| 10:28:54 | <[exa]> | "hackage relies on it" might count as a pretty tough review |
| 10:29:01 | <maerwald> | [exa]: no |
| 10:29:10 | <merijn> | [exa]: how so? |
| 10:29:24 | → | __monty__ joins (~toonn@user/toonn) |
| 10:29:38 | <maerwald> | merijn: https://github.com/haskell/hackage-security/issues/249 |
| 10:29:46 | <[exa]> | it's on internet and no one sploited it yet? |
| 10:29:56 | <maerwald> | [exa]: how do you know? |
| 10:30:10 | [exa] | starts feeling unsafe |
| 10:31:08 | <merijn> | maerwald: I mean, I don't think that makes the implementation half-assed. Not as useful as it could be, but "implemented half-assed" sounds like the actual code implementing it is of negligent quality |
| 10:31:30 | <maerwald> | yes, that is definitely half-assed |
| 10:31:41 | <maerwald> | TUF is a framework that you're supposed to implement as a library |
| 10:31:47 | <maerwald> | no idea what this is |
| 10:32:30 | <maerwald> | and I'm questioning whether you can have a clean implementation if it's NOT implemented as a library |
| 10:33:36 | × | jespada quits (~jespada@148.252.133.207) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 10:33:40 | <maerwald> | you can't even audit it properly that way |
| 10:38:28 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 10:39:31 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:40:14 | → | freeside joins (~mengwong@103.252.202.170) |
| 10:40:24 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 10:41:25 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 10:43:07 | <Profpatsch> | akegalj: The biggest issue you can expect from Haskell libraries is A) DDoS via space leaks and B) not a lot of eyes on some of the code, even sometimes very deep in the library stack |
| 10:43:39 | <Profpatsch> | This is mitigated somewhat by the fact that attackers usually don’t optimize for Haskell (unless it’s a targeted attack but then you have other problems) |
| 10:44:11 | <Profpatsch> | I’d expect Haskell crypto to hold up somewhat, due to the fact that nobody targets it |
| 10:44:12 | <razetime> | I'm trying to load a file into ghci from this project: https://github.com/diku-dk/futhark (src/Language/Futhark/Query.hs), but it complains that the imported modules are not in the search files. How do I tell it which modules to load? |
| 10:44:27 | <merijn> | Profpatsch: That's a DoS, not DDoS :p |
| 10:44:30 | <Profpatsch> | yes |
| 10:44:37 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
| 10:44:42 | <Profpatsch> | A single machine probably is enough to crash 80% of the Haskell webservices out there :P |
| 10:44:45 | <tomsmeding> | razetime: have you tried `cabal repl`? |
| 10:44:56 | <razetime> | i will try that |
| 10:45:14 | <tomsmeding> | razetime: `cabal repl` is the thing that starts ghci with all of the relevant modules in its search path |
| 10:45:28 | <merijn> | Profpatsch: Well, matter, that DDoS relies on distribution to run a target out of bandwidth. Exploiting a space leak to blow up memory consumption is just "denial of service" :p |
| 10:45:30 | <tomsmeding> | razetime: use `:m *Language.Futhark.Query` afterwards to switch focus into that module |
| 10:45:32 | <razetime> | i see, thanks. Will ask if I have any more doubts |
| 10:45:54 | <tomsmeding> | razetime: see also https://downloads.haskell.org/ghc/latest/docs/users_guide/ghci.html#ghci-module-cmd |
| 10:45:55 | <Profpatsch> | akegalj: don’t let that dissuade you though, Haskell is still one of the best languages for writing web services out there |
| 10:46:10 | <Profpatsch> | And issues are gonna be solved in time and with enough industry adoption |
| 10:46:29 | <Profpatsch> | It has a lot less bugs than anything nodejs I’d expect |
| 10:46:47 | × | razetime quits (~Thunderbi@117.193.5.58) (Read error: Connection reset by peer) |
| 10:47:01 | → | razetime joins (~Thunderbi@117.193.5.58) |
| 10:47:27 | <razetime> | sorry tomsmeding, cabal repl ate all my ram and crashed my computer :') |
| 10:47:36 | <razetime> | so it got disconnected |
| 10:47:38 | <tomsmeding> | 😂 |
| 10:47:43 | <tomsmeding> | wat |
| 10:48:01 | <razetime> | futhark build is pretty heavy on the resources, since it's a language compiler |
| 10:48:04 | <Profpatsch> | akegalj: For a recent security issue that has been found and fixed, look at the Aeson Map/KeyMap migration. |
| 10:48:11 | <tomsmeding> | razetime: ah right, might want to try `cabal build -j1` before |
| 10:48:33 | <tomsmeding> | the -j1 makes it use one parallel compiler unit only, which of course also reduces memory consumption |
| 10:48:52 | <razetime> | i already did a cabal build. it seems to be doing something different for cabal repl |
| 10:49:01 | <razetime> | does cabal repl -j1 work? |
| 10:49:24 | <razetime> | yeah it's in the help |
| 10:49:35 | <Profpatsch> | razetime: you migth want to set up https://profpatsch.de/notes/preventing-oom :) |
| 10:49:58 | <maerwald> | Profpatsch: fixed after years and pushing the maintainers to actually do it |
| 10:50:02 | <tomsmeding> | nah if you already built, then that -j1 is doing the wrong thing I think |
| 10:50:04 | <maerwald> | convincing them it's an actual problem |
| 10:50:14 | <maerwald> | it's embarrassing |
| 10:50:25 | <Profpatsch> | maerwald: well are they paid to do it? :) |
| 10:50:33 | <maerwald> | Idc |
| 10:50:41 | <Profpatsch> | e.g. random 1.2 only happened cause the people working on it were doing so fulltime |
| 10:50:57 | <razetime> | Profpatsch: neat, i'll install it |
| 10:51:00 | <Profpatsch> | It took some … mailing list drama to convince the maintainers to unblock |
| 10:51:06 | <Profpatsch> | but then it went through just fine |
| 10:51:10 | <maerwald> | Profpatsch: not sure I like the new random |
| 10:51:21 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 10:51:25 | <Profpatsch> | maerwald: maybe the interface is not the best, but you gotta work with what you got |
| 10:51:26 | <maerwald> | and I don't think resources were blocking the aeson fix |
| 10:51:30 | <maerwald> | more like attitude |
| 10:53:21 | <maerwald> | I have a lot of understanding for the "I'm an unpaid maintainer" lot... I'm one myself |
| 10:53:38 | <maerwald> | but when it's about security, I have low tolerance |
| 10:54:18 | <maerwald> | if you lack understanding, get out of the way... if you need resources to fix a security issue, speak up and inform the community |
| 10:54:28 | <Profpatsch> | agreed |
| 10:54:54 | <Profpatsch> | (I don’t mainain any critical infra in my spare time tho) |
| 10:57:10 | <Profpatsch> | Different topic; |
| 10:57:25 | <Profpatsch> | I have a [Foo] where each foo has a [Bar] |
| 10:57:38 | <Profpatsch> | And I want to do some batched I/O for all of the Bars |
| 10:57:56 | → | haritz joins (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
| 10:57:56 | × | haritz quits (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
| 10:57:56 | → | haritz joins (~hrtz@user/haritz) |
| 10:58:08 | <Profpatsch> | And the result should be a [Baz] where Baz is a Foo with the Bar replaced by the result of the batched IO |
| 10:58:24 | <Profpatsch> | But how do I do that while keeping track of which Bar belonged to which Foo |
| 10:58:53 | <akegalj> | Profpatsch: by no means I think haskell is bad, its my main tool for most problems. I was just wondering when I saw cve list why haskell isn't listed there. |
| 10:58:56 | <Profpatsch> | I guess I could just go via list indexes but that fees a bit meh |
| 10:59:19 | <tomsmeding> | Profpatsch: what structure can your "batched IO" procedure take |
| 10:59:35 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 11:00:03 | <Profpatsch> | tomsmeding: Well it just takes a list of Bars |
| 11:00:11 | <Profpatsch> | and returns a list of results |
| 11:00:15 | <tomsmeding> | Profpatsch: are Foo and Baz related by types somehow? Like Foo ~ Cheese Bar, Baz ~ Cheese ProcessedBar |
| 11:00:29 | → | xff0x joins (~xff0x@ai081074.d.east.v6connect.net) |
| 11:00:45 | <Profpatsch> | tomsmeding: I … could make it that way* |
| 11:00:54 | <Profpatsch> | But I don’t want to overcomplicate this hrm |
| 11:01:09 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 11:01:21 | <tomsmeding> | if so, then perhaps Cheese could be Traversable, and then your batched IO thing could take a Traversable instead of a list |
| 11:01:23 | <Profpatsch> | You know what, I think I’m gonna do an overapproximation, this code has to go away soon anyway |
| 11:01:33 | <tomsmeding> | you can make a list of traversables a traversable |
| 11:01:59 | <tomsmeding> | then modulo wrapping, the processing becomes `traverse process` :) |
| 11:02:21 | <tomsmeding> | uh, no, just `process`, sorry |
| 11:02:21 | <Profpatsch> | tomsmeding: My I/O has to serialize into a list anyway, since I’m contacting a database |
| 11:02:25 | <tomsmeding> | but that kind of thing |
| 11:02:28 | <tomsmeding> | ah |
| 11:02:30 | <Profpatsch> | so that just moves the problem into `process` :) |
| 11:03:50 | <tomsmeding> | I mean one could make an `f :: Traversable f => f a -> ([a], [b] -> f b)` |
| 11:04:08 | <tomsmeding> | no indices involved in f |
| 11:04:17 | × | haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb2 - https://znc.in) |
| 11:08:30 | → | haritz joins (~hrtz@82-69-11-11.dsl.in-addr.zen.co.uk) |
| 11:08:31 | × | haritz quits (~hrtz@82-69-11-11.dsl.in-addr.zen.co.uk) (Changing host) |
| 11:08:31 | → | haritz joins (~hrtz@user/haritz) |
| 11:08:32 | × | haritz quits (~hrtz@user/haritz) (Remote host closed the connection) |
| 11:10:11 | <jackdk> | Profpatsch: use a traversal to focus on all the `Bar`s across all the `Foo`s, use `partsOf` on it to turn it into a "lens" over lists? |
| 11:11:22 | → | haritz joins (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
| 11:11:22 | × | haritz quits (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
| 11:11:22 | → | haritz joins (~hrtz@user/haritz) |
| 11:11:23 | × | haritz quits (~hrtz@user/haritz) (Remote host closed the connection) |
| 11:11:27 | tomsmeding | suspects that my 'f' is basically partsOf |
| 11:11:32 | tomsmeding | doesn't know lenses |
| 11:11:54 | <Profpatsch> | jackdk: does it recover the structure even after >>=ing the resulting list through some IO? |
| 11:12:09 | <jackdk> | I'm noodling with a scratch buffer, standby |
| 11:12:34 | <Profpatsch> | We don’t use lens here, but this is intruiging nonetheless |
| 11:12:53 | <Profpatsch> | > Note: You should really try to maintain the invariant of the number of children in the list. |
| 11:12:55 | <lambdabot> | <hint>:1:55: error: parse error on input ‘of’ |
| 11:13:01 | <Profpatsch> | Ah, that would hint towards it |
| 11:13:16 | <tomsmeding> | Profpatsch: https://paste.tomsmeding.com/2DKZ49Cx |
| 11:13:37 | <tomsmeding> | oh ignore the tsilFromList, I don't use that |
| 11:14:43 | <tomsmeding> | using execState first and evalState afterwards certainly feels lensy |
| 11:16:44 | <Profpatsch> | Looks like partsOf really does the trick if your IO action retains the list length |
| 11:17:09 | → | haritz joins (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
| 11:17:10 | × | haritz quits (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
| 11:17:10 | → | haritz joins (~hrtz@user/haritz) |
| 11:18:21 | × | haritz quits (~hrtz@user/haritz) (Remote host closed the connection) |
| 11:18:47 | × | CiaoSen quits (~Jura@p200300c9573284002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 11:19:30 | <Profpatsch> | It seems to use https://twanvl.nl/blog/haskell/non-regular1 internally |
| 11:19:37 | <Profpatsch> | (The “Bazaar” thing) |
| 11:20:15 | <jackdk> | Profpatsch: Have to use unsafePartsOf because we are changing types: https://www.irccloud.com/pastebin/HgYfkiew/ReplaceTheBars.hs |
| 11:20:49 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 11:21:55 | <Profpatsch> | jackdk: p cool |
| 11:22:01 | <Axman6> | % :t partsOf template |
| 11:22:01 | <yahb2> | <interactive>:1:1: error: Variable not in scope: partsOf :: t0 -> t ; ; <interactive>:1:9: error: Variable not in scope: template |
| 11:22:18 | <Axman6> | % import Control.Lens |
| 11:22:18 | <yahb2> | <no location info>: error: ; Could not find module ‘Control.Lens’ ; It is not a module in the current program, or in any known package. |
| 11:22:20 | <tomsmeding> | sorry no lens :p |
| 11:22:24 | <tomsmeding> | only boot packages currently |
| 11:22:27 | <Axman6> | D: |
| 11:22:37 | <tomsmeding> | :t partsOf template |
| 11:22:39 | <lambdabot> | (Functor f, Data t, Typeable a) => LensLike f t t [a] [a] |
| 11:22:45 | <tomsmeding> | lambdabot got yo' back |
| 11:23:56 | <Axman6> | partsOf template is the magic incantation to find all the a's anywhere within a given t and let you mess with the |
| 11:24:00 | <Axman6> | m |
| 11:24:05 | <Axman6> | <3 tomsmeding |
| 11:26:08 | × | Guest75 quits (~Guest75@178.141.149.12) (Ping timeout: 260 seconds) |
| 11:27:39 | → | teo joins (~teo@user/teo) |
| 11:27:49 | <Profpatsch> | lens would be awesome if it weren’t so impossible to use in any team |
| 11:27:56 | <Profpatsch> | It’s a bit like call/cc |
| 11:28:14 | <Profpatsch> | okay in small doses, but def not in a codebase that should be maintainable |
| 11:28:29 | → | freeside joins (~mengwong@103.252.202.170) |
| 11:28:42 | <jackdk> | I don't understand the BazaarT stuff but I would seriously consider working out what unsafePartsOf is doing and reinventing that; if `Foo` is `Traversable` then your "optic" to find all the `a`s is `traverse . traverse`, you have `(&)` from `Data.Function` in `base`, and `(%%~) = id` |
| 11:29:25 | <Profpatsch> | jackdk: I think it boils down to what tomsmeding posted |
| 11:29:29 | <Profpatsch> | Just a lot more generalized |
| 11:30:52 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 11:30:57 | <jackdk> | Profpatsch: I think you're right; his `foo` function looks a lot like a deepified uniplate-esque thing |
| 11:31:21 | <Profpatsch> | the simplified type of Bazaar is (a -> f b) -> f t |
| 11:35:24 | <jackdk> | $WORK's solution to the lens thing is to a) not go too far beyond get/set and even fooOf functions unless you have a good reason, and b) get everyone to read Optics by Example |
| 11:35:58 | → | beteigeuze joins (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
| 11:36:19 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
| 11:40:59 | <tomsmeding> | Axman6: don't forget to |
| 11:41:00 | <tomsmeding> | @botsnack |
| 11:41:00 | <lambdabot> | :) |
| 11:41:17 | <k> | @botsnack |
| 11:41:18 | <lambdabot> | :) |
| 11:47:02 | <tomsmeding> | Profpatsch: I was overcomplicating things https://paste.tomsmeding.com/bfWxC3Dd |
| 11:49:55 | → | haritz joins (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
| 11:49:56 | × | haritz quits (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
| 11:49:56 | → | haritz joins (~hrtz@user/haritz) |
| 11:50:16 | → | gaff joins (~gaff@49.207.230.13) |
| 11:52:08 | <Profpatsch> | tomsmeding: Ah pretty cool, to unflatten the result you just pass the suffix of the list through the traversal |
| 11:52:11 | <Profpatsch> | Makes sense yeah! |
| 11:52:18 | <Profpatsch> | Super intuitive as well |
| 11:53:36 | <tomsmeding> | I've written code like this on specific data types before but only now realised that it can be generalised to any Traversable :) |
| 11:54:18 | <Profpatsch> | yeah super cool |
| 11:54:41 | <gaff> | i am using vim with haskell language server. on completions from imports, i see a pop up that shows the type and a link to the haddock html documentation, but i am not able to navigate to the documentation link in vim. is there any way this can be done? |
| 11:55:57 | <tomsmeding> | gaff: try typing 'gx' with the cursor on the url |
| 11:56:07 | <tomsmeding> | (source: https://stackoverflow.com/questions/9458294/open-url-under-cursor-in-vim-with-browser ) |
| 11:56:15 | <Profpatsch> | tomsmeding: jackdk now I also understand why you need unsafePartsOf, because partsOf will re-insert the original value if the result is not long enough |
| 11:56:22 | <Profpatsch> | so the types of the output and input have to be the same |
| 11:56:41 | <tomsmeding> | yeah I spotted that in the partsOf docs :) |
| 11:56:50 | <gaff> | https://mmhaskell.com/blog/2022/9/29/using-haskell-in-vim-the-basics has a screenshot of the typical autocomplete screen i see |
| 11:57:44 | <tomsmeding> | Profpatsch: so that 'unsafe' is precisely the 'error' in my code :) |
| 11:57:48 | <Profpatsch> | exactly |
| 11:57:59 | <gaff> | tomsmeding: the problem is that it is a pop up coming from coc-vim, and there is no way to navigate that pop up to reach the url |
| 11:58:08 | <tomsmeding> | ah |
| 11:58:20 | <tomsmeding> | (my nvim lsp client does have navigable popups) |
| 11:58:48 | <gaff> | tomsmeding: you use neo vim? |
| 11:59:04 | <tomsmeding> | sounds like something to bring up on the coc issue tracker as a feature request |
| 11:59:07 | <tomsmeding> | yeah |
| 11:59:12 | <gaff> | ok |
| 11:59:19 | <gaff> | i am using vim |
| 12:00:17 | <gaff> | well, i thought the haskell language server people who set this up may be knowing about it, because this pop up is something they created |
| 12:00:24 | <tomsmeding> | no |
| 12:00:30 | <tomsmeding> | the text in it is something they created |
| 12:00:41 | <tomsmeding> | the popup itself is how coc decides to display those messages |
| 12:00:53 | <gaff> | ok |
| 12:01:29 | × | Buliarous quits (~gypsydang@46.232.210.139) (Ping timeout: 260 seconds) |
| 12:03:01 | → | Buliarous joins (~gypsydang@46.232.210.139) |
| 12:05:34 | × | gaff quits (~gaff@49.207.230.13) (Ping timeout: 260 seconds) |
| 12:08:50 | → | gaff joins (~gaff@49.207.232.105) |
| 12:09:36 | × | elkcl quits (~elkcl@broadband-37-110-27-252.ip.moscow.rt.ru) (Remote host closed the connection) |
| 12:09:37 | → | freeside joins (~mengwong@103.252.202.170) |
| 12:10:01 | <gaff> | tomsmeding: sorry i got disconnected. question: in nvim, you are able to navigate to the link for the documentation and open it? |
| 12:10:46 | → | oldfashionedcow joins (~Rahul_San@user/oldfashionedcow) |
| 12:13:27 | → | jumper149 joins (~jumper149@base.felixspringer.xyz) |
| 12:14:05 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 260 seconds) |
| 12:15:24 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:31:46 | × | gaff quits (~gaff@49.207.232.105) (Quit: Bye ...) |
| 12:37:45 | <tomsmeding> | @tell gaff Yes but that's because my nvim lsp client allows changing focus to the popup and treating it as a read-only buffer |
| 12:37:45 | <lambdabot> | Consider it noted. |
| 12:38:56 | × | razetime quits (~Thunderbi@117.193.5.58) (Remote host closed the connection) |
| 12:43:07 | → | freeside joins (~mengwong@103.252.202.170) |
| 12:44:08 | × | califax quits (~califax@user/califx) (Ping timeout: 255 seconds) |
| 12:46:45 | → | califax joins (~califax@user/califx) |
| 12:47:27 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 248 seconds) |
| 12:50:04 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:53:12 | × | akegalj quits (~akegalj@93-138-129-164.adsl.net.t-com.hr) (Quit: leaving) |
| 13:03:56 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Read error: Connection reset by peer) |
| 13:07:37 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 13:09:02 | → | CiaoSen joins (~Jura@p200300c9573284002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 13:09:21 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 13:09:50 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 13:14:06 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 13:14:08 | × | troydm quits (~troydm@user/troydm) (Ping timeout: 248 seconds) |
| 13:14:57 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:8095:1260:6fef:5d26) (Ping timeout: 252 seconds) |
| 13:15:43 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 13:16:07 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 13:17:12 | → | tremon joins (~tremon@83-85-213-108.cable.dynamic.v4.ziggo.nl) |
| 13:30:25 | → | Guest86 joins (~Guest86@2001:16a2:4222:d000:2df4:2526:36aa:1e0d) |
| 13:31:21 | × | Guest86 quits (~Guest86@2001:16a2:4222:d000:2df4:2526:36aa:1e0d) (Client Quit) |
| 13:37:05 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:40:59 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 252 seconds) |
| 13:43:04 | → | jero98772 joins (~jero98772@2800:484:1d80:d8ce:9815:cfda:3661:17bb) |
| 13:45:20 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 13:59:28 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 14:03:49 | → | akegalj joins (~akegalj@222-217.dsl.iskon.hr) |
| 14:06:44 | → | thegeekinside joins (~thegeekin@189.180.66.244) |
| 14:11:09 | → | thongpv joins (~thongpv87@14.179.159.25) |
| 14:11:45 | × | thongpv quits (~thongpv87@14.179.159.25) (Remote host closed the connection) |
| 14:12:28 | → | thongpv joins (~thongpv87@14.179.159.25) |
| 14:13:12 | × | thongpv quits (~thongpv87@14.179.159.25) (Remote host closed the connection) |
| 14:14:14 | → | thongpv joins (~thongpv87@14.179.159.25) |
| 14:14:33 | → | kurbus joins (~kurbus@user/kurbus) |
| 14:15:03 | × | thongpv quits (~thongpv87@14.179.159.25) (Remote host closed the connection) |
| 14:15:28 | → | thongpv joins (~thongpv87@14.179.159.25) |
| 14:16:26 | × | thongpv quits (~thongpv87@14.179.159.25) (Remote host closed the connection) |
| 14:18:24 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:6f34:bf9c:ac6f:4344) |
| 14:21:08 | × | kurbus quits (~kurbus@user/kurbus) (Ping timeout: 260 seconds) |
| 14:25:37 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 14:26:45 | → | kurbus joins (~kurbus@user/kurbus) |
| 14:27:35 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 14:32:13 | → | thongpv joins (~thongpv87@2402:9d80:3f4:1510:9f76:2d33:c304:1848) |
| 14:32:14 | <yin> | tomsmeding: is there a keybinding to focus navigation on the popup? i think i do it by keeping `K` pressed but am not sure if that's intended behaviour |
| 14:35:57 | × | cheesecake quits (~cheesecak@2600:6c4a:7c7f:ec9b:9cb2:b42f:48ab:b49b) (Quit: Client closed) |
| 14:39:12 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 14:48:47 | × | Angelz quits (Angelz@user/angelz) (Ping timeout: 264 seconds) |
| 14:51:33 | → | Hammdist joins (~Hammdist@67.169.114.135) |
| 14:51:38 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 14:52:19 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 14:52:48 | <Hammdist> | I'm trying to write a program that interfaces with GHC library. To get a Var name, I figure I have to case on Id in the https://hackage.haskell.org/package/ghc-9.4.4/docs/src/GHC.Types.Var.html#Var type. However I get Not in scope: data constructor ‘Id’. any ideas? |
| 14:53:23 | <Hammdist> | I have tried import GHC.Types.Var but it didn't fix anything |
| 14:54:50 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:55:20 | <lortabac> | Hammdist: IIRC the constructors are not exported but you can use 'varName' |
| 14:55:34 | <lortabac> | https://hackage.haskell.org/package/ghc-9.4.4/docs/GHC-Types-Var.html#v:varName |
| 14:57:15 | <Hammdist> | ah thanks -- will give that a go |
| 14:59:02 | × | thongpv quits (~thongpv87@2402:9d80:3f4:1510:9f76:2d33:c304:1848) (Ping timeout: 255 seconds) |
| 14:59:55 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 256 seconds) |
| 15:01:20 | × | CiaoSen quits (~Jura@p200300c9573284002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 15:01:58 | × | kurbus quits (~kurbus@user/kurbus) (Ping timeout: 260 seconds) |
| 15:02:06 | → | rekahsoft joins (~rekahsoft@bras-base-orllon1122w-grc-05-174-88-194-86.dsl.bell.ca) |
| 15:02:09 | × | rekahsoft quits (~rekahsoft@bras-base-orllon1122w-grc-05-174-88-194-86.dsl.bell.ca) (Remote host closed the connection) |
| 15:02:53 | → | rekahsoft joins (~rekahsoft@bras-base-orllon1122w-grc-05-174-88-194-86.dsl.bell.ca) |
| 15:04:37 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 15:06:20 | <segfaultfizzbuzz> | is there a list of the "characteristics of code" somewhere? for example, code may have: memory safety, totality, bounds checking/correctness, -- i would like to continue or "complete" this list |
| 15:10:44 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 15:11:42 | → | merijn joins (~merijn@86.86.29.250) |
| 15:13:10 | <Hammdist> | memory safety isn't a property of code, it's a property of the programming language |
| 15:13:21 | → | kurbus joins (~kurbus@user/kurbus) |
| 15:13:28 | <Hammdist> | correctness is a property of the code |
| 15:13:41 | <segfaultfizzbuzz> | or should we say it is a property of the binary which gets generated...? |
| 15:14:28 | <Hammdist> | it would be hard to define memory safety for a binary. a correct binary could do a lot of dodgy things that are perfectly safe in its context |
| 15:14:32 | <segfaultfizzbuzz> | presumably unless the programming language is "stiff" there will always be a way to say "this function can do unsafe things" |
| 15:15:00 | → | CiaoSen joins (~Jura@p200300c9573284002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 15:15:24 | <segfaultfizzbuzz> | so the real criteria here would be something like "program written in lang X without using unsafe" |
| 15:16:11 | <segfaultfizzbuzz> | i think languages are/can be designed to enforce characteristics of code, so there will probably always be an overlap here |
| 15:16:19 | × | merijn quits (~merijn@86.86.29.250) (Ping timeout: 252 seconds) |
| 15:16:45 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 15:16:48 | → | Angelz joins (Angelz@Angelz.oddprotocol.org) |
| 15:16:55 | <segfaultfizzbuzz> | probably what happens is someone writes code in some language, people run into lots of bugs, and finally someone gets pissed off and promotes that bug type into some kind of formal invariant which can be enforced at the language level |
| 15:17:53 | <segfaultfizzbuzz> | for example languages don't have "choice of unit (e.g. meters kilometers etc) declaration/safety" today, but it would be reasonable to require such a thing |
| 15:24:08 | × | kurbus quits (~kurbus@user/kurbus) (Ping timeout: 260 seconds) |
| 15:30:11 | <kuribas> | Hammdist: "correctness" doesn't exist. |
| 15:30:15 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 15:30:33 | <kuribas> | It's a meaningless word that people like throwing around. |
| 15:30:39 | <segfaultfizzbuzz> | kuribas: right, but we can list desirable characteristics |
| 15:31:03 | <segfaultfizzbuzz> | and perhaps we can say that if we choose good and sufficiently orthogonal characteristics then then program is likely to be better as it meets more of the characteristics |
| 15:31:43 | <kuribas> | segfaultfizzbuzz: a much more meaningful term is "consistency". I'd like my program to be consistent. |
| 15:32:06 | <segfaultfizzbuzz> | well these things, whatever they are called, are externally enforced i think? |
| 15:32:24 | <kuribas> | you mean by tooling? |
| 15:32:39 | <kuribas> | Tooling can verify these properties. |
| 15:32:47 | <segfaultfizzbuzz> | language, tooling, abstract constructs, rules, and maybe heuristics of programming which are not enforced today |
| 15:33:25 | <kuribas> | A program can be consistent in a dynamic language, but it is going to be hard to verify the claim. |
| 15:33:41 | <segfaultfizzbuzz> | can you define consistency? |
| 15:34:06 | <segfaultfizzbuzz> | the term doesn't look right to me because consistency is something which, in my mind, ought to be detectable (such as by the program itself) |
| 15:34:29 | <segfaultfizzbuzz> | but i am interested in all characteristics, including characteristics which the program itself can't know to enforce |
| 15:34:56 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 15:35:22 | <akegalj> | I would like to test function `foo :: IO ()` which reads some input from stdin and outputs somthing to stdout. How to do this simply ? Is there some wrapper `run :: [Text] -> IO Text` that will echo some Text to foo and return stdout back. I see shelly package can be used to model such behaviour, but I wonder is there something simpler maybe in base to use to achieve this? |
| 15:35:47 | <earthy> | segfaultfizzbuzz: you may want to look at F#, which does have units of measure, or Frinklang which is built around the concept of physically correct units. Furthermore, you may want to look into dependently typed programming languages such as Idris |
| 15:35:52 | <geekosaur> | the program can't ensure self-consistency because it can't know the problem it's solving and therefore what counts as consistent within the bounds of that problem. this is one reason external tests exist |
| 15:36:30 | <kuribas> | segfaultfizzbuzz: it means different parts of the program have the same notions of data or behaviour. |
| 15:36:50 | <geekosaur> | this is also why typeclasses in Haskell don';t have built-in consistency checks; you need a stronger language such as Idris to express them |
| 15:37:04 | <segfaultfizzbuzz> | earthy: these are relevant but don't directly address the question,... dependent typing i think is a method/capability for enforcing code invariants at compile time but does not itself describe what should be enforced |
| 15:37:33 | <earthy> | and there's Eiffel as well, with its contracts. |
| 15:37:35 | <segfaultfizzbuzz> | geekosaur: re: can't ensure self-consistency, right |
| 15:37:47 | <geekosaur> | segfaultfizzbuzz, it can express invariants in the type system that a language like Haskell or especially Python can't |
| 15:37:58 | <segfaultfizzbuzz> | yes i understand that |
| 15:38:12 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 15:38:20 | <segfaultfizzbuzz> | but my question is what are (typically fairly universal) desirable invariants |
| 15:38:30 | <earthy> | segfaultfizzbuzz: then I think you must be clearer as to what you try to state; I do not think I understand |
| 15:38:32 | <kuribas> | segfaultfizzbuzz: I think he means encoding laws in the typeclass. |
| 15:38:44 | <segfaultfizzbuzz> | i can repeat my question: |
| 15:38:51 | <geekosaur> | again, many of them aren't universal, they;re defined by the problem the program is intended to solve |
| 15:39:19 | <earthy> | not even garbage collection is universally beneficial |
| 15:39:44 | <segfaultfizzbuzz> | well if you were driving a car which had its system software proven to be memory safe, you would be happier and more relaxed than if it was not, right? |
| 15:40:00 | <earthy> | (for e.g. certain classes of hard real time systems you may want purely statically allocated memory) |
| 15:40:10 | <segfaultfizzbuzz> | right |
| 15:40:11 | <[exa]> | segfaultfizzbuzz: what a relief they now make the cars in javascript! :] |
| 15:40:13 | <jean-paul[m]> | That's not universal, though. That's control software for a car. That's very, very specific. |
| 15:40:27 | <segfaultfizzbuzz> | [exa]: seriously lol but that's just the ui frontend junk i am pretty sure |
| 15:40:31 | <earthy> | hell, one of my cars runs windows :D |
| 15:41:03 | <segfaultfizzbuzz> | jean-paul[m]: ok so are you saying that the desired characteristics of code are always highly context dependent? |
| 15:41:06 | <earthy> | and yeah, just in the 'media/telephone' junk :) |
| 15:41:06 | <[exa]> | segfaultfizzbuzz: I'd say frontend includes the steering wheel. |
| 15:41:39 | <jean-paul[m]> | segfaultfizzbuzz: I don't think you can separate "desire" from a context, right. |
| 15:41:43 | <segfaultfizzbuzz> | maybe my car example is too strong of a context |
| 15:41:53 | <earthy> | I think it may be worthwhile to think about what kinds of guarantees you'd like from your code and get most of them with little work |
| 15:42:10 | <earthy> | static typing is one way of getting guarantees |
| 15:42:17 | <earthy> | garbage collection another |
| 15:42:45 | <segfaultfizzbuzz> | right but *purpose* of garbage collection is to provide memory safety (or, memory safety while limiting programmer effort/likelihood of doing it wrong) |
| 15:42:57 | → | freeside joins (~mengwong@103.252.202.170) |
| 15:43:12 | → | kurbus joins (~kurbus@user/kurbus) |
| 15:43:39 | <segfaultfizzbuzz> | and so my interest is the *purpose*, the *desirable characteristic* (eg memory safety) rather than the *method to accomplish the characteristic* (garbage collection, dynamic types etc) |
| 15:44:04 | <segfaultfizzbuzz> | and the question would be what is a reasonably good list of these desirable charcteristics |
| 15:45:14 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 15:45:14 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 15:45:18 | allbery_b | is now known as geekosaur |
| 15:46:07 | <stefan-_> | purity of (a part of) the program is a nice property |
| 15:46:24 | <kuribas> | segfaultfizzbuzz: I find referential transparency one of the most important properties. |
| 15:46:42 | <kuribas> | Because it means you can understand a part of the program without the need to understand the whole. |
| 15:47:03 | <kuribas> | which is something that clojure is missing, despite trying hard to be functional. |
| 15:47:07 | <segfaultfizzbuzz> | ha |
| 15:47:46 | <kuribas> | Not being referential transparent means you need to understand a lot to make a small change. Also you need to understand the consequences of that change. |
| 15:47:59 | <segfaultfizzbuzz> | another example i only partially understand might be "algebraicity"--for example, using floating point can destroy associativity |
| 15:48:50 | <earthy> | segfaultfizzbuzz: you're getting way into what cross-functional requirements do I want to achieve - territory |
| 15:49:14 | <segfaultfizzbuzz> | earthy: i would say don't think about actually writing code, think about this stuff like a wish list |
| 15:49:31 | <jean-paul[m]> | Referential transparency and algebraicity support the same thing - breaking a problem down so you can solve it in tiny pieces. So, "composability". |
| 15:49:56 | <segfaultfizzbuzz> | sure |
| 15:49:59 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 268 seconds) |
| 15:54:24 | × | kurbus quits (~kurbus@user/kurbus) (Quit: Client closed) |
| 15:55:16 | <stefan-_> | another useful property is immutability of data structures |
| 15:55:35 | <segfaultfizzbuzz> | sure, (which might be part of referential transparency...) |
| 15:56:10 | <earthy> | then again, mutability is very powerful for performance... |
| 15:56:48 | <kuribas> | earthy: err, I contest that, unless you are in a tight inner loop. |
| 15:57:01 | <earthy> | that's the problem really, these things are almost always 'it depends' |
| 15:57:35 | <earthy> | kuribas: oh, I prefer my data to be immutable in general, and there's performance gains to be had that way as well |
| 15:58:03 | <segfaultfizzbuzz> | performance characteristics are valid characteristics of a program but i am trying to keep them independent as a consideration |
| 15:58:19 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 15:58:44 | <segfaultfizzbuzz> | earthy: probably what you mean to say is that "i am willing to sacrifice correctness for speed" which is probably true more often than we would like to admit |
| 15:58:49 | <kuribas> | earthy: after a long list of considerations, it may have an impact. But often it's the first thing people mention when talking about FP. |
| 15:59:52 | → | raehik joins (~raehik@82.21.176.157) |
| 15:59:53 | × | califax quits (~califax@user/califx) (Ping timeout: 255 seconds) |
| 16:00:07 | × | jinsun_ quits (~jinsun@user/jinsun) (Quit: You have been kicked for being idle) |
| 16:00:38 | <segfaultfizzbuzz> | one thing i'm not sure about is whether "linearity" is a desirable characteristic in many situations,... i kind of think it is |
| 16:00:41 | → | jinsun_ joins (~jinsun@user/jinsun) |
| 16:00:49 | <segfaultfizzbuzz> | because linearity helps guarantee the absence of resource leaks |
| 16:02:03 | → | califax joins (~califax@user/califx) |
| 16:02:10 | → | merijn joins (~merijn@86.86.29.250) |
| 16:02:21 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) |
| 16:02:35 | <earthy> | but the purpose is 'no resource leaks' then, isn't it? |
| 16:03:12 | <segfaultfizzbuzz> | earthy: sure, |
| 16:03:29 | <segfaultfizzbuzz> | i am mentioning the method of achieving the characteristic in passing |
| 16:03:51 | <earthy> | which Erlang provides with process trees and let-it-crash |
| 16:04:33 | <segfaultfizzbuzz> | earthy: does it though? i'm assuming crashing comes from some kind of process memory size limit, but you could probably open a zillion files or ports in that limit |
| 16:04:44 | → | nerdypepper joins (~nerdypepp@user/nerdypepper) |
| 16:05:13 | <earthy> | which then get cleaned up by the process reaper |
| 16:05:15 | ← | jinsun_ parts (~jinsun@user/jinsun) () |
| 16:05:31 | <segfaultfizzbuzz> | ok i am not terribly familiar with erlang |
| 16:06:38 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) (Ping timeout: 246 seconds) |
| 16:10:07 | × | kenran` quits (~user@user/kenran) (Remote host closed the connection) |
| 16:14:29 | → | freeside joins (~mengwong@103.252.202.170) |
| 16:14:38 | <segfaultfizzbuzz> | how does the process reaper know it can kill stuff? |
| 16:14:59 | × | oldfashionedcow quits (~Rahul_San@user/oldfashionedcow) (Quit: WeeChat 3.8) |
| 16:15:00 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:6f34:bf9c:ac6f:4344) (Quit: WeeChat 2.8) |
| 16:16:30 | → | oldfashionedcow joins (~Rahul_San@user/oldfashionedcow) |
| 16:17:15 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 16:18:05 | × | dsrt^ quits (~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 16:18:40 | <earthy> | it doesn't. it just kills stuff. :D |
| 16:18:46 | <segfaultfizzbuzz> | hahaha |
| 16:19:10 | <waleee> | looks like the scheduler does some checks with various signal messages, https://www.erlang.org/doc/reference_manual/processes.html#receiving-signals |
| 16:19:31 | <earthy> | but honestly the entire concept of supervision trees and programming the resource behaviour separately from the worker processes is neat and not directly linearized |
| 16:22:35 | <segfaultfizzbuzz> | needing to be able to exit the process under supervision at any time makes me nervous |
| 16:27:23 | × | FragByte quits (~christian@user/fragbyte) (Quit: Quit) |
| 16:27:33 | → | FragByte joins (~christian@user/fragbyte) |
| 16:34:54 | <Hammdist> | how do I convert a ByteString to a String? |
| 16:35:12 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Remote host closed the connection) |
| 16:36:37 | × | merijn quits (~merijn@86.86.29.250) (Ping timeout: 252 seconds) |
| 16:38:27 | × | raehik quits (~raehik@82.21.176.157) (Ping timeout: 252 seconds) |
| 16:38:50 | <geekosaur> | Data.ByteString.Char8.unpack? |
| 16:39:14 | <geekosaur> | (going that direction is safe; the other direction truncates) |
| 16:39:29 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 16:39:44 | × | beteigeuze quits (~Thunderbi@bl14-81-220.dsl.telepac.pt) (Quit: beteigeuze) |
| 16:40:12 | → | beteigeuze joins (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
| 16:42:10 | × | beteigeuze quits (~Thunderbi@bl14-81-220.dsl.telepac.pt) (Client Quit) |
| 16:42:33 | → | troydm joins (~troydm@user/troydm) |
| 16:42:37 | → | beteigeuze joins (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
| 16:43:12 | <Hammdist> | in this definition of a case expression: | Case (Expr b) b Type [Alt b] <-- what is the second b for? |
| 16:44:20 | → | kurbus joins (~kurbus@user/kurbus) |
| 16:44:46 | <[exa]> | Hammdist: where is that from? AST parameters typically mean either extra info (such as location) or binders type (such as variable IDs) |
| 16:45:06 | <Hammdist> | it's from https://hackage.haskell.org/package/ghc-9.4.4/docs/src/GHC.Core.html#Expr |
| 16:45:56 | <Hammdist> | I don't see any AST information on the other cases |
| 16:46:18 | <[exa]> | you can see e.g. that Lam has the `b` (that's the variable that's being bound) |
| 16:46:40 | <Hammdist> | sure but all the bindings in a case are in the alternatives |
| 16:46:51 | <geekosaur> | not true of case in core |
| 16:47:05 | <geekosaur> | core also binds the result of evaluating the expression |
| 16:47:17 | <[exa]> | it says up there: The binder gets bound to the value of the scrutinee, and the Expr must be that of all the case alternatives |
| 16:47:28 | <[exa]> | `b` is that binder. |
| 16:47:50 | <[exa]> | I'm not sure if this has a direct representation in "normal" haskell |
| 16:48:01 | <geekosaur> | it doesn't |
| 16:48:44 | <Hammdist> | so I must translate it as implying a let binding then |
| 16:49:01 | <Hammdist> | let x = expr in case x of ... |
| 16:49:11 | <Hammdist> | as x may appear in ...? |
| 16:49:41 | <geekosaur> | let !x = expr in … |
| 16:49:47 | <geekosaur> | case is strict, let is lazy |
| 16:50:28 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 16:50:55 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 260 seconds) |
| 16:51:03 | × | kurbus quits (~kurbus@user/kurbus) (Ping timeout: 260 seconds) |
| 16:51:56 | glguy_ | is now known as glguy |
| 16:55:29 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 260 seconds) |
| 16:59:43 | × | beteigeuze quits (~Thunderbi@bl14-81-220.dsl.telepac.pt) (Ping timeout: 252 seconds) |
| 16:59:56 | → | econo joins (uid147250@user/econo) |
| 17:07:31 | → | beteigeuze joins (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
| 17:10:25 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 260 seconds) |
| 17:13:49 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 17:18:04 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 17:22:09 | × | teo quits (~teo@user/teo) (Ping timeout: 256 seconds) |
| 17:23:19 | → | werneta joins (~werneta@137.79.207.195) |
| 17:23:43 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 268 seconds) |
| 17:26:45 | × | ddellacosta quits (~ddellacos@143.244.47.83) (Ping timeout: 260 seconds) |
| 17:27:30 | → | kurbus joins (~kurbus@user/kurbus) |
| 17:30:11 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:31:03 | × | CiaoSen quits (~Jura@p200300c9573284002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 17:31:24 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 17:53:02 | × | nschoe quits (~q@141.101.51.197) (Quit: Switching off) |
| 17:53:05 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 17:54:23 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 17:55:35 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) (Remote host closed the connection) |
| 17:55:55 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 17:57:57 | × | zeenk quits (~zeenk@2a02:2f04:a014:8700::7fe) (Quit: Konversation terminated!) |
| 17:58:45 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 252 seconds) |
| 18:05:59 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 18:08:09 | → | talismanick joins (~talismani@2601:200:c181:4c40::1be2) |
| 18:08:22 | × | talismanick quits (~talismani@2601:200:c181:4c40::1be2) (Client Quit) |
| 18:18:40 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 18:21:58 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 18:36:03 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 18:36:39 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 18:39:00 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) |
| 18:39:33 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 18:40:35 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 18:42:42 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 18:43:36 | × | trev quits (~trev@user/trev) (Remote host closed the connection) |
| 18:49:34 | → | opticblast joins (~Thunderbi@172.58.84.5) |
| 18:51:58 | → | slack1256 joins (~slack1256@181.42.52.81) |
| 18:53:38 | → | turlando joins (~turlando@user/turlando) |
| 18:57:02 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 246 seconds) |
| 19:00:21 | × | opticblast quits (~Thunderbi@172.58.84.5) (Ping timeout: 252 seconds) |
| 19:00:43 | × | freeside quits (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
| 19:01:37 | → | bilegeek joins (~bilegeek@2600:1008:b0a9:5822:3cbe:e760:543a:34cb) |
| 19:07:44 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:11:12 | × | haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb2 - https://znc.in) |
| 19:13:10 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 19:14:01 | → | haritz joins (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
| 19:14:01 | × | haritz quits (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
| 19:14:01 | → | haritz joins (~hrtz@user/haritz) |
| 19:16:37 | → | ddellacosta joins (~ddellacos@static-198-44-136-174.cust.tzulo.com) |
| 19:17:20 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 248 seconds) |
| 19:19:19 | → | mechap joins (~mechap@user/mechap) |
| 19:20:32 | × | beteigeuze quits (~Thunderbi@bl14-81-220.dsl.telepac.pt) (Ping timeout: 248 seconds) |
| 19:22:34 | → | beteigeuze joins (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
| 19:25:50 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) (Remote host closed the connection) |
| 19:27:07 | × | beteigeuze quits (~Thunderbi@bl14-81-220.dsl.telepac.pt) (Ping timeout: 252 seconds) |
| 19:28:12 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 19:28:35 | → | bontaq joins (~user@ool-45779fe5.dyn.optonline.net) |
| 19:32:59 | × | ddellacosta quits (~ddellacos@static-198-44-136-174.cust.tzulo.com) (Ping timeout: 252 seconds) |
| 19:33:59 | → | freeside joins (~mengwong@103.252.202.170) |
| 19:35:28 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 248 seconds) |
| 19:41:20 | → | kenran joins (~user@user/kenran) |
| 19:42:29 | × | bgs quits (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
| 19:43:56 | × | oldfashionedcow quits (~Rahul_San@user/oldfashionedcow) (Quit: WeeChat 3.8) |
| 19:44:26 | → | oldfashionedcow joins (~Rahul_San@user/oldfashionedcow) |
| 19:45:24 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 19:46:33 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 19:48:26 | <tomsmeding> | yin: indeed if you press K twice you end up in the popup; whether that's intended behaviour no clue, but it works :) |
| 19:49:55 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
| 19:50:40 | → | cheater_ joins (~Username@user/cheater) |
| 19:50:57 | → | ft joins (~ft@p4fc2a257.dip0.t-ipconnect.de) |
| 19:51:50 | → | PepsiLepreux joins (~pepsi@iron.vengarl.com) |
| 19:52:32 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 19:52:35 | cheater_ | is now known as cheater |
| 19:56:39 | <yin> | where can i learn about the differences between Haskell2010 and GHC2021 ? |
| 19:56:52 | → | MasseR46 joins (~MasseR@2001:bc8:47a0:1521::1) |
| 19:57:35 | <yin> | tomsmeding: yeah, it kind of feels buggy but i do it on purpose often |
| 19:57:52 | → | haasn` joins (~nand@haasn.dev) |
| 19:59:17 | <yushyin> | yin: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/control.html#controlling-extensions |
| 20:01:27 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 20:03:06 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 20:03:26 | kurbus | is now known as test123 |
| 20:03:30 | test123 | is now known as kurbus |
| 20:04:28 | <yin> | ty |
| 20:04:37 | <mauke> | what is DoAndIfThenElse? |
| 20:06:01 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
| 20:07:00 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 20:09:21 | <mniip> | mauke, whether a ";" is allowed before an "else" in an if-then-else |
| 20:09:36 | × | Lears quits (~Leary]@user/Leary/x-0910699) (Remote host closed the connection) |
| 20:09:49 | <mniip> | so that inside a do-block, the if and the else could have the same indentation level (thus inserting a semicolon inbetween) |
| 20:09:57 | → | [Leary] joins (~Leary]@user/Leary/x-0910699) |
| 20:12:13 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) |
| 20:12:13 | × | oldfashionedcow quits (~Rahul_San@user/oldfashionedcow) (Quit: WeeChat 3.8) |
| 20:12:36 | → | oldfashionedcow joins (~Rahul_San@user/oldfashionedcow) |
| 20:13:17 | <segfaultfizzbuzz> | why does the SQL "type system" diverge from the haskell "type system" (or that of other good languages, maybe rust)? |
| 20:13:58 | <segfaultfizzbuzz> | for instance i don't think (?) SQL has algebraic data types, and SQL allows you to make types nullable |
| 20:14:43 | <geekosaur> | because SQL started out as IBM's SEQUEL II, and was designed for the type systems of COBOL and PL/I |
| 20:14:54 | <geekosaur> | in particular this is why numeric types work the way they do |
| 20:15:11 | <segfaultfizzbuzz> | wow that's a real answer |
| 20:15:42 | <segfaultfizzbuzz> | lol so an ORM is really a cobol compatibility layer? lol |
| 20:16:16 | <segfaultfizzbuzz> | so why not drop concrete on sql and greenfield stuff? |
| 20:16:20 | <darkling> | IIRC, the NULL also has a purpose in relational algebra (of which SQL is a poor and mangled implementation). |
| 20:17:09 | <dsal> | SEQUEL II - The Sequel Sequel. |
| 20:17:16 | <segfaultfizzbuzz> | sequel ii - the second one |
| 20:17:40 | <kurbus> | sequel ii is also called just 3 |
| 20:18:01 | <dsal> | We use persistent which is kind of neat, but also kind of annoying. |
| 20:18:05 | <darkling> | ORMs aren't about the COBOL -- they're about trying to map the general structures to each other. You'd have the same problems trying to map anything similarly based on relational algebra into anything using objects. |
| 20:18:15 | <monochrom> | In fact since SQL predates Haskell and Rust, I would say that Haskell and Rust diverged from SQL's type system. >:) |
| 20:18:35 | <darkling> | OO ideas probably map much more cleanly onto CODASYL-like things... |
| 20:19:04 | <geekosaur> | some of us still wish C. J. Date's QUEL had won out over SEQUEL |
| 20:19:22 | <geekosaur> | (see original Ingres) |
| 20:19:34 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 20:19:35 | <monochrom> | But clearly generally younger languages have better chances to improve and refine ideas than old languages. |
| 20:19:40 | <segfaultfizzbuzz> | i mean, who cares right? |
| 20:19:54 | <segfaultfizzbuzz> | start from the best ideas rather than holding up old creaky ones |
| 20:20:07 | <EvanR> | You can't teach an old language new tricks. Unless it's C++, which is I guess forever young? |
| 20:20:07 | <dsal> | esqueleto at least gives us the ability to reuse fragments of queries. |
| 20:20:10 | <darkling> | I really need to get some practice time in with Datalog... |
| 20:20:15 | <geekosaur> | not only does it have more rational types, it's a clean implementation of relational calculus instead of an iffy implementation of relational algebra |
| 20:23:03 | <monochrom> | Hell, even the idea of polymorphism was very loose and broad and muddled in the 1960s until Strachey proposed that there is a difference between ad hoc and parametric, and even then he gave only a wordy (read: can be bent misinterpreted) definition, we had to wait until Reynolds to figure out a mathematical definition. |
| 20:23:10 | <segfaultfizzbuzz> | the most essential concept here i guess is persistence right? |
| 20:24:13 | <monochrom> | To be fair, if Strachey didn't die early, probably he could figure out the same mathematical definition eventually. |
| 20:25:21 | × | mechap quits (~mechap@user/mechap) (Quit: WeeChat 3.8) |
| 20:26:43 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) (Remote host closed the connection) |
| 20:27:02 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 20:31:00 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:885e:183b:67ff:4e55) |
| 20:31:00 | <dminuoso> | akegalj: I think maerwald's mention of lack of screeing is probably a more important one. While the general memory safety certainly rules out 2/3 of bugs, the general lack of research and publications specifically on other errors is slightly worrying. One particular example is cryptonite, a pure-haskell written family of cryptographic functions, which to my knowledge has not been audited or |
| 20:31:02 | <dminuoso> | analyzed for side-channels. |
| 20:32:09 | <dminuoso> | I haven't seen research into whether or why Haskell would be more secure. |
| 20:33:03 | <dminuoso> | It may even be, that an attitude in which you blindly assume lack of bugs due to memory safety and type safety could introduce additional vectors. |
| 20:33:31 | <dminuoso> | A prime example might be `postgresql-simple`, which uses some non-audited adhoc self-written query parameter interpolation rather than relying on the builtin libpq features. |
| 20:33:54 | <dminuoso> | Who knows, maybe that library is ripe for SQL injections, in which case a lot of packages have some dangerous attack vectors. |
| 20:34:58 | <geekosaur> | iirc there has been research demonstrating that declarative FP languages are vulnerable to side channel attacks in general |
| 20:35:00 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 20:35:42 | <geekosaur> | and it's hard to prevent them because you can't e.g. do nonsense work to ensure a failing case takes the same time as a success case |
| 20:36:43 | <monochrom> | Hrm, why is it not code optimization that foils nonsense work, and therefore all performant compilers are vulnerable? |
| 20:36:51 | <segfaultfizzbuzz> | geekosaur: i believe it |
| 20:37:09 | <dminuoso> | monochrom: In facft it is. |
| 20:37:17 | <segfaultfizzbuzz> | security is mostly social acceptability and theatre lol |
| 20:37:24 | <geekosaur> | monochrom, in C there are ways to defeat optimization in those cases, or just disable optimization |
| 20:37:31 | <dminuoso> | monochrom: Which is why well designed cryptographic libraries in part disable or control optimizations that interfere with certain assumptions in cryptographic algorithms. |
| 20:37:38 | <geekosaur> | and yes, this does come up in other languages |
| 20:37:45 | <dminuoso> | Some libraries use inline assembly in critical sections to properly control the code |
| 20:38:28 | × | kurbus quits (~kurbus@user/kurbus) (Quit: Client closed) |
| 20:39:43 | <dminuoso> | for instance intel processors have AES specific instructions that are supposed to have constant-time/constant-power behavior. interestingly, there's some recent data that suggest that intel and arm processors might have a lot more timing dependence on values than users are led to believe |
| 20:39:45 | <dminuoso> | https://www.openwall.com/lists/oss-security/2023/01/25/3 |
| 20:39:56 | <monochrom> | Along another orthogonal axis, automatic GC introduces a lot of side information. But then this one is not particular to FP either, basically everyone except possibly C and Fortran has it. |
| 20:39:57 | <dminuoso> | but GCC would never willingly generate them because they have poor performance |
| 20:40:20 | × | avicenzi quits (~avicenzi@2a00:ca8:a1f:b004::c32) (Ping timeout: 246 seconds) |
| 20:41:40 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 20:41:49 | <geekosaur> | monochrom, indeed quite a lot of security critical software is written in C or a subset of C++ because of that |
| 20:42:04 | <dminuoso> | There's a bunch of languages that let you express cryptographic algorithms for which you can extract some kind of program that will use "provably" correct assembly that has the lack of certain side-effect vectors |
| 20:43:57 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 20:44:22 | <segfaultfizzbuzz> | heh |
| 20:44:28 | × | cods quits (~fred@82-65-232-44.subs.proxad.net) (Ping timeout: 265 seconds) |
| 20:44:40 | → | cods joins (~fred@82-65-232-44.subs.proxad.net) |
| 20:44:48 | <dminuoso> | (under the assumption that the hardware will honor its promites...) |
| 20:44:51 | → | califax joins (~califax@user/califx) |
| 20:45:07 | <dminuoso> | which intel doesnt have a great track record for. :p |
| 20:46:35 | → | pavonia joins (~user@user/siracusa) |
| 20:47:47 | × | danza quits (~francesco@151.53.27.222) (Ping timeout: 255 seconds) |
| 20:50:36 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: Exeunt: personae.ai-integration.biz) |
| 20:50:57 | <dminuoso> | I think HACL* is one of the prominent examples of this |
| 20:51:17 | <dminuoso> | Which made its way into Firefox even |
| 20:51:45 | <segfaultfizzbuzz> | wao ... yeah timing safety is important but very expensive to ensure,... |
| 20:53:53 | <segfaultfizzbuzz> | someone mentioned declarative--where can i find a good discussion of declarative programming |
| 20:54:20 | <monochrom> | I have a cunning plan! We should demand random-time instead... >:) |
| 20:55:01 | <segfaultfizzbuzz> | monochrom: injecting timing noise is probably a cheap and effective way to get around timing side channel problems |
| 20:55:04 | <monochrom> | Very old textbooks that have titles along the line of "principles of programming languages". |
| 20:55:21 | <monochrom> | i.e., those who still believe in "paradigms". |
| 20:55:29 | <segfaultfizzbuzz> | haha as opposed to? |
| 20:55:35 | <segfaultfizzbuzz> | chatgpt? lol |
| 20:55:56 | × | oldfashionedcow quits (~Rahul_San@user/oldfashionedcow) (Quit: WeeChat 3.8) |
| 20:56:18 | <segfaultfizzbuzz> | i've been thinking lately though that this whole practice of trying to construct invariants is statistically invalid in most circumstances... like if you construct rules for business logic, they will eventually break, even if they are very good and last for a good while |
| 20:56:23 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 20:57:09 | → | cheater_ joins (~Username@user/cheater) |
| 20:57:44 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:885e:183b:67ff:4e55) (Quit: WeeChat 2.8) |
| 20:58:04 | <monochrom> | As opposed to for example what Shriram Krishnamurthi from Brown University proposes about "paradigms mean nothing" and you dissect a language's features and semantics instead. |
| 20:58:25 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) (Remote host closed the connection) |
| 20:58:29 | × | cheater quits (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 20:58:36 | cheater_ | is now known as cheater |
| 20:58:55 | <monochrom> | which I just illustrated earlier. Instead of discussing side channels in "FP", I discuss side channels under super-smart code optimizations, under GC, etc. |
| 20:59:28 | <mauke> | random noise just means you need to collect more samples |
| 20:59:46 | <segfaultfizzbuzz> | pyret (from shriram) looks pretty 🔥 |
| 20:59:54 | <monochrom> | https://cs.brown.edu/courses/csci1730/2012/ is his course I learned from about analysing languages (as opposed to paradigm-classifying). |
| 21:00:11 | <mauke> | IIRC one of the old SSL attacks did timing shenanigans over the internet and it still worked |
| 21:01:23 | <segfaultfizzbuzz> | monochrom: cool |
| 21:01:54 | → | cheater_ joins (~Username@user/cheater) |
| 21:02:13 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:04:10 | <mniip> | turn any unknown random distribution into a gaussian with this one weird trick |
| 21:05:43 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 21:05:50 | cheater_ | is now known as cheater |
| 21:06:03 | → | merijn joins (~merijn@86.86.29.250) |
| 21:06:20 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 21:06:31 | <segfaultfizzbuzz> | so what should i think about the apparent statistical invalidity of code invariants |
| 21:07:11 | <segfaultfizzbuzz> | like, i make a type or a relationship between variables because i believe something is true or does not occur, and then statistically the real world will eventually violate that |
| 21:07:24 | <segfaultfizzbuzz> | except in very special and rare cases |
| 21:09:11 | <darkling> | Sure, but if your model as originally designed is intended to honour that invariant, then the invariant is a useful validation of the implementation of that model. |
| 21:09:32 | <darkling> | If the model becomes invalid, then you need a new invariant and a new implementation that the new invariant can check. |
| 21:10:17 | <darkling> | This doesn't mean that you should throw away any invariants or tests just because they might be found to be wrong later (or even that you know they're wrong now). |
| 21:10:50 | <darkling> | That's an inevitable problem of the modelling process, and any model of the real world that you build will be incorrect -- but some will be useful. |
| 21:10:51 | <segfaultfizzbuzz> | i'm thinking that the whole of programming is predicated on the idea that i can construct invariants which are true |
| 21:11:05 | <segfaultfizzbuzz> | but more than likely i can only construct false invariants in almost all circumstances |
| 21:12:08 | <segfaultfizzbuzz> | furthermore the stronger the association between the invariants (the stronger my type system, perhaps), the higher the likelihood that these things break irl |
| 21:12:26 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 21:12:47 | <segfaultfizzbuzz> | because then both invariants need to be true, etc |
| 21:13:30 | <darkling> | You'll never model perfectly. |
| 21:13:40 | <darkling> | All you can do is model *well enough for now*. |
| 21:14:19 | <darkling> | "Close enough for government work." |
| 21:14:26 | <geekosaur> | luckily, that's good enough or we'd still be swinging from the trees |
| 21:14:38 | <darkling> | (Or, tightening the requirement significantly, "close enough for practical purposes") |
| 21:15:21 | × | varoo quits (~varoo@122.161.91.19) (Read error: Connection reset by peer) |
| 21:15:31 | <segfaultfizzbuzz> | i think part of what i am thinking here is that if you aren't doing something like writing cryptographic code, a language model will kick your ass at programming |
| 21:17:26 | <geekosaur> | a "language model" can't do much. a domain model that knows the language might do better — but will have more failure modes, including that you can never be certain that it's using the same model you are (cf. https://www.dropbox.com/s/345iszfohklw0sl/dnn.txt?dl=0) |
| 21:17:51 | <geekosaur> | (note also per that essay that the same applies to people!) |
| 21:18:28 | <geekosaur> | and introspecting models to ensure they're actually doing the right thing is a major open research problem |
| 21:19:08 | <darkling> | In $day_job, one of my hats is "ontologist". Overlapping and inconsistent models of the world are my bread and butter. :) |
| 21:20:11 | <darkling> | Well, they will be again when we get to that phase of the project... |
| 21:20:27 | <segfaultfizzbuzz> | i mean you can annotate stuff like this all day: https://www.categoricaldata.net/images/shot4.png but then you will encounter (i can't read this diagram so don't take this example literally) a specialist who specializes in one field at one college but in a different field at another college, or somesuch |
| 21:21:31 | <darkling> | Yes, and this is where you need to model multiple people's conceptualisations of the field and map between them. |
| 21:23:27 | → | varoo joins (~varoo@122.161.91.19) |
| 21:24:02 | × | EvanR quits (~EvanR@user/evanr) (Remote host closed the connection) |
| 21:24:21 | → | EvanR joins (~EvanR@user/evanr) |
| 21:24:23 | × | varoo quits (~varoo@122.161.91.19) (Client Quit) |
| 21:25:20 | <darkling> | (Or at least agree on a workable compromise) |
| 21:28:40 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 21:29:13 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 21:31:04 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:31:49 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 21:33:29 | × | michalz quits (~michalz@185.246.207.197) (Remote host closed the connection) |
| 21:35:09 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 252 seconds) |
| 21:35:31 | → | king_gs joins (~Thunderbi@2806:103e:29:34e5:ecc6:ec8d:1c5b:35a6) |
| 21:38:24 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 268 seconds) |
| 21:39:02 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 21:39:29 | × | merijn quits (~merijn@86.86.29.250) (Ping timeout: 252 seconds) |
| 21:46:46 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 21:46:49 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 21:47:21 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 21:48:04 | Lord_of_Life_ | is now known as Lord_of_Life |
| 21:48:30 | → | qorgi joins (~qorgi@141.161.13.57) |
| 21:55:35 | × | foul_owl quits (~kerry@193.29.61.202) (Ping timeout: 246 seconds) |
| 21:55:44 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:57:47 | → | Tuplanolla joins (~Tuplanoll@91-159-68-152.elisa-laajakaista.fi) |
| 21:58:55 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) |
| 22:02:05 | → | foul_owl joins (~kerry@71.212.143.88) |
| 22:03:50 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5982:f970:3d14:b25c) (Ping timeout: 260 seconds) |
| 22:04:14 | → | codaraxis joins (~codaraxis@user/codaraxis) |
| 22:06:28 | × | bhall quits (~brunohall@138.199.22.99) (Ping timeout: 252 seconds) |
| 22:06:37 | × | jumper149 quits (~jumper149@base.felixspringer.xyz) (Ping timeout: 252 seconds) |
| 22:08:32 | × | foul_owl quits (~kerry@71.212.143.88) (Ping timeout: 248 seconds) |
| 22:11:53 | <qorgi> | hw |
| 22:13:37 | <geekosaur> | ? |
| 22:14:24 | <jackdk> | Hello World? |
| 22:18:02 | × | akegalj quits (~akegalj@222-217.dsl.iskon.hr) (Quit: leaving) |
| 22:18:15 | → | foul_owl joins (~kerry@157.97.134.62) |
| 22:20:15 | × | king_gs quits (~Thunderbi@2806:103e:29:34e5:ecc6:ec8d:1c5b:35a6) (Ping timeout: 248 seconds) |
| 22:20:59 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 22:22:33 | <qorgi> | y |
| 22:22:44 | <jackdk> | ! |
| 22:23:14 | <qorgi> | :p |
| 22:25:19 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 252 seconds) |
| 22:28:14 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:29:50 | × | troydm quits (~troydm@user/troydm) (Ping timeout: 246 seconds) |
| 22:30:48 | <juri_> | i don't suppose anyone here has done any 3d scanning in haskell? |
| 22:32:05 | → | opticblast joins (~Thunderbi@172.58.84.5) |
| 22:36:14 | → | proportions joins (~proportio@91.150.188.137) |
| 22:36:19 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 22:38:16 | → | merijn joins (~merijn@86.86.29.250) |
| 22:40:22 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 22:42:55 | × | merijn quits (~merijn@86.86.29.250) (Ping timeout: 252 seconds) |
| 22:43:07 | → | gmg joins (~user@user/gehmehgeh) |
| 22:43:52 | × | qorgi quits (~qorgi@141.161.13.57) (Remote host closed the connection) |
| 22:44:11 | → | qorgi joins (~qorgi@185.156.46.108) |
| 22:45:11 | × | qorgi quits (~qorgi@185.156.46.108) (Remote host closed the connection) |
| 22:45:29 | → | qorgi joins (~qorgi@185.156.46.108) |
| 22:49:48 | × | qorgi quits (~qorgi@185.156.46.108) (Ping timeout: 260 seconds) |
| 22:52:58 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection) |
| 22:53:39 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 22:54:33 | → | zeenk joins (~zeenk@2a02:2f04:a014:8700::7fe) |
| 22:55:26 | → | merijn joins (~merijn@86.86.29.250) |
| 22:58:56 | → | zaquest joins (~notzaques@5.130.79.72) |
| 22:59:47 | × | merijn quits (~merijn@86.86.29.250) (Ping timeout: 252 seconds) |
| 23:06:23 | → | qorgi joins (~qorgi@141.161.133.94) |
| 23:06:28 | × | qorgi quits (~qorgi@141.161.133.94) (Remote host closed the connection) |
| 23:09:20 | → | qorgi joins (~qorgi@185.156.46.108) |
| 23:09:28 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 23:12:43 | → | jumper149 joins (~jumper149@base.felixspringer.xyz) |
| 23:15:15 | → | king_gs joins (~Thunderbi@187.201.2.248) |
| 23:16:38 | × | qorgi quits (~qorgi@185.156.46.108) (Ping timeout: 260 seconds) |
| 23:16:48 | × | bilegeek quits (~bilegeek@2600:1008:b0a9:5822:3cbe:e760:543a:34cb) (Quit: Leaving) |
| 23:19:34 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 23:21:06 | <c_wraith> | somebody was doing robotics work. Which is... sort of the opposite, I suppose. |
| 23:21:46 | <juri_> | the opposite is the modeler and slicer i maintain, in haskell. ;) |
| 23:22:14 | <juri_> | just hoping i don't have to add '3d scanner' to that list. its enough already. |
| 23:22:15 | <c_wraith> | that's a different opposite. robotics is causing things to be at points in space |
| 23:22:32 | <c_wraith> | Which is sort of an opposite of detecting them |
| 23:22:57 | <juri_> | ok, fair. |
| 23:23:18 | → | jargon joins (~jargon@184.101.182.107) |
| 23:23:27 | <c_wraith> | But still not useful to you |
| 23:25:46 | <monochrom> | Use https://www.smbc-comics.com/comic/four to reduce detection to actuation. >:D |
| 23:25:46 | × | king_gs quits (~Thunderbi@187.201.2.248) (Read error: Connection reset by peer) |
| 23:29:56 | × | tremon quits (~tremon@83-85-213-108.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in) |
| 23:30:31 | <hpc> | the alt text is how i do all my programming :P |
| 23:30:37 | → | thongpv joins (~thongpv87@14.179.159.25) |
| 23:35:56 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 23:38:33 | <segfaultfizzbuzz> | okay so what if programming languages were designed with the assumption that the programmer is an adversary |
| 23:38:53 | <segfaultfizzbuzz> | like if you hire a hundred people to work on your code base, a few of them might be bad apples, ya know |
| 23:39:09 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 23:39:37 | <c_wraith> | You'd probably get a language based around capabilities with strict static typing. |
| 23:39:45 | <segfaultfizzbuzz> | sounds right |
| 23:40:12 | <segfaultfizzbuzz> | and then probably half of the programmers won't be bad apples but will overestimate how correct they are |
| 23:40:23 | <segfaultfizzbuzz> | and then the remaining half will also overestimate how correct they are |
| 23:40:29 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
| 23:40:59 | <segfaultfizzbuzz> | haskell has capabilities...? |
| 23:42:24 | × | jero98772 quits (~jero98772@2800:484:1d80:d8ce:9815:cfda:3661:17bb) (Ping timeout: 248 seconds) |
| 23:42:38 | <c_wraith> | eh. you could get there with some combination of careful libraries and an extension like Safe Haskell, but it'd be a lot of work. |
| 23:43:12 | <c_wraith> | also, Safe Haskell isn't quite the right tool for the job, so it would need to be something *like* it with a clearer purpose |
| 23:43:19 | <monochrom> | Is there any other goal such as some minimum level of productivity that your hypothetical programming language needs to achieve, and you forgot to mention it? |
| 23:43:46 | <monochrom> | Because without any other goals, the best way to deal with adversaries is to allow nothing. |
| 23:44:05 | <segfaultfizzbuzz> | uh but then you get nothing done |
| 23:44:21 | <monochrom> | Sure. So what's your other goals? |
| 23:44:32 | <monochrom> | And how much? |
| 23:45:03 | <segfaultfizzbuzz> | i don't know, i am personally interested in the "most ideal, least productive" languages these days |
| 23:45:20 | <segfaultfizzbuzz> | for the purpose of getting some kind of understanding of "what is best" |
| 23:45:28 | <segfaultfizzbuzz> | even if i never actually use them |
| 23:45:44 | <monochrom> | I don't know what "ideal" means. (Do you?) But trivially clearly least productive = allow nothing done |
| 23:46:07 | <segfaultfizzbuzz> | yeah i'm not fond of "the safest car is no car" |
| 23:46:31 | <monochrom> | If you want an actually interesting discussion, you need to state actually interesting goals. |
| 23:46:37 | → | off^ joins (~tj99@c-24-30-76-89.hsd1.ga.comcast.net) |
| 23:46:57 | <monochrom> | Because otherwise I'll just trivialize all of your stated scenerios because they are trivial in the first place. |
| 23:48:54 | ← | proportions parts (~proportio@91.150.188.137) () |
| 23:54:26 | <monochrom> | And the other angle is that I learned from multiple practicing teachers and practicing economists that if you treat people as adversaries then they will game your system, but if you respect them then they will respect you. |
| 23:55:01 | <segfaultfizzbuzz> | sure there is the psychology angle on it, but the reality is that there are always some bad apples whatever the case |
| 23:55:11 | <geekosaur> | …often just to get things done |
| 23:55:16 | <monochrom> | I would rather s/bad apples/honest mistakes/ |
| 23:55:54 | × | jumper149 quits (~jumper149@base.felixspringer.xyz) (Quit: WeeChat 3.7.1) |
| 23:56:12 | <monochrom> | So my idea of a good programming language is it respects programmers but acknowledges that there are honest mistakes to guard against or maybe just discourage. |
| 23:56:40 | <monochrom> | But then that also closes this discussion because all practical programming languages already try to do that. |
| 23:57:15 | <monochrom> | So, anything new? |
All times are in UTC on 2023-01-30.