Newest at the top
2025-10-23 15:27:59 +0200 | gustrb | (~gustrb@191.243.134.87) |
2025-10-23 15:26:13 +0200 | trickard_ | (~trickard@cpe-55-98-47-163.wireline.com.au) |
2025-10-23 15:25:46 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
2025-10-23 15:24:03 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
2025-10-23 15:23:28 +0200 | qqe | (~qqq@185.54.23.200) |
2025-10-23 15:22:16 +0200 | trickard_ | (~trickard@cpe-55-98-47-163.wireline.com.au) (Ping timeout: 255 seconds) |
2025-10-23 15:20:40 +0200 | Googulator56 | (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
2025-10-23 15:20:40 +0200 | Googulator72 | (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
2025-10-23 15:16:42 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 256 seconds) |
2025-10-23 15:15:03 +0200 | trickard_ | (~trickard@cpe-55-98-47-163.wireline.com.au) |
2025-10-23 15:14:49 +0200 | trickard_ | (~trickard@cpe-55-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
2025-10-23 15:10:58 +0200 | wbrawner | (~wbrawner@static.56.224.132.142.clients.your-server.de) wbrawner |
2025-10-23 15:08:25 +0200 | wbrawner | (~wbrawner@static.56.224.132.142.clients.your-server.de) (Ping timeout: 264 seconds) |
2025-10-23 15:08:08 +0200 | <tomsmeding> | yes |
2025-10-23 15:08:04 +0200 | <kuribas> | singletons are a good sign you want dependent types :) |
2025-10-23 15:07:23 +0200 | <tomsmeding> | (or at least, I assume it's the same thing) |
2025-10-23 15:07:22 +0200 | petrichor | (~jez@user/petrichor) (Ping timeout: 260 seconds) |
2025-10-23 15:07:16 +0200 | <tomsmeding> | but with singletons |
2025-10-23 15:07:12 +0200 | <tomsmeding> | yeah so this is the same thing |
2025-10-23 15:07:09 +0200 | <kuribas> | In the idris2 compiler. |
2025-10-23 15:07:02 +0200 | <kuribas> | Edwin Bradey said that using dependent types helped a lot in getting the Debruyn indexes correct in his code. |
2025-10-23 15:06:57 +0200 | <tomsmeding> | [exa]: does that mean that you commiserate? |
2025-10-23 15:05:45 +0200 | cipherrot | (~jez@user/petrichor) petrichor |
2025-10-23 15:05:02 +0200 | Enrico63 | (~Enrico63@host-82-59-110-109.retail.telecomitalia.it) Enrico63 |
2025-10-23 15:04:52 +0200 | <tomsmeding> | (this is the most complicated file in the project) |
2025-10-23 15:04:32 +0200 | <tomsmeding> | a taste: https://git.tomsmeding.com/chad-fast/tree/src/CHAD.hs |
2025-10-23 15:04:31 +0200 | <kuribas> | idk, haskell to idris may not be too hard? |
2025-10-23 15:04:10 +0200 | <tomsmeding> | it may or may not have been a good idea |
2025-10-23 15:03:59 +0200 | <tomsmeding> | kuribas: sunk cost, at this point |
2025-10-23 15:03:51 +0200 | <kuribas> | tomsmeding: prototype it in idris/agda, then port to haskell? |
2025-10-23 15:03:46 +0200 | <[exa]> | :) |
2025-10-23 15:03:43 +0200 | <[exa]> | oh man. |
2025-10-23 15:03:38 +0200 | <tomsmeding> | and I'm implementing a highly nontrivial code transformation in it that changes types a bunch |
2025-10-23 15:03:31 +0200 | <kuribas> | ah :) |
2025-10-23 15:03:26 +0200 | <tomsmeding> | with a well-typed well-scoped De Bruijn AST |
2025-10-23 15:03:09 +0200 | <tomsmeding> | kuribas: writing a compiler |
2025-10-23 15:03:09 +0200 | bggd | (~bgg@2a01:e0a:819:1510:f0f7:e908:85f6:a650) (Remote host closed the connection) |
2025-10-23 15:02:55 +0200 | <tomsmeding> | but I concluded each time that the increase in convenience for type-level stuff would not be offset against the loss of convenience when actually doing something useful |
2025-10-23 15:02:46 +0200 | <kuribas> | What is it exactly you are doing? |
2025-10-23 15:02:18 +0200 | <tomsmeding> | I have considered multiple times to rewrite this in agda |
2025-10-23 15:02:16 +0200 | <kuribas> | (or agda, lean, ...) |
2025-10-23 15:02:04 +0200 | <kuribas> | If you are doing lots of type level computation, maybe idris is a better language. |
2025-10-23 15:02:03 +0200 | <tomsmeding> | good question |
2025-10-23 15:01:53 +0200 | <kuribas> | But why do this in haskell at all? |
2025-10-23 15:01:08 +0200 | <tomsmeding> | this is about type family injectivity; the type classes were brought in in an attempt to abuse FunctionalDependencies, which are apparently slightly stronger than tyfam injectivity |
2025-10-23 15:00:49 +0200 | Googulator56 | (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
2025-10-23 15:00:41 +0200 | Googulator56 | (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
2025-10-23 15:00:40 +0200 | wbrawner | (~wbrawner@static.56.224.132.142.clients.your-server.de) wbrawner |
2025-10-23 15:00:39 +0200 | <tomsmeding> | kuribas: in my original code there aren't even any classes! |
2025-10-23 15:00:33 +0200 | <kuribas> | tomsmeding: I don't get why it cannot create a hole for a type class instance that depends on another hole. |