Newest at the top
| 2024-10-06 13:09:18 +0200 | rosco | (~rosco@183.171.72.164) (Ping timeout: 252 seconds) |
| 2024-10-06 13:09:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-10-06 13:04:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-06 13:03:26 +0200 | mrmr155334346318 | (~mrmr@user/mrmr) (Quit: Bye, See ya later!) |
| 2024-10-06 12:53:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-06 12:50:48 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-10-06 12:50:30 +0200 | CiaoSen | (~Jura@2a05:5800:464:f400:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-10-06 12:48:50 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2024-10-06 12:48:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-06 12:43:08 +0200 | <Hecate> | nope sorry |
| 2024-10-06 12:40:54 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:e481:13d5:7eb4:8f9d) (Ping timeout: 246 seconds) |
| 2024-10-06 12:38:54 +0200 | <lxsameer> | hey folks, do you know any channel or forum dedicated to category theory and/or type theory? |
| 2024-10-06 12:38:35 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-10-06 12:37:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-10-06 12:34:03 +0200 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2024-10-06 12:33:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-06 12:29:55 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:e481:13d5:7eb4:8f9d) |
| 2024-10-06 12:28:17 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2024-10-06 12:25:34 +0200 | son0p | (~ff@186.121.110.81) (Remote host closed the connection) |
| 2024-10-06 12:24:13 +0200 | <lambdabot> | Consider it noted. |
| 2024-10-06 12:24:13 +0200 | <tomsmeding> | @tell artu you need :{ and :} to write multi-line definitions in ghci |
| 2024-10-06 12:23:56 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2024-10-06 12:23:10 +0200 | xff0x | (~xff0x@2405:6580:b080:900:e9cd:7fb:f9ec:b14e) |
| 2024-10-06 12:21:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-06 12:16:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-06 12:14:39 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-10-06 12:13:11 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:6ee5:dea:457b:d9d9) (Ping timeout: 252 seconds) |
| 2024-10-06 12:11:01 +0200 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 248 seconds) |
| 2024-10-06 12:03:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-06 12:01:38 +0200 | CrunchyFlakes | (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) |
| 2024-10-06 12:00:35 +0200 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Read error: Connection reset by peer) |
| 2024-10-06 11:59:59 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-10-06 11:59:08 +0200 | xff0x | (~xff0x@2405:6580:b080:900:943:dffd:9430:e374) (Ping timeout: 245 seconds) |
| 2024-10-06 11:58:50 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-06 11:57:05 +0200 | CrunchyFlakes | (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2024-10-06 11:53:19 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:6ee5:dea:457b:d9d9) |
| 2024-10-06 11:46:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-06 11:41:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-06 11:40:22 +0200 | <ncf> | define size? |
| 2024-10-06 11:40:07 +0200 | <haskellbridge> | <thirdofmay18081814goya> data types with values of finite size |
| 2024-10-06 11:39:48 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah, I meant values of finite size |
| 2024-10-06 11:38:23 +0200 | <Lears> | To be clear, "finite" here is ambiguous. If you mean data types of finite cardinality then the answer is still nothing in e.g. System F. I took you to mean data types with values of finite size. |
| 2024-10-06 11:37:54 +0200 | rosco | (~rosco@183.171.72.164) rosco |
| 2024-10-06 11:36:22 +0200 | <haskellbridge> | <thirdofmay18081814goya> ty for answers |
| 2024-10-06 11:36:16 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm i see |
| 2024-10-06 11:36:06 +0200 | <ncf> | or 1 + — i guess |
| 2024-10-06 11:35:37 +0200 | <ncf> | the least fixed point of Const ℕ is infinite |
| 2024-10-06 11:35:19 +0200 | <Lears> | thirdofmay: In Haskell, nothing. In System F, strong normalisation and program finiteness. |
| 2024-10-06 11:35:00 +0200 | <ncf> | nothing |
| 2024-10-06 11:32:53 +0200 | <haskellbridge> | <thirdofmay18081814goya> what guarantees that the least fixed point of a type-functor will produce finite data types? |