Logs: liberachat/#haskell
| 2021-06-01 14:05:41 | × | pe200012 quits (~pe200012@119.131.208.84) (Ping timeout: 264 seconds) |
| 2021-06-01 14:06:54 | <geekosaur> | I think so, yes. the unregisterized backend still exists (but isn't included in ghc releases) and is another post-Cmm target |
| 2021-06-01 14:07:37 | <ski> | flowz : hm, ok. anyway, the issue with `data Tree = Root | Node' is that this is declaring an (unparameterized) data type, named `Tree', having two possible shapes (data constructors), `Root' and `Node'. these two are entirely unrelated to your (parameterized) *types* `Root' and `Node' |
| 2021-06-01 14:08:27 | <ski> | flowz : basically, `data Tree = Root | Node' is comparable to `data Pet = Cat | Dog' or `data Bool = False | True' .. it's just a data type, having two values |
| 2021-06-01 14:10:01 | <arrowd> | Ok, then I'm interested in STG -> Cmm part. |
| 2021-06-01 14:10:48 | <ski> | flowz : in any case, it seems misguided to want to check whether you're given a root node, or another node. afaiui, you should already know which one you're passed, in every point of the program |
| 2021-06-01 14:11:59 | × | ku quits (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) (Ping timeout: 268 seconds) |
| 2021-06-01 14:12:10 | <flowz> | I'm starting to think I should go through some tutorials some more before doing even this (comparatively simple) task. There're still some more basic things I haven't grasped enough. I'll do it in some other language as the deadline is approaching rapidly, but still thanks for all the help and pointers :) |
| 2021-06-01 14:13:34 | → | hexfive joins (~eric@50.35.83.177) |
| 2021-06-01 14:13:38 | <ski> | flowz : possibly you could use something like `data Node a = EmptyNode | InternalNode (Node a) [(a,Node a)]', for the internal nodes |
| 2021-06-01 14:16:25 | <ski> | (hm, or maybe you intended `k' to be the same for all internal nodes ?) |
| 2021-06-01 14:21:53 | × | azeem quits (~azeem@dynamic-adsl-94-34-16-203.clienti.tiscali.it) (Read error: Connection reset by peer) |
| 2021-06-01 14:22:50 | → | ikex joins (~ash@user/ikex) |
| 2021-06-01 14:23:51 | <flowz> | ski: yep, k should be the same, and I've also got that included in my actual code. But I'm going to do it in some other language for now, as I've only got a couple of hours left, and there's still some other more time-consuming stuff left to do as well.. Though I'll have a look at doing something with haskell at the next good opportunity, as I find |
| 2021-06-01 14:23:52 | <flowz> | the language quite interesting. Again, thanks for all the help, gtg now |
| 2021-06-01 14:24:10 | × | flowz quits (~flowz@2a01:aea0:dd4:1573:a8:24ac:7db2:5b39) (Quit: Client closed) |
| 2021-06-01 14:26:24 | → | azeem joins (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it) |
| 2021-06-01 14:27:08 | → | adziahel[m] joins (~adziahelm@2001:470:69fc:105::b4d) |
| 2021-06-01 14:28:25 | × | niflce quits (~IceChat95@user/niflce) (Ping timeout: 272 seconds) |
| 2021-06-01 14:30:20 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-01 14:31:39 | → | niflce joins (~IceChat95@user/niflce) |
| 2021-06-01 14:41:09 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 2021-06-01 14:43:13 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Remote host closed the connection) |
| 2021-06-01 14:44:15 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 2021-06-01 14:47:46 | → | haskman joins (~haskman@171.48.41.1) |
| 2021-06-01 14:48:04 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 2021-06-01 14:50:30 | <[exa]> | arrowd: Cmm is a VERY rough lookalike of C, assignment of instructions and registers happens when compiling Cmm |
| 2021-06-01 14:51:04 | <arrowd> | [exa]: So, "registerizing" is basically adding a new backend to Cmm? |
| 2021-06-01 14:51:06 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Client Quit) |
| 2021-06-01 14:51:38 | <[exa]> | I'm not sure if I translated "registerizing" correctly |
| 2021-06-01 14:52:04 | <[exa]> | to start, afaik STG has is own notion of registers that is more or less independent of the actual CPU registers |
| 2021-06-01 14:52:24 | <[exa]> | I guess you are interested in how the decision "what data to put into which CPU register" happens right? |
| 2021-06-01 14:53:19 | <dminuoso> | bor0: By the way, this is a bit of a subtle thing but I decided to let you know anyhow. Depending on how deep your Proof is nested, this could perform not so nicely. |
| 2021-06-01 14:53:24 | <arrowd> | I guess so. I imagined it to be more like a direct mapping between STG registers and real CPU registers. |
| 2021-06-01 14:53:43 | <arrowd> | I took the "registerizing" term from here: https://downloads.haskell.org/~ghc/6.4/docs/html/building/sec-porting-ghc.html |
| 2021-06-01 14:53:55 | <dminuoso> | bor0: This is because while there is a Functor law that states `fmap f . fmap g = fmap (f . g)`, GHC will not use this knowledge and fuse these functions `f` and `g` together. |
| 2021-06-01 14:54:34 | <dminuoso> | bor0: There is however a standard trick to ensure fusion occurs. It's something we can talk about in a later point in time if the need arises. |
| 2021-06-01 14:54:41 | <geekosaur> | arrowd, just to let you know, that's fairly old documentation |
| 2021-06-01 14:55:05 | <arrowd> | I know, but I believe this part is still more or less relevant. |
| 2021-06-01 14:56:40 | <[exa]> | arrowd: no, STG is a virtual machine with virtual registers... there will be some correspondence, but mostly accidental |
| 2021-06-01 14:58:29 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 264 seconds) |
| 2021-06-01 14:58:33 | <arrowd> | I'm confused about this. |
| 2021-06-01 14:58:51 | × | haskman quits (~haskman@171.48.41.1) (Ping timeout: 268 seconds) |
| 2021-06-01 14:59:08 | <arrowd> | LLVM is also a VM in a sense, but only architecturally. There are no traces of "VM-ness" in the final compiled executable. |
| 2021-06-01 14:59:17 | × | dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.1) |
| 2021-06-01 14:59:28 | × | bfrk quits (~Thunderbi@200116b84593d400e083e41adfb91d63.dip.versatel-1u1.de) (Ping timeout: 268 seconds) |
| 2021-06-01 14:59:43 | <arrowd> | Unlike Java, where the compiled binary is a bytecode, which get interpreted/JITed during execution. |
| 2021-06-01 14:59:58 | <arrowd> | STG is like LLVM in this sense, right? |
| 2021-06-01 15:00:14 | <merijn> | Not really |
| 2021-06-01 15:00:23 | → | fart joins (~fart@user/actor) |
| 2021-06-01 15:00:24 | <merijn> | STG is much higher level still |
| 2021-06-01 15:00:35 | <[exa]> | well, in this very rough sense, yes -- it's not interpreted nor JITed, just compiled into next layer |
| 2021-06-01 15:00:55 | <arrowd> | Ok, and the next layer is Cmm? |
| 2021-06-01 15:00:58 | <[exa]> | yes |
| 2021-06-01 15:01:03 | <merijn> | arrowd: FYI, those docs you linked are *ancient* |
| 2021-06-01 15:01:04 | <[exa]> | (I hope) |
| 2021-06-01 15:01:19 | <merijn> | GHC 6.4 is like over a decade old? |
| 2021-06-01 15:01:58 | → | amahl joins (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 2021-06-01 15:02:18 | <arrowd> | Good. Now if I try to port GHC to a new ISA, at what level would I need to work? Cmm, right? |
| 2021-06-01 15:02:35 | <merijn> | Correction, over 16 years old :p |
| 2021-06-01 15:03:20 | <merijn> | arrowd: There's two backends in GHC: the native backend that goes from Cmm to assembly directly and an LLVM backend that converts Cmm to LLVM IR, then uses LLVM for that |
| 2021-06-01 15:03:34 | <arrowd> | I'm talking about NCG right now. |
| 2021-06-01 15:03:48 | <merijn> | arrowd: NCG goes from Cmm to a specific ISA, yes |
| 2021-06-01 15:04:14 | <arrowd> | All right, now I get it. Thanks everyone for explanations. |
| 2021-06-01 15:04:37 | <merijn> | arrowd: See also #ghc for questions about GHC specifics |
| 2021-06-01 15:04:49 | → | dhouthoo joins (~dhouthoo@178-117-36-167.access.telenet.be) |
| 2021-06-01 15:05:43 | → | Bartosz joins (~textual@24.35.90.211) |
| 2021-06-01 15:06:01 | <merijn> | arrowd: angerman has been working on a NCG backend for Apple's M1 (iirc?), so he probably knows where to get the most up-to-date info |
| 2021-06-01 15:08:11 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 2021-06-01 15:08:36 | × | Kaipi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection) |
| 2021-06-01 15:10:51 | × | oxide quits (~lambda@user/oxide) (Ping timeout: 272 seconds) |
| 2021-06-01 15:11:07 | → | Kaipi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 2021-06-01 15:14:46 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 2021-06-01 15:16:48 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) |
| 2021-06-01 15:17:00 | <bor0> | dminuoso, I guess this is related to `join`? If I don't `join`, I end up with `Proof (Proof ...)` |
| 2021-06-01 15:18:10 | <ski> | bor0 : you have a `Monad Proof' instance ? |
| 2021-06-01 15:18:16 | → | oxide joins (~lambda@user/oxide) |
| 2021-06-01 15:18:45 | <bor0> | Nope. Not sure what that would look like, yet. https://github.com/bor0/hoare-imp/blob/master/src/Common.hs#L16-L19 |
| 2021-06-01 15:19:14 | <ski> | imho, it'd probably not be usefuö |
| 2021-06-01 15:19:53 | <boxscape> | bor0 note btw that `x >>= f` is the same as `join (f <$> x)`, which is why it came up in some of those translations |
| 2021-06-01 15:19:56 | <ski> | (i was just wondering, since you mentioned `join' and `Proof (Proof (..))' at the same time ..) |
| 2021-06-01 15:20:53 | → | renzhi joins (~xp@2607:fa49:6500:bc00::e7b) |
| 2021-06-01 15:21:24 | <boxscape> | hm, seems like it would have been Either String (Either String (Proof (..))) |
| 2021-06-01 15:21:25 | → | Guest9 joins (~Guest9@43.241.144.2) |
| 2021-06-01 15:21:26 | <bor0> | Actually, sorry, I meant `Right (Right (Proof ... ))` |
| 2021-06-01 15:21:33 | <boxscape> | or that |
| 2021-06-01 15:21:38 | <ski> | yea, that's another thing |
| 2021-06-01 15:22:27 | <bor0> | But that's probably related to what dminuoso said, "depending how deep your Proof is nested". My expectation is it's only 1 level, right after `Right` - all should be of form `Right (Proof ...)` |
| 2021-06-01 15:23:23 | × | fart quits (~fart@user/actor) (Quit: Connection closed) |
| 2021-06-01 15:23:47 | × | curiousgay quits (~quassel@178.217.208.8) (Ping timeout: 252 seconds) |
| 2021-06-01 15:23:52 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-06-01 15:25:15 | <boxscape> | bor0 I don't think that's what dminuoso meant - to get into Right (Right (Proof (..))) you would have to use (fmap . fmap) f, rather than (fmap f . fmap g). Rather, since `go` is a recursive function, it fmaps again and again, and these fmaps are not automatically optimized into a single fmap |
| 2021-06-01 15:26:09 | × | shailangsa quits (~shailangs@host165-120-169-73.range165-120.btcentralplus.com) () |
| 2021-06-01 15:26:24 | <boxscape> | (and how often it recurs depends on how deep the data structure of the proof is) |
| 2021-06-01 15:26:42 | <bor0> | Ah, was he talking specifically about `go`? My bad then. I thought it was in general, e.g.:https://paste.tomsmeding.com/aCf3hYea |
| 2021-06-01 15:27:06 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:bdf8:f228:7df7:147f) (Quit: WeeChat 2.8) |
| 2021-06-01 15:27:25 | <bor0> | https://paste.tomsmeding.com/H3e0gBbu shows what c1 and c2 are specifically |
| 2021-06-01 15:28:02 | ← | ubh parts (~ubh@2001:470:69fc:105::852) () |
| 2021-06-01 15:28:55 | → | blizzard joins (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) |
| 2021-06-01 15:29:05 | blizzard | is now known as derelict |
All times are in UTC.