< 1601251248 883765 :zzo38!~zzo38@host-24-207-14-22.public.eastlink.ca PRIVMSG #esoteric :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 < 1601251603 994559 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :concatenative languages feel like borderline magic. < 1601252855 127448 :zzo38!~zzo38@host-24-207-14-22.public.eastlink.ca PRIVMSG #esoteric :O, I didn't know that < 1601253398 999476 :arseniiv!~arseniiv@94.41.83.26.dynamic.ufanet.ru QUIT :Ping timeout: 260 seconds < 1601262027 47720 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1601262099 44724 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 256 seconds < 1601262100 650867 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1601265316 312479 :adu!~arobbins@c-76-111-99-194.hsd1.md.comcast.net JOIN :#esoteric < 1601270711 148873 :adu!~arobbins@c-76-111-99-194.hsd1.md.comcast.net QUIT :Quit: adu < 1601273131 870450 :adu!~arobbins@c-76-111-99-194.hsd1.md.comcast.net JOIN :#esoteric < 1601274082 91931 :deltaepsilon23!~deltaepsi@cpe-24-208-148-153.insight.res.rr.com QUIT :Quit: Leaving < 1601275171 582389 :adu!~arobbins@c-76-111-99-194.hsd1.md.comcast.net QUIT :Quit: adu < 1601276892 585199 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net QUIT :Read error: Connection reset by peer < 1601277056 927296 :V!v@anomalous.eu QUIT :Quit: V < 1601277110 158426 :V!v@anomalous.eu JOIN :#esoteric < 1601278537 866882 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 246 seconds < 1601280003 487858 :hendursaga!~weechat@gateway/tor-sasl/hendursaga QUIT :Remote host closed the connection < 1601280066 216534 :hendursaga!~weechat@gateway/tor-sasl/hendursaga JOIN :#esoteric < 1601280527 747521 :hendursa1!~weechat@gateway/tor-sasl/hendursaga JOIN :#esoteric < 1601280643 775636 :hendursaga!~weechat@gateway/tor-sasl/hendursaga QUIT :Ping timeout: 240 seconds < 1601281806 884399 :cpressey!~cpressey@79-72-202-6.dynamic.dsl.as9105.com JOIN :#esoteric < 1601288987 561042 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 240 seconds < 1601291179 867518 :arseniiv!~arseniiv@94.41.83.26.dynamic.ufanet.ru JOIN :#esoteric < 1601292398 984494 :t20kdc!~20kdc@cpc139384-aztw33-2-0-cust220.18-1.cable.virginm.net JOIN :#esoteric < 1601294213 832809 :cpressey!~cpressey@79-72-202-6.dynamic.dsl.as9105.com QUIT :Quit: WeeChat 1.9.1 < 1601296708 45869 :hendursa1!~weechat@gateway/tor-sasl/hendursaga QUIT :Quit: hendursa1 < 1601296725 795910 :hendursaga!~weechat@gateway/tor-sasl/hendursaga JOIN :#esoteric < 1601297939 568905 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Read error: Connection reset by peer < 1601297993 569559 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1601299374 285541 :cpressey!~cpressey@79-72-202-6.dynamic.dsl.as9105.com JOIN :#esoteric < 1601299775 424769 :cpressey1!~cpressey@79-72-202-115.dynamic.dsl.as9105.com JOIN :#esoteric < 1601299925 578542 :cpressey1!~cpressey@79-72-202-115.dynamic.dsl.as9105.com PRIVMSG #esoteric :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 < 1601299940 399702 :cpressey!~cpressey@79-72-202-6.dynamic.dsl.as9105.com QUIT :Ping timeout: 272 seconds < 1601299945 25980 :cpressey1!~cpressey@79-72-202-115.dynamic.dsl.as9105.com NICK :cpressey < 1601300371 491187 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net JOIN :#esoteric < 1601301658 961072 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :HOAS is kinda crazy, im still not sure i get it < 1601301671 782797 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :functions are kind ofthe most opaque data structure possible < 1601301679 664459 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :so the idea of using them for programming is kinda mad < 1601301844 931814 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: Using the host language's model of lambda calculus is the whole point though? < 1601301887 405973 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(AIUI, HOAS is supposed to be convenient.) < 1601301902 298724 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(And also efficient.) < 1601302782 423663 :cpressey!~cpressey@79-72-202-115.dynamic.dsl.as9105.com PRIVMSG #esoteric :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 < 1601302810 204212 :arseniiv!~arseniiv@94.41.83.26.dynamic.ufanet.ru PRIVMSG #esoteric :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 < 1601302830 817328 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: I don't believe theory papers. < 1601302840 251337 :int-e!~noone@int-e.eu PRIVMSG #esoteric ::P < 1601302858 742044 :arseniiv!~arseniiv@94.41.83.26.dynamic.ufanet.ru PRIVMSG #esoteric :maybe I should take this into consideration too… < 1601302859 640359 :int-e!~noone@int-e.eu PRIVMSG #esoteric :they'll stress the part where you don't have to deal with alpha-renaming or index shifting and all that. < 1601302871 119194 :int-e!~noone@int-e.eu PRIVMSG #esoteric :because what else can you write about, really? < 1601302899 757704 :cpressey!~cpressey@79-72-202-115.dynamic.dsl.as9105.com PRIVMSG #esoteric :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 :) < 1601302908 841692 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: disclaimer, I have not really read any HOAS papers (maybe one or two) < 1601303533 340686 :cpressey!~cpressey@79-72-202-115.dynamic.dsl.as9105.com PRIVMSG #esoteric :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". < 1601303554 299024 :cpressey!~cpressey@79-72-202-115.dynamic.dsl.as9105.com PRIVMSG #esoteric :Which seems to be how it's used when I see it used in Haskell. < 1601304052 459684 :cpressey!~cpressey@79-72-202-115.dynamic.dsl.as9105.com PRIVMSG #esoteric :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. < 1601304144 60227 :Remavas!~Remavas@unaffiliated/remavas JOIN :#esoteric < 1601304159 656931 :Remavas!~Remavas@unaffiliated/remavas QUIT :Remote host closed the connection < 1601305328 961984 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1601305396 961822 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 246 seconds < 1601305402 216222 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1601306009 910407 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1601307402 212589 :Arcorann_!~awych@121-200-5-186.79c805.syd.nbn.aussiebb.net QUIT :Read error: Connection reset by peer < 1601308176 27258 :_underscore_!47b863bc@pool-71-184-99-188.bstnma.fios.verizon.net JOIN :#esoteric < 1601308444 801256 :_underscore_!47b863bc@pool-71-184-99-188.bstnma.fios.verizon.net QUIT :Remote host closed the connection < 1601309097 265911 :cpressey!~cpressey@79-72-202-115.dynamic.dsl.as9105.com QUIT :Quit: WeeChat 1.9.1 < 1601310855 799854 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric < 1601312153 805490 :kmc!~beehive@unaffiliated/kmcallister PRIVMSG #esoteric :it avoids needing to reimplement the rigamarole relating to name shadowing / substitution / etc < 1601312165 874468 :kmc!~beehive@unaffiliated/kmcallister PRIVMSG #esoteric :because your host language already implements that < 1601312208 692614 :kmc!~beehive@unaffiliated/kmcallister PRIVMSG #esoteric :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 < 1601312256 173925 :kmc!~beehive@unaffiliated/kmcallister PRIVMSG #esoteric :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 < 1601312284 897149 :kmc!~beehive@unaffiliated/kmcallister PRIVMSG #esoteric :i guess it's kind of a similar principle to church encoding < 1601312337 460375 :kmc!~beehive@unaffiliated/kmcallister PRIVMSG #esoteric :or maybe i'm full of nonsense. that is always a distinct possibility < 1601314449 915758 :kmc!~beehive@unaffiliated/kmcallister PRIVMSG #esoteric :fungot: what do you think < 1601314450 60716 :fungot!~fungot@unaffiliated/fizzie/bot/fungot PRIVMSG #esoteric :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 > 1601314703 362364 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03Bulkasmakom 5* 10New user account > 1601315177 19324 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=77758&oldid=77724 5* 03Bulkasmakom 5* (+1406) 10 > 1601315247 658259 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=77759&oldid=77758 5* 03Bulkasmakom 5* (-108) 10 < 1601315482 576578 :arseniiv!~arseniiv@94.41.83.26.dynamic.ufanet.ru PRIVMSG #esoteric :is there an induction principle for function types? < 1601315560 384054 :arseniiv!~arseniiv@94.41.83.26.dynamic.ufanet.ru PRIVMSG #esoteric :hm it seems exactly it should involve application < 1601315826 334032 :arseniiv!~arseniiv@94.41.83.26.dynamic.ufanet.ru PRIVMSG #esoteric :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 < 1601315897 277739 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :induction for function types is basically forall > 1601316185 694692 PRIVMSG #esoteric :14[[07Welcome14]]4 N10 02https://esolangs.org/w/index.php?oldid=77760 5* 03Bulkasmakom 5* (+1204) 10Created page with "== Description == ScriptJava is like JavaScript, but different. It reverses the behavior when possible. [[ https://github.com/nikita202/scriptjava ]] == Substitutions == gene..." > 1601316249 957781 PRIVMSG #esoteric :14[[07Special:Log/move14]]4 move10 02 5* 03Bulkasmakom 5* 10moved [[02Welcome10]] to [[ScriptJava]]: a mistake > 1601316262 143930 PRIVMSG #esoteric :14[[07Welcome14]]4 10 02https://esolangs.org/w/index.php?diff=77763&oldid=77762 5* 03Bulkasmakom 5* (-24) 10Blanked the page > 1601316426 244908 PRIVMSG #esoteric :14[[07ScriptJava14]]4 10 02https://esolangs.org/w/index.php?diff=77764&oldid=77761 5* 03Bulkasmakom 5* (+0) 10 > 1601316474 949531 PRIVMSG #esoteric :14[[07ScriptJava14]]4 10 02https://esolangs.org/w/index.php?diff=77765&oldid=77764 5* 03Bulkasmakom 5* (+24) 10 > 1601316530 875838 PRIVMSG #esoteric :14[[07List of ideas14]]4 M10 02https://esolangs.org/w/index.php?diff=77766&oldid=77475 5* 03Bulkasmakom 5* (+44) 10 < 1601317361 778923 :zzo38!~zzo38@host-24-207-14-22.public.eastlink.ca PRIVMSG #esoteric :imode: Why do you ask about defining a while loop word in PostScript? < 1601317678 772720 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :zzo38: was working through some rewriting logic for evaluating a concatenative language. < 1601317948 448602 :zzo38!~zzo38@host-24-207-14-22.public.eastlink.ca PRIVMSG #esoteric :imode: O, OK. < 1601318228 926661 :oren!~oren@ec2-34-239-129-109.compute-1.amazonaws.com QUIT :Ping timeout: 256 seconds < 1601318282 630953 :oren!~oren@ec2-34-239-129-109.compute-1.amazonaws.com JOIN :#esoteric < 1601330022 135446 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr 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.” < 1601330339 940536 :adu!~arobbins@c-76-111-99-194.hsd1.md.comcast.net JOIN :#esoteric < 1601331384 883814 :t20kdc!~20kdc@cpc139384-aztw33-2-0-cust220.18-1.cable.virginm.net QUIT :Remote host closed the connection < 1601331410 930711 :t20kdc!~20kdc@cpc139384-aztw33-2-0-cust220.18-1.cable.virginm.net JOIN :#esoteric < 1601334365 975655 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1601335026 395301 :Arcorann_!~awych@121-200-5-186.79c805.syd.nbn.aussiebb.net JOIN :#esoteric < 1601336792 896872 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 256 seconds < 1601336844 621183 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1601336894 859015 :arseniiv!~arseniiv@94.41.83.26.dynamic.ufanet.ru QUIT :Ping timeout: 256 seconds