[00:02:31] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[00:06:18] * jhei [jhei!sid81469@gateway/web/irccloud.com/x-dxhysxuxmltdgjeo] has quit (Ping timeout: 265 seconds).
[00:06:18] * cstrahan [cstrahan!sid36118@gateway/web/irccloud.com/x-wgyjvtldvadsavch] has quit (Ping timeout: 265 seconds).
[00:30:26] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Read error: Connection reset by peer).
[01:07:35] * Sgeo_ [Sgeo_!~Sgeo@ool-18b98dd9.dyn.optonline.net] has joined the channel.
[01:10:21] * Sgeo [Sgeo!~Sgeo@ool-18b98dd9.dyn.optonline.net] has quit (Ping timeout: 240 seconds).
[03:08:23] * pierpa [pierpa!57100917@gateway/web/freenode/ip.87.16.9.23] has quit (Quit: Page closed).
[03:09:28] * jtimon [jtimon!~quassel@226.110.132.37.dynamic.jazztel.es] has quit (Ping timeout: 265 seconds).
[03:53:44] * erkin [erkin!~erkin@unaffiliated/erkin] has joined the channel.
[04:31:06] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[04:54:09] * v0id_NULL [v0id_NULL!~igor_@217.150.79.251] has joined the channel.
[06:22:38] * erkin [erkin!~erkin@unaffiliated/erkin] has quit (Quit: Ouch! Got SIGIRL, dying...).
[06:23:07] * erkin [erkin!~erkin@unaffiliated/erkin] has joined the channel.
[10:33:19] * mtsd [mtsd!~mtsd@77.110.61.100] has joined the channel.
[11:40:35] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Ping timeout: 240 seconds).
[11:48:13] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[11:57:27] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Ping timeout: 256 seconds).
[12:29:40] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[13:07:06] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Quit: Poof).
[13:07:30] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[13:09:33] * mtsd [mtsd!~mtsd@77.110.61.100] has quit (Quit: Leaving).
[13:17:26] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Ping timeout: 276 seconds).
[13:30:04] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[14:43:51] * Sonderblade [Sonderblade!~bjourne@n152-p235.eduroam.kth.se] has joined the channel.
[15:13:14] * Sonderblade [Sonderblade!~bjourne@n152-p235.eduroam.kth.se] has quit (Quit: Konversation terminated!).
[15:13:28] * Sonderblade [Sonderblade!~bjourne@n152-p235.eduroam.kth.se] has joined the channel.
[15:44:12] * jtimon [jtimon!~quassel@226.110.132.37.dynamic.jazztel.es] has joined the channel.
[15:52:47] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Ping timeout: 255 seconds).
[16:26:40] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[16:26:59] * Sonderblade [Sonderblade!~bjourne@n152-p235.eduroam.kth.se] has quit (Quit: Konversation terminated!).
[16:31:45] * Sonderblade [Sonderblade!~bjourne@n152-p235.eduroam.kth.se] has joined the channel.
[17:05:18] * MDude [MDude!~MDude@c-73-187-225-46.hsd1.pa.comcast.net] has quit (Quit: Going offline, see ya! (www.adiirc.com)).
[18:11:33] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Quit: Poof).
[18:11:53] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[18:16:20] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Read error: Connection reset by peer).
[18:21:15] <maaku> v0id_NULL: it's entirely possible to create a statically checked type system for a concatenative language
[18:21:21] <maaku> look more to kitten than factor
[18:21:48] <maaku> but even kitten has some mistakes...
[18:22:09] <maaku> basically there's nothing special about combinators, or deeply polymorphic operations like keep
[18:22:31] <maaku> but some combinators have to have their input types constrained
[18:23:45] <hackerfoo> Popr is statically typed as well, but fully inferred, so there isn't any syntax for annotations.
[18:23:57] <maaku> e.g. IF <cond> THEN <then> ELSE <else> ;; <cond> :: (a -- Bool) ;; <then> :: (b c -- d) ;; <else> :: (b c -- d) 
[18:24:05] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[18:24:20] <hackerfoo> You can still write an annotation as a function that checks a property, and fails otherwise.
[18:24:21] <maaku> it's important that the <then> and <else> have the same type, and ELSE is required if the type isn't ( -- )
[18:25:00] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Read error: Connection reset by peer).
[18:25:10] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[18:25:20] <maaku> there's lots of other gotchas, like pattern matching (a la kitten/haskell) having the same outputs (and inputs beyond the matched pattern, if any)
[18:26:11] <maaku> but if you do that, then the polymorphic type of a program fragment can be inferred, and a full program (including inputs) is monomorphic -- and this is statically checkable.
[18:27:14] <hackerfoo> maaku: The type of a conditional expression can be the union of the type of both branches.
[18:27:20] <maaku> I'm working on an intermediate VM that does this, and could be used as a back end for any strongly typed stack language
[18:28:15] <hackerfoo> maaku: Do you have any source code up?
[18:28:16] <maaku> hackerfoo: while technically true, you get combinatorial explosion of types for a program, which makes the type system pretty much useless
[18:28:34] <hackerfoo> maaku: It's not that bad.
[18:28:51] <maaku> hackerfoo: no but I will soon
[18:29:03] <maaku> this is half of my full-time job, not a hobby thing, so I really will :)
[18:29:14] <hackerfoo> Usually both types will be converted to the same type later.
[18:29:20] <hackerfoo> maaku: Cool
[18:30:06] <hackerfoo> maaku: What is the purpose of the project, if I can ask?
[18:31:08] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Read error: Connection reset by peer).
[18:32:22] <maaku> Something I tried to hire evincarofautumn for three years ago actually, a "programmable signature" language as the base layer for block chain smart contracts, in the same category as. e.g. bitcoin script
[18:32:39] <hackerfoo> maaku: Oh hey, are you in Mountain View?
[18:32:44] <maaku> San Jose
[18:33:24] <hackerfoo> We should have a language designer meetup sometime. There's like 50 of them here at Google.
[18:33:55] <maaku> concatenative people?
[18:34:12] <maaku> yeah a meetup would be great
[18:34:37] <hackerfoo> I suppose, but no reason to restrict it too much. There still aren't a lot of language designers.
[18:35:16] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[18:38:16] <maaku> Ah well I guess I'd be interested in anything having to do with concativenative or strongly typed languages, not more broadly than that. For myself at least
[18:39:09] <hackerfoo> Slava Pestov (Factor) and Jon Purdy (Kitten) are in the area, they went to a presentation of mine a while ago up in SF: https://www.meetup.com/SF-Types-Theorems-and-Programming-Languages/events/232732627/
[18:40:43] <maaku> regarding your earlier comment "usually both types will be converted to the same type later", do you have any examples of when that can't be done within the clause itself?
[18:41:40] <maaku> otherwise you could use sum-types (variants) to carry forward the state (e.g. Bool | Int), but I recognize that is a cumbersome work-around
[18:42:21] <maaku> Yeah Jon Purdy inspired the work I'm currently doing. I had the good fortune of meeting him a few years back. Smart guy.
[18:43:07] <hackerfoo> Sure. I'm not sure how useful it is, because I don't tend to use it much yet, but you could do something conditional on the type, apply some polymorphic functions, and then convert the result to a specific type.
[18:44:09] <hackerfoo> It's a consequence of how Popr is designed. I decided direct branching support was a hack, so I designed something inspired by GPU masking and logic programming.
[18:45:06] <hackerfoo> Furthermore, if/then/else makes a mess of code pretty quickly, if you have branching interleaved with computation.
[18:46:25] <hackerfoo> So, essentially, the creation and pruning of branches are separate primitives, inspired by linear logic.
[18:46:45] <maaku> hackerfoo: do you have something written up on that?
[18:46:53] <maaku> sorry for the assymetric request ;)
[18:47:45] <hackerfoo> maaku: Here's the presentation I gave a while ago: http://hackerfoo.com/presentations/ttpl_slides.html
[18:47:53] <maaku> thanks
[18:48:17] <hackerfoo> maaku: Here's a more recent tutorial, sort of: http://hackerfoo.com/posts/popr-tutorial-0-dot-machines.html
[18:48:24] * jhei [jhei!sid81469@gateway/web/irccloud.com/x-kllpmbmvpizwthol] has joined the channel.
[18:48:55] <hackerfoo> maaku: And then there's a quick language overview on the project page: https://github.com/hackerfoo/poprc
[18:49:19] <maaku> hackerfoo: looks like we're working on very similar things
[18:50:26] <hackerfoo> maaku: And here's my incomplete attempt at formal typing rules for the language: https://drive.google.com/file/d/0B6W_9Wbvba0oSlpTM2R6R0o3Qlk/view?usp=sharing
[18:51:35] <hackerfoo> You can play with the compiler here: http://hackerfoo.com/eval.html
[18:54:34] <maaku> your "why no popl?" isn't very convincing
[18:56:02] <hackerfoo> Yeah, I suppose. Maybe the tutorial explains it better.
[18:57:21] <maaku> I mean is there a non-implementation-specific technical reason?
[18:57:22] <hackerfoo> If you're familiar with Haskell, it would be like extracting an argument after partial application: f (+ x) = x
[18:57:50] <maaku> It's weird to do that in haskell. It's not so weird in a concatenative language, where the transformation is straightforward.
[18:58:44] <maaku> but i'll read the tutorial and other stuff before commenting further
[18:59:32] <hackerfoo> Quotes in Popr are somewhat like currying in Haskell, except applying arguments and evaluation are separate operations.
[19:01:01] <hackerfoo> Anyway, yeah, there are a lot of things that are surprising until you get an intuition for the language. It's very different; I've mostly given up explaining it in relation to other languages, as you can see from the tutorial introduction.
[19:03:57] <hackerfoo> It's designed to compile to fairly straightforward SSA, so you can't tear apart quotes and play with them; it generates native code (through C currently.)
[19:04:52] <hackerfoo> Furthermore, static typing would be difficult to impossible.
[19:09:01] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Read error: Connection reset by peer).
[19:14:20] * v0id_NULL [v0id_NULL!~igor_@217.150.79.251] has quit (Ping timeout: 260 seconds).
[19:14:54] <maaku> hackerfoo: if words can't exist outside of a quotation, what is the result of [1 +] popr?
[19:15:57] <hackerfoo> maaku: It fails.
[19:16:45] <maaku> you can't tell that it would fail at compile time though right?
[19:17:06] <maaku> i mean you can here, but potentially the quottion [1 +] was constructed, or passed in from somewhere else
[19:17:27] <maaku> seems like an arbitrary restriction
[19:18:04] <hackerfoo> It's no different than  `[] popr`
[19:19:16] <hackerfoo> I can calculate the arity of any quote parameter at compile time, so `popr` requires a quote that takes no arguments, and produces at least one result.
[19:20:58] <hackerfoo> There's a similar discussion on LtU: http://lambda-the-ultimate.org/node/5520
[19:21:31] <maaku> ok a more convincing argument (for me at least) about popl is that you can't know whether to do rho reduction on the type
[19:21:33] <maaku> [2 3 + 5 *] :: ( -- Int ) popl :: ( Int -- Int ) ... but [25] popl :: ( -- )
[19:22:02] <maaku> whereas popr is always well defined (even for words like (*), if you dropped your restriction)
[19:23:15] <maaku> the comparison to Haskell just doesn't hold because one of the reasons you can't "undo" partial application is because it's non-trivial to specify which is being removed 
[19:23:27] <hackerfoo> Right. And whether an expression has been reduced or not should not be observable in any way.
[19:24:02] <maaku> but with stack languages we go from lexical scoping of variables to stack ordering, so it *is* well defined what a popl would be in terms of which "variable" is being extracted
[19:24:09] <hackerfoo> maaku: What about [swap] ?
[19:24:38] <hackerfoo> [1 2 swap] = [2 1], so what is [1 2 swap] popl?
[19:26:45] <maaku> hackerfoo: you add typeof(1) to the input side of the rho type
[19:26:55] <maaku> ( -- ) -> ( Int -- )
[19:26:57] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel.
[19:27:59] <maaku> your "type stack" goes from [ ( -- Int Int) ] to [ ( -- Int ) ( Int -- Int Int ) ]
[19:28:50] <hackerfoo> Sure, that works here, but what about [1 A swap]? (A is a symbol, which is singleton type)
[19:29:52] <maaku> [ ( -- Atom Int ) ] to [ ( -- Int ) ( Int -- Atom Int ) ]
[19:30:03] <maaku> not sure what the issue is?
[19:30:15] <maaku> (or whatever your type of symbols is)
[19:33:02] <maaku> popr of words is well defined here too. [1 2 swap] -> [1 2] 'swap :: ( -- Int Int ) -> ( -- Int Int ) ( Int Int -- Int Int )
[19:34:31] <maaku> hrm. actually you run into the same issue with rho reduction on both popl and popr
[19:36:46] <maaku> [1 swap] :: ( Int -- Int Int)... but [1] 'swap , should the [1] be ( -- Int ) or ( Int -- Int Int ) ?
[19:37:13] <maaku> the first is correct, but the 2nd might just as well be valid if you didn't introspect the contents
[20:09:46] <hackerfoo> maaku: Sorry, meetings. I'll reply later.
[20:44:52] * Sonderblade [Sonderblade!~bjourne@n152-p235.eduroam.kth.se] has quit (Quit: Konversation terminated!).
[22:25:37] <hackerfoo> maaku: I don't understand why there should be a separate kind of quote.
[22:27:06] <hackerfoo> A quote is a (possibly incomplete) computation reified as a value.
[22:27:33] <hackerfoo> It's not an AST, or source code.
[22:32:02] <maaku> hackerfoo: I see that your quotations are hunks in the Haskell/ML lazy evaluation sense, not quoted source code in the Lisp sense
[22:37:25] <hackerfoo> Evaluation at runtime is slow and difficult to type. I don't consider it acceptable for the applications I'm interested in.
[22:38:31] <hackerfoo> PoprC is fully ahead-of-time compiled with a minimal runtime (like C.)
[23:15:52] <maaku> I don't see any additional challenge to typing. The compiler knows and can enforce the types of the fragments you are composing together.
[23:17:04] <maaku> It's some work for implementation, but not to the level of embedding a whole compiler. Fragments would be compiled and you send function pointers around
[23:17:33] <maaku> Think more STL's <functional> than an embedded compiler with string or AST inputs.
[23:18:12] <maaku> As a concrete motivation for why, SQL or SQL-like query compilers come to mind.
[23:18:17] <maaku> *query optimizers
[23:19:05] <maaku> Which incidentally are a very big use case for your "alternatives" computation model
[23:19:49] <maaku> "SELECT * FROM table WHERE ..." the select returns the entire table as alternates, then the where clauses prune.
[23:20:46] <maaku> being able to dynamically build WHERE clauses in a type-safe way would have many uses