Newest at the top
| 2024-11-19 12:36:54 +0100 | euleritian | (~euleritia@ip4d16fc9f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2024-11-19 12:34:08 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2024-11-19 12:32:28 +0100 | euleritian | (~euleritia@ip4d16fc9f.dynamic.kabel-deutschland.de) |
| 2024-11-19 12:31:19 +0100 | euleritian | (~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 +0100 | ubert | (~Thunderbi@178.115.41.15.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 2024-11-19 12:29:18 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2024-11-19 12:21:35 +0100 | ubert | (~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 +0100 | sawilagar | (~sawilagar@user/sawilagar) sawilagar |
| 2024-11-19 12:10:30 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Remote host closed the connection) |
| 2024-11-19 12:10:02 +0100 | ubert | (~Thunderbi@178.115.41.15.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 2024-11-19 12:09:56 +0100 | notzmv | (~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 +0100 | ubert | (~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 +0100 | ubert | (~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? |
| 2024-11-19 11:53:16 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2024-11-19 11:23:37 +0100 | mange | (~user@user/mange) (Quit: Zzz...) |
| 2024-11-19 11:21:54 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-11-19 11:19:23 +0100 | <Leary> | (where `type f ! k = forall t. f (k @ t)`) |
| 2024-11-19 11:18:31 +0100 | <Leary> | jackdk: For e.g. `type data Wibble = Wobble Foo | Nibble Wibble Wibble` I'm writing TH that ought to generate `deriving instance Show (Wibble @ t)` given that we already have `Show! Foo` in scope, but really it will generate `deriving instance (Show! Foo, Show! Wibble, Show! Wibble) => Show (Wibble @ t)`. |
| 2024-11-19 11:13:12 +0100 | <jackdk> | Something like that. I don't know enough about your problem to be sure |
| 2024-11-19 11:12:58 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |