Newest at the top
| 2024-05-16 12:50:46 +0200 | <tomsmeding> | I wonder if your :- parsing is working though; should it not parse a '-'? |
| 2024-05-16 12:49:42 +0200 | <tomsmeding> | note the type of Postfix here https://hackage.haskell.org/package/parser-combinators-1.3.0/docs/Control-Monad-Combinators-Expr.h… |
| 2024-05-16 12:49:14 +0200 | <tomsmeding> | famubu: `Postfix rep` doesn't work? |
| 2024-05-16 12:49:06 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:d028:ce6d:23c1:c5bb) (Remote host closed the connection) |
| 2024-05-16 12:44:01 +0200 | yin | (~yin@user/zero) |
| 2024-05-16 12:41:39 +0200 | <famubu> | where they mention it for `+`, and `*`. But still couldn't figure how to make it more general. |
| 2024-05-16 12:41:15 +0200 | <famubu> | Saw this (parsec): https://stackoverflow.com/questions/9020254/using-parsec-to-parse-regular-expressions |
| 2024-05-16 12:38:31 +0200 | <famubu> | I wasn't sure how to add `rep` to the operator table (`optab`) |
| 2024-05-16 12:38:01 +0200 | <famubu> | This is what I have: https://bpa.st/5O4Q |
| 2024-05-16 12:37:33 +0200 | <famubu> | Hi. I had been trying to make a megaparsec parser to parse regular expression. I got atoms and concatenation working. Now I'm trying to get repetition like `r{2,4}` but couldn't finish it. |
| 2024-05-16 12:33:26 +0200 | famubu | (~julinuser@user/famubu) |
| 2024-05-16 12:28:55 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 260 seconds) |
| 2024-05-16 12:26:29 +0200 | patrl | (~patrl@user/patrl) (Remote host closed the connection) |
| 2024-05-16 12:24:05 +0200 | patrl | (~patrl@user/patrl) |
| 2024-05-16 12:23:19 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-05-16 12:21:37 +0200 | patrl | (~patrl@user/patrl) (Remote host closed the connection) |
| 2024-05-16 12:20:48 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-05-16 12:13:28 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-05-16 12:08:51 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 255 seconds) |
| 2024-05-16 12:02:08 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1) |
| 2024-05-16 12:01:38 +0200 | danse-nr3 | (~danse-nr3@an-19-164-164.service.infuturo.it) (Ping timeout: 268 seconds) |
| 2024-05-16 11:58:52 +0200 | libertyprime | (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) (Remote host closed the connection) |
| 2024-05-16 11:56:36 +0200 | pie_ | (~pie_bnc@user/pie/x-2818909) |
| 2024-05-16 11:56:18 +0200 | pie_ | (~pie_bnc@user/pie/x-2818909) () |
| 2024-05-16 11:53:45 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-05-16 11:52:10 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 2024-05-16 11:49:41 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-05-16 11:46:26 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-05-16 11:42:40 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:e4f7:dd84:71b6:db6) |
| 2024-05-16 11:38:38 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
| 2024-05-16 11:38:23 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-05-16 11:37:44 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2024-05-16 11:37:44 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 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/ |