Newest at the top
| 2026-02-07 14:00:58 +0100 | comonad | (~comonad@pd9e072e5.dip0.t-ipconnect.de) |
| 2026-02-07 13:59:08 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 13:59:08 +0100 | trickard_ | trickard |
| 2026-02-07 13:56:14 +0100 | Square2 | (~Square@user/square) Square |
| 2026-02-07 13:48:39 +0100 | <mesaoptimizer> | int-e: recommended reading to understand SMT solvers? |
| 2026-02-07 13:48:08 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-02-07 13:47:55 +0100 | emmanuelux | (~em@user/emmanuelux) (Quit: bye) |
| 2026-02-07 13:46:17 +0100 | <mesaoptimizer> | gentauro: I'm trying to patch microhs / mcabal using Gemini 3 Pro to be able to build `http-conduit`, and I must say, I'm not impressed |
| 2026-02-07 13:45:19 +0100 | comonad | (~comonad@pd9e072e5.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2026-02-07 13:44:23 +0100 | <mesaoptimizer> | jreicher: I am on #emacs but never read it |
| 2026-02-07 13:43:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 13:40:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-02-07 13:37:14 +0100 | Pozyomka | (~pyon@user/pyon) pyon |
| 2026-02-07 13:35:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 13:32:26 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-02-07 13:32:25 +0100 | comonad | (~comonad@pd9e072e5.dip0.t-ipconnect.de) |
| 2026-02-07 13:31:41 +0100 | Pozyomka | (~pyon@user/pyon) (Quit: WeeChat 4.8.1) |
| 2026-02-07 13:30:14 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-02-07 13:26:10 +0100 | comonad | (~comonad@p200300d02722ae00dce4ce9451b59974.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2026-02-07 13:23:52 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-02-07 13:17:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 13:06:59 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-02-07 13:06:07 +0100 | jreicher | (~joelr@user/jreicher) (Remote host closed the connection) |
| 2026-02-07 13:06:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-07 13:05:22 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-02-07 13:00:30 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-02-07 12:58:08 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:55:07 +0100 | <ski> | (i was recently starting to formulate (optimized) CPS-transformation, first in lambdaProlog (which also has matching on HOAS, but not dependent types), then trying to do it in Twelf, for comparision .. ran out of steam, after a while, fighting with it to accept some parts, though) |
| 2026-02-07 12:53:45 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-02-07 12:50:53 +0100 | <ski> | .. i can't keep from feeling like there ought to be a way to address those concerns more directly .. rather than resorting to going to a different (functional) computational model. Twelf is the only dependently typed logic programming language i'm aware of, and it would seem to be a shame to not further develop that |
| 2026-02-07 12:50:36 +0100 | Beowulf | (florian@2a01:4f9:3b:2d56::2) |
| 2026-02-07 12:49:25 +0100 | <ski> | the issue being limitations in reasoning about local parameters (data constructors), and local assumptions, for the mode-checking. and, perhaps, also some limitations in doing (effectively) anonymous predicates, e.g. extending an accumulator predicate parameter -- and associated reasoning about mode for such higher-order predicates |
| 2026-02-07 12:47:30 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-02-07 12:47:13 +0100 | <ski> | said above (meta-)proof checking) |
| 2026-02-07 12:47:06 +0100 | <ski> | one of the reasons they stated for developing Delphin (rather than Twelf), was a claim of having trouble with some kinda of higher-order programming. afaict, what they mean by this is not lack of support for higher-order predicates, per se, but rather lack of adequate support for the static mode&determinism *checking* (which is optional (from a computational standpoint), but essential for when you want to do |
| 2026-02-07 12:46:32 +0100 | Beowulf | (florian@2a01:4f9:3b:2d56::2) (Quit: = "") |
| 2026-02-07 12:44:18 +0100 | jreicher | (~joelr@user/jreicher) (Quit: In transit) |
| 2026-02-07 12:42:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:35:26 +0100 | <ski> | it also has facilities to be able to state such theorems, and let a theorem-prover (in the language implementation) search for a proof (and realize it as a recursive predicate) |
| 2026-02-07 12:34:27 +0100 | <ski> | so, the system has facilities to do this (meta-proof) checking of modes, in order to ensure that the predicate whose definition encodes your proof actually proves the intended thing (e.g. that if an (object-language) term has some type, and you reduce the term one step, then it still has that type) |
| 2026-02-07 12:33:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-02-07 12:32:43 +0100 | <ski> | mode&determinism declaration on the predicate (if you will, ensuring that the relation is functional) |
| 2026-02-07 12:32:37 +0100 | <ski> | one of the interesting things you can do in Twelf, is to encode a proof as a relation. to actually check that the proof is valid, you then need to check that for each possible input for some designated input parameters to the relation/predicate, there is a related output asssigned to the output parameter(s), such that the (dependently typed) relation holds. from a logic programming standpoint, this is a |
| 2026-02-07 12:28:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:24:11 +0100 | _JusSx_ | (~jussx@78.211.193.248) |
| 2026-02-07 12:23:30 +0100 | <ski> | schematic variables to fill in with other LF terms) |
| 2026-02-07 12:23:24 +0100 | <ski> | (ooc, they also had effectively a monad, in the language, for computations which will result in a value term of an LF type. the type `<T>' is short for `T * unit', which is short for `exists _ : T. unit'. in `T * U', `U' is not allowed to be an LF type, but `T' is. the reason is that they want all expressions of LF type to not have any computational (Delphin-level) subexpressions, only an LF-term, with some |
| 2026-02-07 12:22:25 +0100 | _JusSx_ | (~jussx@78.210.148.66) (Ping timeout: 245 seconds) |
| 2026-02-07 12:19:36 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2026-02-07 12:19:19 +0100 | <ski> | in the case of the functional programming (Delphin), they choose to instead allow you to add patterns for "parameters" of (LF) types, in your `case'-`of' expressions (and then you'd often also pass some kind of accumulating substitution function, or similar, to the traversal function, initializing it to the empty function at the top call) |