Newest at the top
| 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) |
| 2026-02-07 12:17:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-02-07 12:17:32 +0100 | <ski> | in the case of logic programming (Twelf), you'll be dynamically (similar to dynamic scope, being the operational interpretation of implicational logic programming goals here) adding clauses to your recursive traversal predicates, as you step under the binders |
| 2026-02-07 12:16:07 +0100 | <ski> | so, `x',`f',`f',`x' (four different variables, the language automatically ensures no clashes, capture-free substitution) here will, in the local contexts, act as new temporary data constructors for the expression data type (with `app' and `lam' as the *only* global data constructors, in this example of pure lambda calculus) |
| 2026-02-07 12:13:30 +0100 | <ski> | if you match on and do recursion on an LF term like `app (lam x\ lam f\ f x) (lam f\ lam x\ f x x)' (representing `(\x. \f. f x) (\f. \x. f x x)', where `app : expr (A -> B) -> (expr A -> expr B)' and `lam : (expr A -> expr B) -> expr (A -> B)'), you'll need to step inside the binders, traversing open terms |
| 2026-02-07 12:12:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:09:26 +0100 | ski | was reading, recently, about a (rather restricted, in various ways) dependently typed functional language (Delphin, meant as a different approach to the logic programming approach Twelf to LF terms) for doing computation over LF (Logical Framework) terms, typically used to represent HOAS (that you can *pattern-match* on !) |
| 2026-02-07 12:04:22 +0100 | <ski> | (.. in some cases, one might be able to get away with generating something like `\[a,b,c,...,z] -> ...' for an indefinite number of elements in the list pattern, but still keep the simple static types) |
| 2026-02-07 12:03:13 +0100 | <ski> | provides) |
| 2026-02-07 12:03:07 +0100 | <ski> | (depending on what one'd want to do ?) i think one could possibly do that kind of thing, in MetaML or MetaOCaml, with their quasiquoted code expressions. one'd need to introduce local (quoted) binders for them, though. and, i guess, might need to either resort to dynamically typed code expressions (which at least MetaML provides, i forget about MetaOcaml), or else to dependent typing (which neither of them |
| 2026-02-07 12:02:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-02-07 11:58:53 +0100 | <ski> | .. presumable that F# binding can do that, as well ? |
| 2026-02-07 11:58:24 +0100 | <ski> | i suppose sometimes you'd like to generate fresh variables (perhaps in a loop, or in a recursive computation) .. |
| 2026-02-07 11:57:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 11:48:33 +0100 | <int-e> | jreicher: So basically, it's a different flavor of name clashes than variable capture. |
| 2026-02-07 11:46:35 +0100 | <int-e> | Oh also I think terms are first-order, so there are no binders that could capture variables. |
| 2026-02-07 11:46:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-02-07 11:45:22 +0100 | <int-e> | No, there's no substitution taking place. There's a global namespace. But users may want to generate auxiliary variables without clashing with other auxiliary variables, so as a convenience, fresh name generation is provided by the SMT solver. (At no real cost; the SMT solver will need that functionality internally anyway.) |
| 2026-02-07 11:42:51 +0100 | AlexZenon | (~alzenon@85.174.182.86) |
| 2026-02-07 11:42:27 +0100 | <jreicher> | int-e: I'm not familiar with Z3, but is the generation of fresh names a crappy implementation of capture-avoiding substitution? |
| 2026-02-07 11:42:00 +0100 | qqq | (~qqq@185.54.22.56) (Quit: Lost terminal) |
| 2026-02-07 11:41:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 11:40:14 +0100 | gentauro | less is more |
| 2026-02-07 11:40:09 +0100 | <gentauro> | but I guess if we can do something like that in OCaml for .NET, we should probably be able to mimic that in Haskell right? |
| 2026-02-07 11:38:50 +0100 | gentauro | I want to remove the string variables and just rely on the languages value binding |
| 2026-02-07 11:38:07 +0100 | AlexZenon | (~alzenon@85.174.182.86) (Ping timeout: 240 seconds) |
| 2026-02-07 11:37:54 +0100 | <gentauro> | very succint |
| 2026-02-07 11:37:45 +0100 | <int-e> | (managing your own names is probably suboptimal) |
| 2026-02-07 11:37:37 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-07 11:37:35 +0100 | <gentauro> | probie: I tried to use Code Quotations and Computation Expressions in F# and I end up with this -> https://paste.tomsmeding.com/bi5MGjco |
| 2026-02-07 11:37:24 +0100 | trickard | (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-07 11:37:00 +0100 | <int-e> | probie: Well, in the Z3 API, generating fresh names is tied to function declarations, https://z3prover.github.io/api/html/group__capi.html#ga76d673b3b3f53c1044fd59621b1b8b68 (nice anchor I'm sure it's very stable) |
| 2026-02-07 11:35:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-02-07 11:33:57 +0100 | AlexZenon | (~alzenon@85.174.182.86) |
| 2026-02-07 11:33:03 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 260 seconds) |
| 2026-02-07 11:31:40 +0100 | p3n | (~p3n@217.198.124.246) p3n |
| 2026-02-07 11:31:17 +0100 | <probie> | I mean you certainly could do something like `do { name <- freshName "q1"; mkVar intType name }`, but I don't think you really gain much |