2025/10/23

Newest at the top

2025-10-23 15:27:59 +0200gustrb(~gustrb@191.243.134.87)
2025-10-23 15:26:13 +0200trickard_(~trickard@cpe-55-98-47-163.wireline.com.au)
2025-10-23 15:25:46 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-10-23 15:24:03 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-10-23 15:23:28 +0200qqe(~qqq@185.54.23.200)
2025-10-23 15:22:16 +0200trickard_(~trickard@cpe-55-98-47-163.wireline.com.au) (Ping timeout: 255 seconds)
2025-10-23 15:20:40 +0200Googulator56(~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed)
2025-10-23 15:20:40 +0200Googulator72(~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu)
2025-10-23 15:16:42 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 256 seconds)
2025-10-23 15:15:03 +0200trickard_(~trickard@cpe-55-98-47-163.wireline.com.au)
2025-10-23 15:14:49 +0200trickard_(~trickard@cpe-55-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-10-23 15:10:58 +0200wbrawner(~wbrawner@static.56.224.132.142.clients.your-server.de) wbrawner
2025-10-23 15:08:25 +0200wbrawner(~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 +0200petrichor(~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 +0200cipherrot(~jez@user/petrichor) petrichor
2025-10-23 15:05:02 +0200Enrico63(~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 +0200bggd(~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 +0200Googulator56(~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu)
2025-10-23 15:00:41 +0200Googulator56(~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed)
2025-10-23 15:00:40 +0200wbrawner(~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.