2024/11/19

Newest at the top

2024-11-19 12:45:58 +0100 <hellwolf> I can't find one.
2024-11-19 12:45:55 +0100 <hellwolf> what's the standard "hush" function for Ether a b -> Maybe b?
2024-11-19 12:43:05 +0100housemate(~housemate@2a04:9dc0:0:162::5d91:d7ed) housemate
2024-11-19 12:42:10 +0100igemnace(~igemnace@user/igemnace) igemnace
2024-11-19 12:40:42 +0100Smiles(uid551636@id-551636.lymington.irccloud.com) Smiles
2024-11-19 12:39:20 +0100igemnace(~igemnace@user/igemnace) (Quit: ZNC 1.9.0+deb2build3 - https://znc.in)
2024-11-19 12:38:18 +0100euleritian(~euleritia@dynamic-176-001-000-183.176.1.pool.telefonica.de)
2024-11-19 12:36:54 +0100euleritian(~euleritia@ip4d16fc9f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2024-11-19 12:34:08 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2)
2024-11-19 12:32:28 +0100euleritian(~euleritia@ip4d16fc9f.dynamic.kabel-deutschland.de)
2024-11-19 12:31:19 +0100euleritian(~euleritia@ip4d16fc9f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-11-19 12:31:19 +0100 <geekosaur> we have that in at least two ways though (RebindableSyntax and QualifiedDo)
2024-11-19 12:29:34 +0100ubert(~Thunderbi@178.115.41.15.wireless.dyn.drei.com) (Ping timeout: 260 seconds)
2024-11-19 12:29:18 +0100pavonia(~user@user/siracusa) siracusa
2024-11-19 12:21:35 +0100ubert(~Thunderbi@178.115.41.15.wireless.dyn.drei.com) ubert
2024-11-19 12:11:12 +0100 <kuribas> For example, do can be overloaded by defining your own (>>=) function.
2024-11-19 12:10:49 +0100sawilagar(~sawilagar@user/sawilagar) sawilagar
2024-11-19 12:10:30 +0100sawilagar(~sawilagar@user/sawilagar) (Remote host closed the connection)
2024-11-19 12:10:02 +0100ubert(~Thunderbi@178.115.41.15.wireless.dyn.drei.com) (Ping timeout: 252 seconds)
2024-11-19 12:09:56 +0100notzmv(~daniel@user/notzmv) (Read error: Connection reset by peer)
2024-11-19 12:07:20 +0100 <kuribas> It's a nice to have in idris, because it allows syntactic overloading, but I am not sure it is necessary to have.
2024-11-19 12:06:18 +0100 <kuribas> And type checking very slow.
2024-11-19 12:06:05 +0100 <kuribas> Which makes getting accurate error message difficult.
2024-11-19 12:05:52 +0100 <kuribas> One blocking issue for me with idris and error messages is the ad-hoc polymorphism.
2024-11-19 12:05:35 +0100 <kuribas> yeah ...
2024-11-19 12:05:33 +0100ubert(~Thunderbi@178.115.41.15.wireless.dyn.drei.com) ubert
2024-11-19 12:05:23 +0100 <Hecate> maybe improve idris too while you're at it? :D
2024-11-19 12:05:16 +0100ubert(~Thunderbi@178.115.41.15.wireless.dyn.drei.com) (Read error: Connection reset by peer)
2024-11-19 12:05:14 +0100 <Hecate> there are indeed
2024-11-19 12:05:07 +0100 <kuribas> When dabbling with idris I feel there is a lot of low hanging fruit there.
2024-11-19 12:04:53 +0100 <Hecate> best case, an LLM will feed off of your work later
2024-11-19 12:04:52 +0100 <kuribas> Hecate: agreed :)
2024-11-19 12:04:40 +0100 <Hecate> kuribas: ah, DT languages with good ergonomics are something that need you to advance the state of the art
2024-11-19 12:04:35 +0100 <kuribas> Or maybe elaborate a bit then?
2024-11-19 12:04:11 +0100 <Hecate> kuribas: To rephrase your suggestion: "Would it be possible to train an LLM on an existing dataset to generate new things, which an LLM simply cannot?"
2024-11-19 12:04:06 +0100 <int-e> and LLMs are terrible at that
2024-11-19 12:04:02 +0100 <kuribas> I am happy with GHC error messages, but I am interested in creating a general purpose dependently typed language.
2024-11-19 12:04:00 +0100 <int-e> but error messages need to be accurate
2024-11-19 12:03:41 +0100 <kuribas> More beginner friendly.
2024-11-19 12:03:30 +0100 <int-e> kuribas: define "better"
2024-11-19 12:03:28 +0100 <Hecate> kuribas: no it's not outrageous, it's ridiculous :P
2024-11-19 12:03:20 +0100 <lambdabot> the eta-reduction property does not hold
2024-11-19 12:03:20 +0100 <int-e> @ghc
2024-11-19 12:03:04 +0100 <kuribas> Is that so outrageous?
2024-11-19 12:03:01 +0100 <lambdabot> Its main purpose is to encapsulate the Horrible State Hack
2024-11-19 12:03:01 +0100 <int-e> @ghc
2024-11-19 12:02:33 +0100 <Hecate> :P
2024-11-19 12:02:32 +0100 <Hecate> you silly
2024-11-19 12:02:31 +0100 <Hecate> kuribas: hahahahahahaha
2024-11-19 12:01:56 +0100 <kuribas> Would it be possible to train a llm to generate better error messages?