Newest at the top
| 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) |
| 2024-05-16 09:42:21 +0200 | oo_miguel | (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 2024-05-16 09:36:41 +0200 | bilegeek | (~bilegeek@2600:1008:b010:1cfe:3776:17b8:1dc2:3fdf) (Quit: Leaving) |
| 2024-05-16 09:33:31 +0200 | <tomsmeding> | but true |
| 2024-05-16 09:33:02 +0200 | <tomsmeding> | with slightly more overhead |
| 2024-05-16 09:32:35 +0200 | <c_wraith> | and a TVar-based approach lets you write much more obviously-correct code that works under the write-light conditions. |
| 2024-05-16 09:30:55 +0200 | bo_ | (~bo@198.red-83-56-252.dynamicip.rima-tde.net) (Ping timeout: 256 seconds) |