2025/06/06

Newest at the top

2025-06-07 00:07:09 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-07 00:06:44 +0200ljdarj1ljdarj
2025-06-07 00:06:44 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds)
2025-06-07 00:03:30 +0200ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-06-07 00:01:05 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-07 00:00:43 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-07 00:00:17 +0200todi(~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-06-07 00:00:16 +0200iteratee(~kyle@199.119.84.78) iteratee
2025-06-06 23:59:54 +0200tromp(~textual@2001:1c00:3487:1b00:8836:3ddb:338e:2a33) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-06-06 23:57:54 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 23:57:31 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-06 23:53:27 +0200iteratee(~kyle@199.119.84.78) (Ping timeout: 272 seconds)
2025-06-06 23:52:48 +0200michalz(~michalz@185.246.207.205) (Remote host closed the connection)
2025-06-06 23:52:32 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 23:52:05 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-06 23:51:17 +0200ystael(~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 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 23:47:01 +0200sabathan2(~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 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 23:42:48 +0200sabathan2(~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 +0200iteratee(~kyle@199.119.84.78) iteratee
2025-06-06 23:39:23 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au)
2025-06-06 23:39:09 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-06-06 23:37:44 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 23:37:23 +0200sabathan2(~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 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2025-06-06 23:33:34 +0200jmcantrell(~weechat@user/jmcantrell) (Ping timeout: 252 seconds)
2025-06-06 23:30:56 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 23:30:30 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-06 23:29:23 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-06-06 23:27:13 +0200prdak(~Thunderbi@user/prdak) (Ping timeout: 248 seconds)
2025-06-06 23:26:09 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 23:25:46 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-06 23:24:28 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-06-06 23:21:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-06-06 23:21:13 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 23:20:46 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-06 23:17:51 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-06-06 23:17:35 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich)
2025-06-06 23:16:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn