00:00:48 <zzo38> Perhaps like this: /while {{exec} 0 get exch {{exit} ifelse} aload pop 5 array astore cvx loop} bind def Now you can write: 9 {dup 0 ne} {dup = 1 sub} while
00:06:43 <imode> concatenative languages feel like borderline magic.
00:27:35 <zzo38> O, I didn't know that
00:36:38 -!- arseniiv has quit (Ping timeout: 260 seconds).
03:00:27 -!- Lord_of_Life_ has joined.
03:01:39 -!- Lord_of_Life has quit (Ping timeout: 256 seconds).
03:01:40 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
03:55:16 -!- adu has joined.
05:25:11 -!- adu has quit (Quit: adu).
06:05:31 -!- adu has joined.
06:21:22 -!- deltaepsilon23 has quit (Quit: Leaving).
06:39:31 -!- adu has quit (Quit: adu).
07:08:12 -!- Sgeo has quit (Read error: Connection reset by peer).
07:10:56 -!- V has quit (Quit: V).
07:11:50 -!- V has joined.
07:35:37 -!- imode has quit (Ping timeout: 246 seconds).
08:00:03 -!- hendursaga has quit (Remote host closed the connection).
08:01:06 -!- hendursaga has joined.
08:08:47 -!- hendursa1 has joined.
08:10:43 -!- hendursaga has quit (Ping timeout: 240 seconds).
08:30:06 -!- cpressey has joined.
10:29:47 -!- sprocklem has quit (Ping timeout: 240 seconds).
11:06:19 -!- arseniiv has joined.
11:26:38 -!- t20kdc has joined.
11:56:53 -!- cpressey has quit (Quit: WeeChat 1.9.1).
12:38:28 -!- hendursa1 has quit (Quit: hendursa1).
12:38:45 -!- hendursaga has joined.
12:58:59 -!- Lord_of_Life has quit (Read error: Connection reset by peer).
12:59:53 -!- Lord_of_Life has joined.
13:22:54 -!- cpressey has joined.
13:29:35 -!- cpressey1 has joined.
13:32:05 <cpressey1> So HOAS, at least as Haskellers use it, turns out to be exactly *not* what I thought it was. Representing your programs as lambda terms -- yes, OK, fine; implementing those lambda terms with functions in the host language -- ack what whyyyy
13:32:20 -!- cpressey has quit (Ping timeout: 272 seconds).
13:32:25 -!- cpressey1 has changed nick to cpressey.
13:39:31 -!- Sgeo has joined.
14:00:58 <rain1> HOAS is kinda crazy, im still not sure i get it
14:01:11 <rain1> functions are kind ofthe most opaque data structure possible
14:01:19 <rain1> so the idea of using them for programming is kinda mad
14:04:04 <int-e> cpressey: Using the host language's model of lambda calculus is the whole point though?
14:04:47 <int-e> (AIUI, HOAS is supposed to be convenient.)
14:05:02 <int-e> (And also efficient.)
14:19:42 <cpressey> int-e: the papers and articles that I read up to this point definitely definitely did not lead me to believe that it was the whole point, that's all I can say
14:20:10 <arseniiv> I thought there’s usually a way to make functions not as opaque, something like they all get arguments of such a “type of variables” which allows to get a substituted body and not evaluate it too much? I forgot what I read
14:20:30 <int-e> cpressey: I don't believe theory papers.
14:20:58 <arseniiv> maybe I should take this into consideration too…
14:20:59 <int-e> they'll stress the part where you don't have to deal with alpha-renaming or index shifting and all that.
14:21:11 <int-e> because what else can you write about, really?
14:21:39 <cpressey> int-e: https://en.wikipedia.org/wiki/Higher-order_abstract_syntax#Implementation -- maybe you'd like to add "Also the function values of the host language can be used, in fact it's the whole point" to that :)
14:21:48 <int-e> cpressey: disclaimer, I have not really read any HOAS papers (maybe one or two)
14:32:13 <cpressey> The section below that, on their use in logical frameworks, does say that it "usually refers to a specific representation that uses the binders of the meta-language".
14:32:34 <cpressey> Which seems to be how it's used when I see it used in Haskell.
14:40:52 <cpressey> So the underlying thing seems to be that I'm expecting to see the term used in a general sense, but I'm seeing it used in a more specific sense that a particular subculture uses. OK then.
14:42:24 -!- Remavas has joined.
14:42:39 -!- Remavas has quit (Remote host closed the connection).
15:02:08 -!- Lord_of_Life_ has joined.
15:03:16 -!- Lord_of_Life has quit (Ping timeout: 246 seconds).
15:03:22 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
15:13:29 -!- imode has joined.
15:36:42 -!- Arcorann_ has quit (Read error: Connection reset by peer).
15:49:36 -!- _underscore_ has joined.
15:54:04 -!- _underscore_ has quit (Remote host closed the connection).
16:04:57 -!- cpressey has quit (Quit: WeeChat 1.9.1).
16:34:15 -!- LKoen has joined.
16:55:53 <kmc> it avoids needing to reimplement the rigamarole relating to name shadowing / substitution / etc
16:56:05 <kmc> because your host language already implements that
16:56:48 <kmc> it's been a while, but I think you can easily convert a HOAS term into a first order traditional AST by feeding in a supply of fresh names
16:57:36 <kmc> so yes, in one sense host language functions are the most opaque data structure there is; in another sense they are the most versatile because you can ask them anything you want just by applying them
16:58:04 <kmc> i guess it's kind of a similar principle to church encoding
16:58:57 <kmc> or maybe i'm full of nonsense. that is always a distinct possibility
17:34:09 <kmc> fungot: what do you think
17:34:10 <fungot> kmc: and it just might be all three possible codes, yielding a radically exactly the same as the word " crazy" t)(at is so ridiculous shit so youll probably sleep with the damn point
17:38:23 <esowiki> [[Special:Log/newusers]] create * Bulkasmakom * New user account
17:46:17 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=77758&oldid=77724 * Bulkasmakom * (+1406)
17:47:27 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=77759&oldid=77758 * Bulkasmakom * (-108)
17:51:22 <arseniiv> is there an induction principle for function types?
17:52:40 <arseniiv> hm it seems exactly it should involve application
17:57:06 <arseniiv> yeah, if one’s to show something like “foldNat Z z s = z, foldNat (S x) z s = s (foldNat x z s)”, then we have foldFun (λa. x) a = x
17:58:17 <rain1> induction for function types is basically forall
18:03:05 <esowiki> [[Welcome]] N https://esolangs.org/w/index.php?oldid=77760 * Bulkasmakom * (+1204) Created page with "== Description == ScriptJava is like JavaScript, but different. It reverses the behavior when possible. [[ https://github.com/nikita202/scriptjava ]] == Substitutions == gene..."
18:04:09 <esowiki> [[Special:Log/move]] move * Bulkasmakom * moved [[Welcome]] to [[ScriptJava]]: a mistake
18:04:22 <esowiki> [[Welcome]] https://esolangs.org/w/index.php?diff=77763&oldid=77762 * Bulkasmakom * (-24) Blanked the page
18:07:06 <esowiki> [[ScriptJava]] https://esolangs.org/w/index.php?diff=77764&oldid=77761 * Bulkasmakom * (+0)
18:07:54 <esowiki> [[ScriptJava]] https://esolangs.org/w/index.php?diff=77765&oldid=77764 * Bulkasmakom * (+24)
18:08:50 <esowiki> [[List of ideas]] M https://esolangs.org/w/index.php?diff=77766&oldid=77475 * Bulkasmakom * (+44)
18:22:41 <zzo38> imode: Why do you ask about defining a while loop word in PostScript?
18:27:58 <imode> zzo38: was working through some rewriting logic for evaluating a concatenative language.
18:37:08 -!- oren has quit (Ping timeout: 256 seconds).
18:38:02 -!- oren has joined.
21:53:42 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”).
21:58:59 -!- adu has joined.
22:16:24 -!- t20kdc has quit (Remote host closed the connection).
22:16:50 -!- t20kdc has joined.
23:06:05 -!- sprocklem has joined.
23:17:06 -!- Arcorann_ has joined.
23:46:32 -!- sprocklem has quit (Ping timeout: 256 seconds).
23:47:24 -!- sprocklem has joined.
23:48:14 -!- arseniiv has quit (Ping timeout: 256 seconds).