Logs: freenode/#haskell
| 2021-03-29 10:42:55 | → | ubert joins (~Thunderbi@p200300ecdf25d94cca5b76fffe29f233.dip0.t-ipconnect.de) |
| 2021-03-29 10:43:38 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 2021-03-29 10:43:43 | <bor0> | I have a PropCalc data type defined as `data PropCalc = P | Q | R | Not PropCalc | And PropCalc PropCalc | Or PropCalc PropCalc | Imp PropCalc PropCalc`. I want to create a function `apply` so that it modifies an element in a specific order. E.g., apply 1 (\x -> P) (And Q R) should return (And P R). Is there an elegant/easy way of doing this? One way I thought of was to create between trees and list representations |
| 2021-03-29 10:43:44 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 252 seconds) |
| 2021-03-29 10:44:19 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-29 10:44:36 | <ski> | what's the `1' for ? |
| 2021-03-29 10:44:46 | <bor0> | Position of the tree node |
| 2021-03-29 10:45:23 | <bor0> | For unary operators it is easy: go n pos f (Not x) | n == pos = Not (f x) and go n pos f (Not x) = go (n + 1) pos f (Not x). Things get trickier when I have to deal with `And` |
| 2021-03-29 10:45:48 | <bor0> | I don't know the count of the nodes in advance... maybe I should calculate that in the interim |
| 2021-03-29 10:48:03 | <ski> | hm. numbered leaf ? |
| 2021-03-29 10:48:51 | <bor0> | Yeah.. that could also work - to convert every node in the structure from Node to (Int, Node) |
| 2021-03-29 10:48:59 | <ski> | i'm wondering if you could avoid referring to things to replace by numbers, at all |
| 2021-03-29 10:49:08 | <ski> | if you could, that would probably be nicer |
| 2021-03-29 10:49:36 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-03-29 10:49:45 | <bor0> | Basically, I'm trying to provide a toy implementation of Gentzen's propositional calculus. In it, we can replace some rules (e.g. ~~P with P). But I want to be able to specify at which point do I want to make this replacement |
| 2021-03-29 10:49:51 | <ski> | (but if you really want to or have to use numbering, that's also possible .. you'd thread a state through the recursion. can be done manually. state-monad would be easier, though, i think) |
| 2021-03-29 10:50:05 | <bor0> | Maybe there is a much more elegant way to achieve this than what I'm trying to do now |
| 2021-03-29 10:50:07 | <ski> | hm, ok |
| 2021-03-29 10:50:14 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-29 10:50:19 | <ski> | replace an arbitrary subformula ? |
| 2021-03-29 10:50:29 | <ski> | or just replace leaves (that is, propositional variables) ? |
| 2021-03-29 10:50:48 | <ski> | and, replace all occurances of a particular propositional variable ? or just a single occurance ? |
| 2021-03-29 10:50:50 | <bor0> | Yeah. I was trying to map some of the examples used in Godel Escher Bach, and in there he just replaces an arbitrary subformula |
| 2021-03-29 10:51:15 | <ski> | instead of using number, perhaps you could use a path to the formula you want to replace |
| 2021-03-29 10:51:40 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Error from remote client") |
| 2021-03-29 10:52:31 | <bor0> | So, let's say I want to convert (Imp (And P Q) Q) to (Imp (And (~~P) Q) Q). How would that work with this path approach? |
| 2021-03-29 10:52:58 | <ski> | hm, also, i'm wondering if it's Genzen's Natural Deductin, or perhaps his Sequent Calculus |
| 2021-03-29 10:53:10 | <ski> | s/Deductin/Deduction/ |
| 2021-03-29 10:54:05 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-03-29 10:54:07 | <ski> | well, in that case, the path would consist of two components, one indicating the left subtree of `Imp', and the next indicating the left subtree of `And' |
| 2021-03-29 10:54:26 | <ski> | the indicators could be numbers. could also be symbolic, if you prefer |
| 2021-03-29 10:54:27 | <ph88> | i'm using tasty-hunit and for one test i would like to change the current working directory. How can i find my project directory or test directory ?? (from these i can calculate the working directory i need) |
| 2021-03-29 10:54:28 | <bor0> | Hm, I think that's not specified.. the way he uses the rules are like https://imgur.com/a/l8oV8p0 |
| 2021-03-29 10:54:49 | <bor0> | Note how he applied contrapositive to the left argument of Imp |
| 2021-03-29 10:54:59 | <merijn> | ph88: You can't reall, tbh |
| 2021-03-29 10:55:12 | <ph88> | hows that ? |
| 2021-03-29 10:55:13 | <bor0> | s/contrapositive/double-tilde/ |
| 2021-03-29 10:55:20 | <merijn> | ph88: What's in this working directory? Input files for tests? |
| 2021-03-29 10:55:42 | <ski> | bor0 : hm, that looks like some Hilbert-style axiomatix system. my condoleances |
| 2021-03-29 10:55:54 | <ph88> | the input files of the test are in a specific directory. I want to set the current working directory to this directory |
| 2021-03-29 10:55:56 | <bor0> | :D |
| 2021-03-29 10:55:57 | <ski> | hm, or maybe it isn't |
| 2021-03-29 10:56:04 | → | dandart joins (~Thunderbi@home.dandart.co.uk) |
| 2021-03-29 10:56:06 | <ski> | maybe that's just a deduction tree |
| 2021-03-29 10:56:16 | <bor0> | Looks like it |
| 2021-03-29 10:56:45 | <ski> | although .. i don't think it's either NK or LK |
| 2021-03-29 10:56:48 | <merijn> | ph88: When installing package, the source isn't (normally) installed, so cabal doesn't allow you to depend on the layout of your source directory/ies |
| 2021-03-29 10:56:56 | <merijn> | ph88: You probably want data-files instead: https://cabal.readthedocs.io/en/latest/cabal-package.html?highlight=getdatafile#accessing-data-files-from-package-code |
| 2021-03-29 10:57:09 | <bor0> | OK, so by path you mean accept a list like [Left, Left, Right] which would pinpoint to exactly the node we want? |
| 2021-03-29 10:57:31 | <ph88> | merijn, i need to install my package for i can run its tests ? |
| 2021-03-29 10:57:32 | <bor0> | and when I reach [] I just apply f in there |
| 2021-03-29 10:58:09 | <ski> | bor0 : "Note how he applied contrapositive to the left argument of Imp" -- i don't think that's what he did, actually |
| 2021-03-29 10:58:14 | <merijn> | ph88: No, you don't have to install. But cabal doesn't allow you to ask "what is the path to the source directory?" because that question is non-sensical when packages get installed |
| 2021-03-29 10:58:16 | <ski> | hm |
| 2021-03-29 10:58:24 | <bor0> | ski, sorry. I amended that with s/contrapositive/double-tilde/ |
| 2021-03-29 10:58:27 | <bor0> | You probably missed that |
| 2021-03-29 10:58:34 | <ski> | ah, just noticed your correction |
| 2021-03-29 10:58:37 | <merijn> | ph88: Instead, you should use the data-files field and getDataFile to access read-only data from your code |
| 2021-03-29 10:58:41 | <ski> | sure, yea |
| 2021-03-29 10:59:07 | <merijn> | ph88: See the link I sent |
| 2021-03-29 10:59:18 | <bor0> | I like this path approach. It's much better than converting between list/tree representations and the numbering one. Thanks! Will try doing that. |
| 2021-03-29 10:59:24 | <ski> | bor0 : "OK, so by path you mean .. " -- yes, something like that. that would be much easier to interpret, in `Apply' |
| 2021-03-29 10:59:34 | <ph88> | oki |
| 2021-03-29 10:59:37 | <ph88> | thanks |
| 2021-03-29 11:00:32 | <ski> | bor0 : if you go symbolic, i guess for `Not', you'd have a `Down' rather than arbitrarily choosing between `Left' and `Right' |
| 2021-03-29 11:00:36 | <bor0> | Yes! |
| 2021-03-29 11:00:37 | → | idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-03-29 11:00:42 | <bor0> | I just hit that and started asking a question lol |
| 2021-03-29 11:01:03 | <ski> | (one could have `ImpLeft',`AndLeft' and so on .. but it probably doesn't make too much of a difference) |
| 2021-03-29 11:01:17 | <ph88> | merijn, what do you think about this solution ? https://stackoverflow.com/a/21033253 since i know the structure of my project i can calculate the directory from any source file |
| 2021-03-29 11:01:33 | <ski> | bor0 : heh, nice that i anticipated that, then :P |
| 2021-03-29 11:01:46 | <bor0> | ski, in terms of front-end experience, the numbers make most sense. but in terms of simple implementation, I think [Left, Right, Down] will be acceptable |
| 2021-03-29 11:02:05 | <ski> | you could obviously convert between the formats, if needed |
| 2021-03-29 11:02:05 | <bor0> | (After all, it's probably only myself who will be the front-end user of this :D) |
| 2021-03-29 11:02:06 | → | ixlun joins (~matthew@109.249.184.133) |
| 2021-03-29 11:02:34 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 2021-03-29 11:02:39 | <merijn> | ph88: I think it's terrible and dear god, please don't ever do that in a package you plan for other people to use... >.> |
| 2021-03-29 11:02:47 | <ski> | (btw, "switcheroo" is a weird name ..) |
| 2021-03-29 11:02:50 | → | puke joins (~vroom@217.138.252.168) |
| 2021-03-29 11:02:50 | <ph88> | why terrible ?? |
| 2021-03-29 11:03:12 | <merijn> | ph88: Because you're hardcoding the compile time source path in your code |
| 2021-03-29 11:03:21 | <bor0> | In https://en.wikipedia.org/wiki/Switcheroo there's some clarification: "In his book G�del, Escher, Bach, Douglas Hofstadter names one of the rules in his version of propositional calculus the Switcheroo Rule, apparently in honour of an Albanian railroad engineer, name Q. Q. Switcheroo, who "worked in logic on the siding".[5] This is in reality the material implication." |
| 2021-03-29 11:03:21 | × | stree quits (~stree@68.36.8.116) (Quit: Caught exception) |
| 2021-03-29 11:03:21 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Remote host closed the connection) |
| 2021-03-29 11:03:38 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 2021-03-29 11:03:48 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-29 11:03:49 | <merijn> | ph88: When someone tries to install your package, that path will almost certainly be in a temporary directory that gets deleted, so now the installed executable refers to a non-existent temporary path |
| 2021-03-29 11:04:07 | <merijn> | Not to mention CPP is a terrible extension >.> |
| 2021-03-29 11:04:17 | <ski> | (bor0 : i have read GEB, but it was a long time ago, so i don't remember much specifics of the formal systems in it) |
| 2021-03-29 11:04:25 | <merijn> | Where as data-files is literally less work *and* more robust/safer |
| 2021-03-29 11:04:28 | <ph88> | merijn, i figured since it's just for testing it's ok |
| 2021-03-29 11:04:49 | × | dandart quits (~Thunderbi@home.dandart.co.uk) (Quit: dandart) |
| 2021-03-29 11:04:57 | <bor0> | ski, yeah. So I'm trying to implement in Haskell his toy implementations of Gentzen's Propositional Calculus and later I want to also tackle Peano's arithmetic (TNT) |
| 2021-03-29 11:05:25 | <ph88> | merijn, what about data-files ? do i have to list each individual file ? |
| 2021-03-29 11:06:45 | <ph88> | oh wildcards cool |
| 2021-03-29 11:07:27 | ski | nods to bor0 |
| 2021-03-29 11:07:52 | <ski> | bor0 : the basic rules of NK or LK aren't terribly complicated, either, btw |
| 2021-03-29 11:08:05 | <bor0> | What's NK and LK? |
| 2021-03-29 11:08:14 | <ski> | (NK is the Natural Deduction version. LK is the Sequent Calculus version) |
| 2021-03-29 11:10:11 | <bor0> | While I have your interest here, could use your :eyes: for a quick review :) https://github.com/bor0/misc/blob/master/2021/Gentzen.hs |
All times are in UTC.