Newest at the top
| 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 |
| 2024-05-16 10:19:35 +0200 | <ski> | no, LF is dependently typed to begin with |
| 2024-05-16 10:19:22 +0200 | <kuribas`> | Twelf is dependently typed Elf? |
| 2024-05-16 10:19:01 +0200 | <ski> | (in LF, the Logical Framework system, that Elf is based on, and of which Twelf is an implementation of) |
| 2024-05-16 10:18:19 +0200 | <ski> | there are three levels, values, types, and kinds |
| 2024-05-16 10:17:40 +0200 | <kuribas`> | ski: so types are not values then? |
| 2024-05-16 10:16:46 +0200 | <ski> | kuribas` : aiui, no parametric polymorphism, types only depend on values, not types; iirc, in original implementation, they had that, but they didn't include it in the reworked implementation (yet at least), because the theory for it was unclear |
| 2024-05-16 10:15:27 +0200 | danza | (~francesco@an-19-164-164.service.infuturo.it) (Remote host closed the connection) |
| 2024-05-16 10:03:14 +0200 | danza | (~francesco@an-19-164-164.service.infuturo.it) |
| 2024-05-16 10:02:54 +0200 | titibandit | (~user@user/titibandit) |
| 2024-05-16 10:02:03 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-05-16 09:56:54 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-05-16 09:49:30 +0200 | <kuribas`> | https://twelf.org/wiki/equality/ |
| 2024-05-16 09:46:51 +0200 | <kuribas`> | perhaps offtopic, but I looked at twelf, and I am surprised you need to reinvent equality (refl, cong, ...) for each datatype. |
| 2024-05-16 09:44:11 +0200 | cfricke | (~cfricke@user/cfricke) |