Newest at the top
2025-01-14 12:43:05 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) alexherbo2 |
2025-01-14 12:42:32 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) (Remote host closed the connection) |
2025-01-14 12:37:43 +0100 | dmwit | (~dmwit@pool-173-66-76-243.washdc.fios.verizon.net) (Quit: Client closed) |
2025-01-14 12:36:51 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
2025-01-14 12:36:06 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) alexherbo2 |
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 |