Newest at the top
2025-06-07 00:07:34 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-07 00:07:09 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-07 00:06:44 +0200 | ljdarj1 | ljdarj |
2025-06-07 00:06:44 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
2025-06-07 00:03:30 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
2025-06-07 00:01:05 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-07 00:00:43 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-07 00:00:17 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
2025-06-07 00:00:16 +0200 | iteratee | (~kyle@199.119.84.78) iteratee |
2025-06-06 23:59:54 +0200 | tromp | (~textual@2001:1c00:3487:1b00:8836:3ddb:338e:2a33) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2025-06-06 23:57:54 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 23:57:31 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-06 23:53:27 +0200 | iteratee | (~kyle@199.119.84.78) (Ping timeout: 272 seconds) |
2025-06-06 23:52:48 +0200 | michalz | (~michalz@185.246.207.205) (Remote host closed the connection) |
2025-06-06 23:52:32 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 23:52:05 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-06 23:51:17 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 248 seconds) |
2025-06-06 23:47:58 +0200 | <ski> | (in MetaML you instead would use the distinction between functions (not inspectable), and quotations of functions (inspectable). basically `T -> U' s. `TExp (T -> U)', in TH terms) |
2025-06-06 23:47:26 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 23:47:01 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
2025-06-06 23:46:17 +0200 | <ski> | i also recall reading a paper (by Dale Miller, i think), of a system having both FP style (normal) functions, and a different type of matchable, restricted, functions |
2025-06-06 23:45:40 +0200 | <tomsmeding> | right |
2025-06-06 23:45:23 +0200 | <ski> | more that there are implemented systems with notions of functions along these lines, making this idea practical |
2025-06-06 23:45:15 +0200 | <tomsmeding> | also, I can't find any lambdaProlog code in the Pfenning/Elliott paper |
2025-06-06 23:43:13 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 23:42:48 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
2025-06-06 23:41:17 +0200 | <tomsmeding> | in which case: well, yes |
2025-06-06 23:41:05 +0200 | <tomsmeding> | ski: I may be misunderstanding you, but are you saying "you can match on functions if you restrict functions to the ones you can match on"? |
2025-06-06 23:40:49 +0200 | <ski> | "The first programming language which directly supported λ-bindings in syntax was the higher-order logic programming language λProlog. The paper that introduced the term HOAS used λProlog code to illustrate it." |
2025-06-06 23:40:08 +0200 | <ski> | (see the <https://en.wikipedia.org/wiki/Higher-order_abstract_syntax#Use_in_logic_programming> and <https://en.wikipedia.org/wiki/Higher-order_abstract_syntax#Use_in_logical_frameworks> (Twelf is implementation of LF) sections) |
2025-06-06 23:39:51 +0200 | iteratee | (~kyle@199.119.84.78) iteratee |
2025-06-06 23:39:23 +0200 | trickard_ | (~trickard@cpe-53-98-47-163.wireline.com.au) |
2025-06-06 23:39:09 +0200 | trickard_ | (~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
2025-06-06 23:37:44 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 23:37:23 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-06 23:37:18 +0200 | <ski> | "you couldn't check it, but there is nothing to check in the first place" -- you can (pattern-match on functions, traversing inside their bodies), in lambdaProlog, Twelf (and MetaML), because the functions there are restricted, can't express general computation (in the MetaML case, you'd be matching on quoted functions, comparable to Template Haskell with quasiquotation, although a bit smoother) |
2025-06-06 23:33:44 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
2025-06-06 23:33:34 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 252 seconds) |
2025-06-06 23:30:56 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 23:30:30 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-06 23:29:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-06-06 23:27:13 +0200 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 248 seconds) |
2025-06-06 23:26:09 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 23:25:46 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-06 23:24:28 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
2025-06-06 23:21:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-06-06 23:21:13 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 23:20:46 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-06 23:17:51 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-06-06 23:17:35 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |