Newest at the top
| 2025-01-14 12:33:38 +0100 | jespada | (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) jespada |
| 2025-01-14 12:26:22 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 12:24:13 +0100 | dysthesis | (~dysthesis@user/dysthesis) dysthesis |
| 2025-01-14 12:16:23 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-14 12:13:59 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2025-01-14 12:13:29 +0100 | xff0x | (~xff0x@2405:6580:b080:900:5599:62cc:9825:4e0a) |
| 2025-01-14 12:10:06 +0100 | <tomsmeding> | is HOAS not more about representing an AST? |
| 2025-01-14 12:10:04 +0100 | <kuribas> | tomsmeding: I was just considering this: https://en.wikipedia.org/wiki/Higher-order_abstract_syntax |
| 2025-01-14 12:10:04 +0100 | akegalj | (~akegalj@89-172-71-66.adsl.net.t-com.hr) (Ping timeout: 244 seconds) |
| 2025-01-14 12:09:25 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) Miroboru |
| 2025-01-14 12:08:55 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) kuribas |
| 2025-01-14 12:08:19 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 2025-01-14 12:07:46 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-01-14 11:59:34 +0100 | mange | (~user@user/mange) (Quit: Zzz...) |
| 2025-01-14 11:59:03 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal) |
| 2025-01-14 11:51:25 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) kuribas |
| 2025-01-14 11:49:36 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 11:45:12 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2025-01-14 11:39:12 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 11:38:46 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-14 11:38:45 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2025-01-14 11:37:19 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds) |
| 2025-01-14 11:37:10 +0100 | sprotte24 | (~sprotte24@p200300d16f2d390001157685e299ee37.dip0.t-ipconnect.de) (Client Quit) |
| 2025-01-14 11:37:08 +0100 | sprotte24 | (~sprotte24@p200300d16f2d390001157685e299ee37.dip0.t-ipconnect.de) |
| 2025-01-14 11:35:05 +0100 | jespada | (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-01-14 11:33:06 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 11:32:28 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2025-01-14 11:27:55 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 11:24:39 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 252 seconds) |
| 2025-01-14 11:14:32 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2025-01-14 11:10:13 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 11:09:50 +0100 | <smiesner> | *laughs in java and js* (pls free me) |
| 2025-01-14 11:01:22 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2025-01-14 10:58:34 +0100 | <tomsmeding> | :D |
| 2025-01-14 10:58:23 +0100 | <kuribas> | Python and clojure :( |
| 2025-01-14 10:58:06 +0100 | <kuribas> | gotto do my day job now :) |
| 2025-01-14 10:57:19 +0100 | <kuribas> | tomsmeding: not exactly sure, I'll need to work it out... |
| 2025-01-14 10:56:57 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2025-01-14 10:54:45 +0100 | <tomsmeding> | never mind that this type doesn't have a sensible implementation, but more complicated such examples do |
| 2025-01-14 10:54:15 +0100 | <tomsmeding> | so then how are you going to write the type "(f : Type -> Type) -> (a : Type) -> f a"? |
| 2025-01-14 10:53:39 +0100 | <kuribas> | polymorphic types. |
| 2025-01-14 10:53:29 +0100 | <kuribas> | Yeah, in the implementing language. Like HOAS. |
| 2025-01-14 10:52:28 +0100 | <tomsmeding> | wasn't the premise that you can write types using combinators instead of foralls? |
| 2025-01-14 10:52:07 +0100 | <kuribas> | tomsmeding: not in the implementing language. |
| 2025-01-14 10:51:04 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-01-14 10:50:59 +0100 | <tomsmeding> | but then you aren't actually applying types, are you? What is S? |
| 2025-01-14 10:50:50 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 10:50:42 +0100 | <kuribas> | a -> a |
| 2025-01-14 10:50:22 +0100 | <tomsmeding> | what is S? |
| 2025-01-14 10:50:19 +0100 | <tomsmeding> | is I "a -> a"? or is I just "a"? |