00:00:00 --- log: started forth/21.04.28 00:13:00 --- join: andrei-n joined #forth 01:19:32 --- join: vesankellot joined #forth 01:25:53 --- part: vesankellot left #forth 01:41:35 --- quit: jimt[m] (Quit: Bridge terminating on SIGTERM) 01:41:35 --- quit: jevinskie[m] (Quit: Bridge terminating on SIGTERM) 01:41:44 --- quit: siraben (Quit: Bridge terminating on SIGTERM) 01:49:35 --- join: jevinskie[m] joined #forth 01:57:47 --- quit: mtsd (Quit: Leaving) 01:58:34 --- join: jimt[m] joined #forth 01:58:34 --- join: siraben joined #forth 02:42:24 --- join: mtsd joined #forth 03:04:15 --- join: jedb_ joined #forth 03:05:23 --- quit: jedb (Ping timeout: 252 seconds) 03:05:28 --- join: jedb__ joined #forth 03:08:27 --- quit: jedb_ (Ping timeout: 246 seconds) 03:21:30 --- join: f-a joined #forth 03:30:55 siraben: I have not had a ton of time for recreational programming recently but I have been getting into scheme slowly in guile 03:31:42 Was out all last night looking for a friend's cat 03:31:50 Probably stolen 03:32:18 It's interesting so far, not sure what to make of it yet 03:32:30 I try not to pass judgement on languages until I really understand them 03:33:59 What scared and intrigued me a little was seeing all cores running on a program that got stuck! 03:40:28 veltas: I think I'm ever so gradually beginning to see some of the usefulness of Lisp/scheme. 03:40:43 Not super clearly yet, but something is "teasing at me." 03:41:42 What's still got my head going in circles is DKordic's lambda calculus presenttion he linked a few days ago. 03:41:57 That still just feels like a game with extremely arbitrary rules to me. 03:43:36 And the examples they give seem like they're chosen to be as confusing as possible - sort of like those arithmetic riddles you see online sometimes where they leave out the parentheses and write things in the most obtuse way possible - I think the whole point of those is to make people argue about them. 03:44:18 Like they'll give an LC expression where x appears in like three different independent ways. 03:44:25 Why would anyone even write something like that???? 03:44:36 Use different symbols so that it's clear. 03:45:55 And there's utterly no consistency. This feature associates left, that feature associates right, nothing is commutative, etc. etc. It feels like the rules were DESIGNED to make it unwieldy and hard to learn. 03:46:24 But there must be something to it; DKordic seemed beyond excited over it the other day. 03:46:50 --- part: f-a left #forth 03:48:05 I think, for example, it would be easier to parse if they just nixed the left and right association rules and just required parentheses to designate that. 03:49:04 I can already tell that as I learn to deal with the things I'm probably going to be re-writing all of them I encounter in that way - insert the parentheses so I can SEE the association. 03:50:18 I just feel like someone (Church, I guess) got carried away with brevity. 03:56:09 And regarding free, bound, and binding variables, I *think* it's the lambda that makes the variable(s) after it bound, but I'm not sure it actually SAID THAT anywhere. 04:02:01 KipIngram: (lambda (x) e), then when x occurs free in e, it is bound by the outer lambda 04:02:38 Yes, that's what I'd inferred, more or less. But only within e, right? 04:02:57 KipIngram: hm, I think lambda calculus notation is terse but it's precise also. application associates left so x y z means (x y) z 04:03:01 Right. 04:03:10 Oh I'm sure it is (terse). 04:03:26 too many parents would make hard to write I suppose 04:03:29 parens 04:03:31 I guess I'm thinking perhaps a little too terse, given how contradictory to most of mathematics some of the rules are. 04:03:46 Could you link to the presentation again? 04:03:59 Yeah it funnily enough breaks with traditional mathematical notation 04:04:01 Especiaslly the fact that different associtivity changes the meaning - that just doesn't happen very much in math. 04:04:22 A*B*C = (A*B)*C = A*(B*C) etc. But not in LC. 04:04:32 It's because there's no binary operator here, everything is prefix 04:04:39 https://www.cs.helsinki.fi/u/jllang/Introduction_to_Lambda_Calculus.pdf 04:04:58 I mean to say, the only binary operation is really application, which is invisible 04:05:11 a(bc) =/= (ab)c 04:05:35 That makes sense - I'm just noting it's not how most of math trains your brain. 04:06:23 It's just another version of the same problem some folks have getting comfortable with the lack of commutivity in matrix multiplication. 04:07:37 KipIngram: wow, that seems like a lot for a presentation 04:07:58 I've certainly seem far simpler explanations of the lambda calculus, showing how it can be used to actually compute as well 04:08:00 I feel like the presentation could profit from some more examples. But examples that actually show a practical use case, rather than examples chosen to force you to carefully invoke the rules to be sure you get it right. 04:08:22 You know, some where I can clearly see what it's telling me. 04:08:39 KipIngram: I think this is great: https://mroman42.github.io/mikrokosmos/tutorial.html 04:08:59 For me it was when LC really clicked, with all those examples of it actually doing stuff 04:09:35 Oh, cool - good. Another one - maybe that one will sink in better. :-) 04:10:04 I'm griping over this and I shouldn't be - I'm just used to understanding things fairly well on first reading, and I'm not getting that from the one I linked. 04:10:38 I think it might be because of all the non-LC stuff in the presentation as well! 04:11:13 it looks more appropriate for logicians or mathematicians 04:11:30 Oh, I like this one better already. 04:12:00 That first bulleted list right at the top already conveys a lot. 04:12:11 Do try the evaluation buttons, it's slow only on the first click when it loads stuff I tihnk 04:12:12 think* 04:14:44 also, numbers are not condemned to be unary in LC, a binary encoding is possible with all the log n bounds, but at that rate you might as well use native integers or bignums 04:15:13 What's going on in that first evaluate? Where does the second lambda come from and why are there so many a's? 04:15:18 What's interesting, rather, is that the encoding of natural numbers is enough to do all the usual arithmetic, in theory. 04:15:24 That's the Church encoding of 6 04:15:35 I think it should print out 6 if it detects the Church encoding 04:16:06 λa.λb.a (a (a (a (a (a b))))) can be thought of as, take a function a and apply it to an argument b 6 times 04:17:03 I guess they'll avoid presenting, say, 1427 that way. 04:17:31 Hah, certainly. 04:18:53 KipIngram: funny story is that when Church invented that encoding for natural numbers, he had a hard time figuring out how to write the predecessor function and almost gave up on LC, but his grad student (Kleene, I think), had it come to him during a dentist visit 04:21:30 "Kleene allegedly realized how to define the predecessor function (as given in the previous section: Kleene had earlier defined the predecessor function using an encoding of numerals different from those of Church) while at the dentist for the removal of two wisdom teeth" 04:21:46 https://iep.utm.edu/lambda-calculi/ 04:23:29 veltas: that's a good idea, to not judge a language until one really understands them 04:23:37 I struggled with Forth initially but stuck through it to see the other side 04:25:15 Forth was an instant love for me, because most of my programming prior to finding it had been on an HP-41CV calculator. 04:25:30 At first Forth was just an "RPN language" - that was the drawing card for me. 04:25:48 But it didn't take long for me to see its... "further beauty." :-) 04:30:20 On the other hand, my first reaction to Lisp, long long ago, was "yuck - way too many parentheses..." :-) 04:30:57 But that's probably because Forth had spoiled me on that front. 04:31:06 That's the whole beauty of RPN, actually. 04:31:54 Of course, Lisp's ability to add two numbers, or three, or 300 is pretty cool. 04:43:29 --- join: tech_exorcist joined #forth 05:06:13 --- nick: jedb__ -> jedb 05:07:13 --- quit: Zarutian_HTC (Remote host closed the connection) 06:41:57 --- quit: lonjil (Quit: No Ping reply in 180 seconds.) 06:44:17 --- quit: dave0 (Quit: dave's not here) 06:44:33 --- join: lonjil joined #forth 06:48:58 --- join: user51 joined #forth 06:50:13 --- part: user51 left #forth 07:25:50 You know, it's a bit of a shame that Forth doesn't allow nested namespaces like Lisp does. Then I could put all my "helper words" inside the scope of the word they're helping, rather than require a separate mechanism for hiding or otherwise removing helper names. I must say, though, even if the machinery would allow that, I'd really hate having the name of a word "up here" and then the (short) code for the 07:25:52 word an the far side of a big slug of helper word definitions. I think my .: / .wipe mechanism is about as simple as it gets, but it is still "something extra" that I have to put in. 07:27:01 There's just an elegance to the Lisp approach that we're missing in Forth. 07:54:09 some forths have namespacing, i think factor handles the non-built-in as hashtables but don't remember if it supports modifying and juggling them at runtime 07:55:38 i mainly use forth as a toy or exercise on fairly capable hardware so crude prefixing hasn't become a problem yet 07:57:49 Crude prefixing? I don't quite follow. 07:58:13 e.g. : helper-wordname ... ; 08:01:05 if you're implementing your own system it might be interesting to experiment with chaining dictionaries in a list and figure out some way to connect metadata to it 08:17:19 Oh, got it. Actual prefixes. :-) 08:18:53 I do something like you described already. My dictionary is one continuous range of memory, but within that I have multip linked lists, each associated with a specific vocabulary. At any given time I maintain a higher level linked list, of vocabularies, that specify my search path. 08:19:40 This will let me do what I described, but in my previous system I had a way of actually removing the names and links of temporary words completely from the dictionary, leaving only the CFA/PFA pair and the implementtion body after the need for the words ended. 08:20:38 This time, on my new implementation, I won't be recovering the RAM the names and links occupy, but I do intend to "unlink" temporary words from their linked list when I'm done with them. 08:21:30 That will be a feature of the base system, as is the ability to search the structure I described above. Actual ability to define and manage vocaulary words, though, is something I will add later on. 08:22:19 After I am far enough along that I can edit Forth source into disk blocks and use them to extend the system. 09:29:03 siraben: huh, I haven't thought about a topological interpretation like that at all... tbh my knowledge of topology is pretty much limited to what's covered in the chapters of HoTT not about topology, heh 09:35:47 one way to solve the problem is to tag pointers as pointers then garbage collect at the end 09:36:04 although that adds a good bit of complexity 10:03:56 remexre: at the basic level, topology looks like glorified set theory because the conditions to be a topological space talk only about a family a subsets of a set X being closed under finite intersection and arbitrary union 10:23:36 --- quit: tech_exorcist (Quit: tech_exorcist) 10:24:06 --- join: tech_exorcist joined #forth 10:44:50 --- quit: tech_exorcist (Remote host closed the connection) 10:47:41 --- join: tech_exorcist joined #forth 12:21:39 --- join: f-a joined #forth 12:42:50 --- quit: gravicappa (Ping timeout: 268 seconds) 12:55:08 --- quit: andrei-n (Quit: Leaving) 13:19:03 --- quit: mtsd (Quit: Leaving) 13:22:38 --- quit: f-a (Ping timeout: 252 seconds) 13:22:47 --- join: f-a joined #forth 13:27:45 --- quit: f-a (Quit: leaving) 14:06:05 --- quit: tech_exorcist (Ping timeout: 268 seconds) 15:38:11 --- join: dave0 joined #forth 15:38:27 maw 15:40:31 Evening. 15:40:53 hey KipIngram 16:27:50 --- quit: jn__ (Ping timeout: 252 seconds) 16:28:57 --- join: jn__ joined #forth 17:54:26 --- quit: dave0 (Quit: dave's not here) 17:58:47 So I'm starting to get at least a few of the lambda calculus quiz problems right. 17:59:20 I haven't quite gotten it pat for some of the "orderings" of things. 18:56:54 --- join: boru` joined #forth 18:56:57 --- quit: boru (Disconnected by services) 18:56:59 --- nick: boru` -> boru 19:41:29 --- quit: sts-q (Ping timeout: 276 seconds) 19:46:59 --- join: sts-q joined #forth 20:11:31 --- join: dave0 joined #forth 20:13:00 maw 20:19:34 --- join: jedb_ joined #forth 20:22:08 --- quit: jedb (Ping timeout: 252 seconds) 20:47:52 --- nick: jedb_ -> jedb 20:50:32 --- join: andrei-n joined #forth 21:10:58 --- quit: Kumool (Ping timeout: 268 seconds) 21:11:27 --- join: Kumool joined #forth 21:18:02 --- join: gravicappa joined #forth 22:16:51 --- quit: gravicappa (Ping timeout: 260 seconds) 23:09:35 --- join: gravicappa joined #forth 23:43:59 --- quit: gravicappa (Ping timeout: 252 seconds) 23:59:59 --- log: ended forth/21.04.28