00:00:00 --- log: started forth/20.07.31 00:11:35 --- join: xek joined #forth 00:11:46 --- quit: jsoft (Ping timeout: 240 seconds) 01:49:44 --- quit: xek (Ping timeout: 240 seconds) 03:14:22 --- quit: deesix (Ping timeout: 264 seconds) 03:14:38 --- join: deesix joined #forth 03:14:49 --- join: dddddd_ joined #forth 03:14:59 --- quit: dddddd (Ping timeout: 264 seconds) 03:15:16 --- nick: dddddd_ -> dddddd 03:24:05 --- join: proteus-guy joined #forth 03:37:07 --- join: xek joined #forth 04:12:23 --- quit: _whitelogger (Remote host closed the connection) 04:15:03 --- join: jsoft joined #forth 04:15:23 --- join: _whitelogger joined #forth 04:54:15 --- quit: deesix (Ping timeout: 256 seconds) 04:54:56 --- quit: dddddd (Ping timeout: 240 seconds) 05:04:39 --- join: dddddd joined #forth 05:04:56 --- join: deesix joined #forth 05:53:04 --- join: Zarutian_HTC joined #forth 06:07:36 --- quit: dave0 (Quit: dave's not here) 06:51:08 --- quit: xek (Ping timeout: 246 seconds) 07:10:34 --- quit: proteus-guy (Ping timeout: 260 seconds) 07:22:57 --- join: proteus-guy joined #forth 07:48:34 --- quit: Zarutian_HTC (Ping timeout: 264 seconds) 08:05:24 --- quit: proteus-guy (Ping timeout: 260 seconds) 08:26:32 --- quit: X-Scale` (Ping timeout: 240 seconds) 08:27:06 --- join: X-Scale joined #forth 09:10:14 --- join: proteus-guy joined #forth 09:23:32 proteusguy (or proteus-guy... are you the same person?): not necessarily. I am pessimistic towards language designs that try to combine heavy abstractions with low-level access to the machine, because you usually get all the predictability (and therefore optimizability) of the latter coupled with all the performance of the former 09:26:01 from a cursory reading of the doc pages it doesn't seem that ActorForth strives for the low-level access characteristic of classic Forth, so, well... the actor model is cool, stack-based (concatenative, however you want to call them) languages are cool, so merging them may well get you something useful 09:28:12 though from the same very cursory reading it doesn't appear that the type system is particularly good... swap : Any Any -> Any Any is a rather weak typing (I'd hope for swap : forall a b. a b -> b a or something like that) 09:28:33 alexshpilkin, yeah our target domain is different than what is classically forth - but the architectural drivers are the same - relentlessly eliminate all unnecessary complexity. Our intention is to have a system where a single developer can understand the full tech stack from the top all the way to the gate level. Not possible on "modern" tech stacks. 09:29:32 Ultimately it'll be Any1 Any2 -> Any2 Any1. Just hasn't come up given where we are in the initial implementation. 09:30:02 Actually it'll look more like swap : _1 _2 -> _2 _1 09:31:35 well, parametric polymorphism by any other name ... 09:32:13 but good to know you are planning it 09:32:28 alexshpilkin, part of what we're doing is trying to see how powerful a type system can be implemented in a point-free stack based language. 09:35:10 oh, really? I'll be watching that place then :) 09:36:17 yeah this is more of a "discover based" rather than a planned based system and we expect that it'll take a few implementations before we get the right balance. 09:37:15 have you seen Kleffner's talk about typing stack-based languages (http://prl.ccs.neu.edu/blog/2017/03/10/type-inference-in-stack-based-programming-languages/)? I've linked to it before on ForthHub, but it... well, wasn't met with enthusiasm 09:38:15 yes I have that paper and have read it a few times. 09:43:04 wohoo 10:10:49 --- join: Zarutian_HTC joined #forth 10:25:26 alexshpilkin: you might be interested in my implementation of Algorithm J (of the HM type system) for a concatenative language: https://github.com/ActorForth/ActorForth/blob/haskell/forth.hs 10:25:59 --- quit: proteus-guy (Ping timeout: 260 seconds) 10:26:00 It uses a representation of the stack isomorphic to nested tuples, so barely ant difference from Algorithm J. 10:27:13 It properly deals with polymorphic functions like swap : a:b:s → b:a:s 10:27:22 where a b s are type variables 10:32:18 alexshpilkin: why wasn't it met with enthusiasm from ForthHub? 10:37:23 I should note that there isn't anything particularly hard about type inference in stack-based languages. With a proper AST representation it's no different than writing a typechecker for a functional language. 10:45:21 *shrug* it was mostly met with silence, so no idea. maybe everybody already knows that, maybe nobody is interested, maybe I'm just unpleasant to talk with 10:48:07 Skimming through that conversation, heh that's interesting. Dynamic words like EXECUTE are problematic from a static analysis perspective. This sort of thing is similar to the situation in Lisp. 10:49:19 (I have to admit I've never actually implemented inference, even though I think I kinda understand how it works. No excuse really) 10:50:06 Forth in its current form is no better than assembly, so naturally adding a type system severely restricts the language. 10:50:34 alexshpilkin: I believe using Matrix replies duplicates the content for IRC users, please use mentions instead. 10:50:47 (I'm also on a Matrix bridge) 10:51:40 I'll have to sign off for tonight, will check the messages tomorrow. 10:54:12 alexshpilkin: Do you come from an FP background as well? 10:56:33 siraben : well, my point was there that first-order languages are just easier to type. EXECUTE by itself appears to be just an application operator like Haskell's ($), so not particularly evil, no? though the fact that everything happens on a single stack stack and has variable arity does complicate things 10:58:47 siraben : well to some extent yes. more like I owe my interest in types to FP (Haskell in particular; proof-assistant-y things tend to go over my head, sadly) 11:04:34 --- join: crc_ joined #forth 11:07:33 --- quit: crc (Quit: ZNC 1.7.4 - https://znc.in) 11:07:34 --- nick: crc_ -> crc 11:07:56 --- mode: ChanServ set +v crc 11:41:46 --- quit: jsoft (Ping timeout: 240 seconds) 12:23:12 --- join: xek joined #forth 12:29:19 --- join: WickedShell joined #forth 14:03:18 --- quit: `presiden (Read error: Connection reset by peer) 14:04:22 --- join: `presiden joined #forth 14:17:14 --- quit: Zarutian_HTC (Read error: No route to host) 14:17:31 --- join: Zarutian_HTC joined #forth 14:23:59 --- quit: xek (Ping timeout: 256 seconds) 14:39:27 --- quit: gravicappa (Ping timeout: 260 seconds) 18:04:22 --- join: boru` joined #forth 18:04:24 --- quit: boru (Disconnected by services) 18:04:27 --- nick: boru` -> boru 18:05:06 alexshpilkin: Right, you can consider EXECUTE like that. The type to me would be unclear due to variable arity. 18:05:53 Yes, I'm also a big fan of Haskell. I also like Coq, although it does take some getting used to. 18:18:31 --- join: tabemann joined #forth 18:21:22 --- join: jsoft joined #forth 19:23:58 * tabemann hates how dead this channel's become 20:01:44 --- join: proteus-guy joined #forth 20:06:59 --- quit: proteus-guy (Ping timeout: 260 seconds) 20:19:15 --- join: proteus-guy joined #forth 20:29:09 --- quit: proteus-guy (Ping timeout: 260 seconds) 20:41:21 --- join: proteus-guy joined #forth 20:48:06 --- quit: WickedShell (Remote host closed the connection) 21:30:47 <`presiden> siraben, "I also like Coq" sounds lewd when spoken out loud 21:37:59 --- quit: proteus-guy (Ping timeout: 260 seconds) 21:39:21 `presiden: *sigh*, if I got a dollar every time someone has made a Coq joke 21:39:54 There's actually good reasons for the naming, named after Thierrey Coquand, plus the Calculus of Constructions, and "coq" means rooster in French which is where INRIA is based. 21:40:45 <`presiden> siraben, :P 21:43:29 --- quit: jsoft (Ping timeout: 256 seconds) 21:50:25 --- join: proteus-guy joined #forth 21:55:21 --- quit: proteus-guy (Ping timeout: 244 seconds) 22:36:16 --- join: gravicappa joined #forth 22:44:58 --- join: jsoft joined #forth 23:59:59 --- log: ended forth/20.07.31