Newest at the top
| 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) |
| 2024-05-16 10:54:55 +0200 | <int-e> | Now what do I google to figure out what beta_0 is :) |
| 2024-05-16 10:54:54 +0200 | ski | idly wonders whether something like L-lambda / higher-order pattern unification, could sensibly be added to GHC |
| 2024-05-16 10:54:09 +0200 | <ski> | (the rules for how it's restricted are somewhat complicated. i read the L-lambda unification paper, and also the details of which unifications are allowed in Twelf, but i don't recall the details of either that well) |
| 2024-05-16 10:53:52 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-16 10:52:10 +0200 | <ski> | it has beta_0 |
| 2024-05-16 10:51:23 +0200 | <ski> | yes, the unification is restricted |
| 2024-05-16 10:48:21 +0200 | <int-e> | You have to restrict beta for this to be decidable (unification can guess arguments of unbounded size so termination doesn't save you). https://www.cs.cmu.edu/~twelf/guide-1-4/twelf_5.html#SEC27 mentions higher-order pattern unification which IIRC doesn't have beta, and also doesn't guess the head of applications. The type checking/inference might have something a bit more fancy though. |
| 2024-05-16 10:48:19 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:d028:ce6d:23c1:c5bb) |
| 2024-05-16 10:45:06 +0200 | chele | (~chele@user/chele) |
| 2024-05-16 10:42:28 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 255 seconds) |
| 2024-05-16 10:41:05 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-05-16 10:40:45 +0200 | _bo | (~bo@198.red-83-56-252.dynamicip.rima-tde.net) (Quit: Leaving) |
| 2024-05-16 10:37:04 +0200 | frumon | (~Frumon@user/Frumon) (Leaving) |
| 2024-05-16 10:32:39 +0200 | danse-nr3 | (~danse-nr3@an-19-164-164.service.infuturo.it) |
| 2024-05-16 10:25:53 +0200 | <ski> | (i may be missing some detail, or getting some details wrong, but that's my impression, from reading some papers about it, semi-recently .. still need to play around more in the implementation, though) |
| 2024-05-16 10:24:19 +0200 | <ski> | (they have unification of lambda terms, up to alpha-, beta-, and eta- conversion. but lambda terms are rather weak, can't compute on sum types, and no recursion. you do computation not with functions, but with predicates/relations, iow logic programming, searching for proofs/values of propositions/types) |
| 2024-05-16 10:22:36 +0200 | <ski> | aiui, this is because (a) they purposely want a rather weak theory, to not assume too much, when representing object systems (logics, type systems, operational semantics, &c.); but also (b) in order to keep unification and type checking decidable |
| 2024-05-16 10:20:54 +0200 | <ski> | yep |
| 2024-05-16 10:20:24 +0200 | <kuribas`> | right, no type 1, type 2, ... as in idris2 |
| 2024-05-16 10:20:15 +0200 | <ski> | it's a fairly conservative/restrictive theory |
| 2024-05-16 10:19:44 +0200 | <ski> | bu there's no infinite tower of sorts |