Newest at the top
| 2024-05-16 12:26:29 +0200 | patrl | (~patrl@user/patrl) (Remote host closed the connection) |
| 2024-05-16 12:24:05 +0200 | patrl | (~patrl@user/patrl) |
| 2024-05-16 12:23:19 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-05-16 12:21:37 +0200 | patrl | (~patrl@user/patrl) (Remote host closed the connection) |
| 2024-05-16 12:20:48 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-05-16 12:13:28 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-05-16 12:08:51 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 255 seconds) |
| 2024-05-16 12:02:08 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1) |
| 2024-05-16 12:01:38 +0200 | danse-nr3 | (~danse-nr3@an-19-164-164.service.infuturo.it) (Ping timeout: 268 seconds) |
| 2024-05-16 11:58:52 +0200 | libertyprime | (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) (Remote host closed the connection) |
| 2024-05-16 11:56:36 +0200 | pie_ | (~pie_bnc@user/pie/x-2818909) |
| 2024-05-16 11:56:18 +0200 | pie_ | (~pie_bnc@user/pie/x-2818909) () |
| 2024-05-16 11:53:45 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-05-16 11:52:10 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 2024-05-16 11:49:41 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-05-16 11:46:26 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-05-16 11:42:40 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:e4f7:dd84:71b6:db6) |
| 2024-05-16 11:38:38 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
| 2024-05-16 11:38:23 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-05-16 11:37:44 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2024-05-16 11:37:44 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-05-16 11:35:22 +0200 | <ski> | (i guess one should clearly distinguish here between wanting to parameterize an LF program (being a signature), and wanting to parameterize a realization of that signature (which would give a functor). what i meant to say at the end above is that i've seen papers for (and source code implementing) the latter, but not the former) |
| 2024-05-16 11:34:45 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-05-16 11:34:26 +0200 | cfricke | (~cfricke@user/cfricke) (Remote host closed the connection) |
| 2024-05-16 11:33:51 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:e61a:851b:d7b:27e8) |
| 2024-05-16 11:32:15 +0200 | <ski> | kuribas` : or load five (copy-pasted) versions of it. or perhaps it could be possible to parameterize the whole file on `elem', but aiui, Twelf doesn't currently implement anything like that |
| 2024-05-16 11:31:02 +0200 | <ski> | proof search automatically can find for your), into a derivation in the declarative system) |
| 2024-05-16 11:30:56 +0200 | <ski> | inference rules (comprising one signature), and then also specify an alternative set of "algorithmic" inference rules (avoiding ambiguity, and allowing the type signatures to be effectively be interpreted as a logic program, something the declarative version often doesn't usefully, or at least efficiently, admit) .. and then the functor tells you how to transform a derivation in the algorithmic system (which |
| 2024-05-16 11:30:50 +0200 | <ski> | (btw .. an LF program is basically a signature, a list of type signatures of constants (value constants and type constants) .. you can interpret this as something quite close to an ML module signature, and then you can introduce ML module functors into the picture, implementing the constants of one signature in terms of those of another. this is e.g. useful when you specify a type system using "declarative" |
| 2024-05-16 11:26:57 +0200 | <kuribas`> | ski: If if I need 5 different types of lists, I need to load the module 5 times? |
| 2024-05-16 11:26:22 +0200 | <ski> | (so `list' itself is not a parameterized type, and relations/predicates operating over it won't be parametrically polymorphic in the element type) |
| 2024-05-16 11:25:30 +0200 | <ski> | kuribas` : sure, it's parametric in the sense of ML functors (parameterized modules), you can assume anything you like about the element type `elem'. but `list' has type `type', not `type -> type' |
| 2024-05-16 11:24:50 +0200 | <ski> | "A Semi-Functional Implementation of a Higher-Order Logic Programming Language" by Conal Elliott,Frank Pfenning in 1990-02 (draft) at <http://www.cs.cmu.edu/~fp/papers/elpsml90.pdf>,<http://www.cs.cmu.edu/~fp/papers/elpsml-paper.tar.gz> |
| 2024-05-16 11:24:47 +0200 | <ski> | "Unification Under a Mixed Prefix" by Dale Miller in 1992-07-08 at <https://www.lix.polytechnique.fr/~dale/papers/jsc92.pdf> |
| 2024-05-16 11:22:50 +0200 | destituion | (~destituio@85.221.111.174) |
| 2024-05-16 11:21:59 +0200 | destituion | (~destituio@2a02:2121:10b:62ca:bae7:e090:21e:1459) (Ping timeout: 256 seconds) |
| 2024-05-16 11:21:37 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-05-16 11:20:41 +0200 | <kuribas`> | ski: it looks like lists are parametric? https://twelf.org/wiki/lists/ |
| 2024-05-16 11:17:51 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:a189:af79:61c5:4ba2) (Ping timeout: 268 seconds) |
| 2024-05-16 11:07:53 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-05-16 11:02:22 +0200 | <ski> | (they implement in SML, using a one-level continuation-passing style. success means calling continuation deeper. failure means returning. initial continuation will print out answer substitution, and query if user wants to search for more solutions. they implement cut by throwing exception) |
| 2024-05-16 11:00:09 +0200 | <ski> | .. as well as the tutorial interpreter paper for lambdaProlog (which implements that idea, amongst various other stuff) |
| 2024-05-16 10:59:40 +0200 | <ski> | the "unification under a mixed prefix" paper by Dale Miller is also relevant |
| 2024-05-16 10:58:45 +0200 | ski | read it like last month or so |
| 2024-05-16 10:57:47 +0200 | <int-e> | And I think it's a detail of the pattern unification that I forgot. Yeah I do remember support for constructors too. |
| 2024-05-16 10:56:44 +0200 | <ski> | (i think in some papers, they also allow substituting like numeric literal, (unapplied) data constructors) |
| 2024-05-16 10:56:06 +0200 | <int-e> | Ah, yeah supporting that makes sense to me. |
| 2024-05-16 10:55:54 +0200 | <ski> | (well, more specifically, either with a bound variable, or with a constant. but not with a logic / meta- variable, nor with an arbitrary term) |
| 2024-05-16 10:55:21 +0200 | <ski> | basically `(\x. M) y', substituting `x' with another variable `y' |
| 2024-05-16 10:55:10 +0200 | libertyprime | (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) |