2021-05-21 05:30:42 +0200 | <edwardk> | Examples for me are things like https://arxiv.org/abs/1609.03543 and https://intelligence.org/files/ParametricBoundedLobsTheorem.pdf The former covers 'how do you get an agent to gain consistency in its belief structure over time so you can't hold inconsistent beliefs against it forever?' and 'how do you even allow intelligences to cooperate and beat the nash equilibria, because nash equilibria where agents are getting smarter at |

2021-05-16 19:08:23 +0200 | <mysterybear> | https://web.cecs.pdx.edu/~mpj/pubs/springschool95.pdf mark p. jones |

2021-05-13 15:06:36 +0200 | <romesrf> | i got it from http://okmij.org/ftp/papers/LogicT.pdf |

2021-05-12 16:54:08 +0200 | <dminuoso> | https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/embedding-short.pdf |

2021-05-12 00:49:26 +0200 | <shanemikel> | In particular this paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/typefun.pdf |

2021-05-11 22:25:13 +0200 | <shapr> | m_shiraeeshi: at the momemt, yes... the FPGA designs has on-die RAM that's much faster https://www-users.york.ac.uk/~mt540/graceful-ws/slides/Stewart.pdf |

2021-05-09 01:17:48 +0200 | <olle> | https://userpages.uni-koblenz.de/~laemmel/TheEagle/resources/pdf/xproblem1.pdf |

2021-05-06 10:51:22 +0200 | <jacks2> | olle, see this: http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf |

2021-05-06 06:53:35 +0200 | <dmj`> | gnumonic: I have the PFDS books, there are Haskell versions in the appendices. Check page 185 https://doc.lagout.org/programmation/Functional%20Programming/Chris_Okasaki-Purely_Functional_Data… |

2021-05-03 23:23:34 +0200 | <safinaskar> | i wonder whether this method will work for really complex logics such as logic of ghc itself: https://github.com/ghc/ghc/blob/master/docs/core-spec/core-spec.pdf |

2021-04-28 19:02:44 +0200 | <tomsmeding> | shapr: this one https://www.microsoft.com/en-us/research/uploads/prod/1987/01/slpj-book-1987.pdf |

2021-04-28 19:01:22 +0200 | <tomsmeding> | shapr: this one? https://www.microsoft.com/en-us/research/wp-content/uploads/1992/01/student.pdf |

2021-04-28 17:30:59 +0200 | <shapr> | the big ideas are really neat though, https://www-users.york.ac.uk/~mt540/graceful-ws/slides/Stewart.pdf |

2021-04-25 19:57:04 +0200 | <hpc> | maybe it's if and only if, like https://arxiv.org/pdf/1002.2284.pdf |

2021-04-23 15:22:36 +0200 | <merijn> | carbolymer: http://ezyang.com/jfp-ghc-rts-draft.pdf |

2021-04-14 23:24:08 +0200 | <ski> | * ski had some vague ideas how that could possibly be related to derivatives of data structures <http://strictlypositive.org/diff.pdf>, combinatorial species <https://byorgey.wordpress.com/category/species/>, naperian containers <https://web.archive.org/web/20161104231529/http://sneezy.cs.nott.ac.uk/containers/blog/> |

2021-04-14 23:22:31 +0200 | <ski> | * ski . o O ( "Toposes, Triples and Theories" by Michael Barr,Charles Wells in 2000 at <https://www.math.mcgill.ca/barr/papers/ttt.pdf> ; "Elementary Categories, Elementary Toposes" by Colin McLart in 1992 ) <yetanother> Hardly an intro <yetanother> (Bar) <OP> yetanother: yes I have watched these but he is a bit slow and the recording is bad (I am a bit of a princess at times) |

2021-04-14 23:22:21 +0200 | <ski> | * ski . o O ( "Seven Sketches in Compositionality - An Invitation to Applied Category Theory" by Brendan Fong,David I. Spivak in - 2018-10-12 at <https://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf>,<https://math.mit.edu/~dspivak/teaching/sp18/> ) <yetanother> OP: some haskell folks like Bartosz Milewski |

2021-04-14 23:21:24 +0200 | <ski> | <ski> 1992,"Computational Category Theory" by D. E. Rydeheard,R. M. Burstall in 2001 at <http://www.cs.man.ac.uk/~david/categories/book/book.pdf>,<http://www.cs.man.ac.uk/~david/categories/> |

2021-04-14 23:21:10 +0200 | <ski> | <ski> there's also a few books that relate a bit more to CS. like "Basic Category Theory for Computer Scientists" by Benjamin Pierce,"Categories, types, structures - An introduction to category theory for the working computer scientist" by Andrea Asperti,Guiseppe Longo in 1991 at <https://www.di.ens.fr/users/longo/files/CategTypesStructures/book.pdf>,"Categories and Computer Science" by R. F. Walters in |

2021-04-13 20:31:39 +0200 | ski | . o O ( <https://en.wikipedia.org/wiki/Drinker_paradox> ; "Searchable Sets, Dubuc-Penon Compactness, Omniscience Principles, and the Drinker Paradox" by Martín Hötzel Escardó,Paulo Oliva in 2010 at <http://www.cs.bham.ac.uk/~mhe/papers/dp.pdf>,<http://www.cs.bham.ac.uk/~mhe/papers/DP/> ) |

2021-04-13 20:12:59 +0200 | <lambdabot> | "On Understanding Data Abstraction, Revisited" by William R. Cook in 2009-10 at <http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf> |

2021-04-13 20:12:56 +0200 | <lambdabot> | "On Understanding Types, Data Abstraction, and Polymorphism" by Luca Cardelli,Peter Wegner in 1985-12 at <http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf> |

2021-04-12 06:12:06 +0200 | <lambdabot> | "On Understanding Data Abstraction, Revisited" by William R. Cook in 2009-10 at <http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf> |

2021-04-12 06:10:14 +0200 | <lambdabot> | "On Understanding Types, Data Abstraction, and Polymorphism" by Luca Cardelli,Peter Wegner in 1985-12 at <http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf> |

2021-04-09 17:13:39 +0200 | <lambdabot> | "On Understanding Types, Data Abstraction, and Polymorphism" by Luca Cardelli,Peter Wegner in 1985-12 at <http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf> |

2021-04-09 06:24:09 +0200 | <wroathe> | And this is the paper: https://web.cecs.pdx.edu/~mpj/thih/thih.pdf (Sorry for the spam) |

2021-04-07 03:27:12 +0200 | <Axman6> | I think it was https://simonmar.github.io/bib/papers/concurrent-data.pdf |

2021-04-06 00:15:44 +0200 | <superstar64> | i just implemented this paper https://www.mathematik.uni-marburg.de/~rendel/rendel10invertible.pdf similar pattern for partial isomorphisms, but i found out you only really need prisms |

2021-03-31 21:55:33 +0200 | <tomsmeding> | searching "strachey 1967" turns up https://www.cs.cmu.edu/~crary/819-f09/Strachey67.pdf which doesn't contain the word 'currying' |

2021-03-30 20:53:59 +0200 | <shapr> | Lycurgus: also http://dimacs.rutgers.edu/~graham/pubs/papers/cmencyc.pdf |

2021-03-30 20:51:16 +0200 | <shapr> | Lycurgus: that and more in the readme for this lib "Finding Frequent Items in Data Streams", http://www.ece.uc.edu/~mazlack/dbm.w2010/Charikar.02.pdf https://sites.google.com/site/countminsketch/cm-eclectics https://tech.shareaholic.com/2012/12/03/the-count-min-sketch-how-to-count-over-large-keyspaces-whe… |

2021-03-30 20:50:11 +0200 | <Lycurgus> | http://dimacs.rutgers.edu/~graham/pubs/papers/encalgs-ams.pdf noteworthy for some of the applications, has c code links. At first I thought AMS was the math soc |

2021-03-30 13:38:40 +0200 | <edwardk> | http://www.riec.tohoku.ac.jp/~asada/papers/arrStrMnd.pdf goes into the topic of strength here, but it might be a slow slog on first reading |

2021-03-30 00:41:14 +0200 | <sclv> | i should mention regarding the above discussion btw the "a la carte" approach https://www.microsoft.com/en-us/research/uploads/prod/2018/03/build-systems.pdf |

2021-03-24 17:39:43 +0100 | <siraben> | sclv: something like "Fast and Loose Reasoning is Morally Correct" https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf ? |

2021-03-24 17:38:20 +0100 | ski | . o O ( "A Tutorial on (Co)Algebras and (Co)Induction" by Bart Jacobs,Jan Rutten in 1997 at <https://www.cs.ru.nl/B.Jacobs/PAPERS/JR.pdf> ) |

2021-03-21 23:29:45 +0100 | <ski> | -- "Locus Solum : From the rules of logic to the logic of rules" (Appendix A, "A pure waste of paper") by Jean-Yves Girard in 2001 at <https://girard.perso.math.cnrs.fr/0.pdf> |

2021-03-19 13:21:02 +0100 | <jackdk> | Is anyone here familiar with the STG paper at https://www.microsoft.com/en-us/research/wp-content/uploads/1992/04/spineless-tagless-gmachine.pdf ? Section 4.2 says that it's safe to mark every lambda as non-updateable, but then when they specify the abstract machine, Rule 15 seems to be the only one for updateable closures, and it requires an empty arglist. I am confused. |

2021-03-16 16:53:05 +0100 | <dminuoso> | In the sense of https://simonmar.github.io/bib/papers/ext-exceptions.pdf |

2021-03-16 14:17:52 +0100 | <merijn> | http://dev.stephendiehl.com/hask/tutorial.pdf |

2021-03-15 08:24:49 +0100 | <dmj`> | koz_: http://web.cecs.pdx.edu/~mpj/thih/thih.pdf |

2021-03-11 22:32:12 +0100 | <sclv> | re wholemeal programming: https://www.cs.ox.ac.uk/people/ralf.hinze/publications/ICFP09.pdf |

2021-03-09 18:02:39 +0100 | <Gurkenglas> | ( https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf ) |

2021-03-08 16:43:57 +0100 | <Gurkenglas> | Shouldn't https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf -> (69) use Nu rather than Mu? |

2021-03-04 17:08:52 +0100 | <lambdabot> | http://www.cs.cmu.edu/~rwh/theses/okasaki.pdf |

2021-03-04 17:07:46 +0100 | <dolio> | jhaxim: https://www.cs.cmu.edu/~rwh/theses/okasaki.pdf |

2021-03-03 17:31:42 +0100 | <merijn> | robwebbjr: If you wanna get sidetracked pondering folds for some time, here's a good link: https://tsouanas.org/teaching/fun/2019.2/doc/hutton-fold.pdf :) |

2021-03-03 08:20:57 +0100 | <edwardk> | http://web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf is a nice paper (from 1993!) where Mark P Jones of hugs fame and Luc Duponcheel go through a few ways to compose pointed functors with monads to get a monad. |

2021-02-26 19:54:36 +0100 | <tomsmeding> | koz_: I assume you've already looked at https://simonmar.github.io/bib/papers/applicativedo.pdf ? |

2021-02-26 09:07:10 +0100 | <koz_> | https://transfer.sh/urUNU/enjoy-reading.pdf |

2021-02-25 21:55:49 +0100 | <dminuoso> | 21:48:33 ski | dminuoso : "On the Meanings of the Logical Constants and the Justifications of the Logical Laws" by Per Martin-Löf in 1996 at <https://www.ae-info.org/attach/User/Martin-L%C3%B6f_Per/OtherInformation/article.pdf>,<https://intuitionistic.wordpress.com/works-on-martin-lofs-type-theory/> |

2021-02-25 21:48:33 +0100 | <ski> | dminuoso : "On the Meanings of the Logical Constants and the Justifications of the Logical Laws" by Per Martin-Löf in 1996 at <https://www.ae-info.org/attach/User/Martin-L%C3%B6f_Per/OtherInformation/article.pdf>,<https://intuitionistic.wordpress.com/works-on-martin-lofs-type-theory/> |

2021-02-25 10:06:29 +0100 | <ski> | "A Theory of Changes for Higher-Order Languages: Incrementalizing λ-Calculi by Static Differentiation" by Yufei Cai,Paulo G. Giarrusso (pgiarrusso),Tillmann Rendel,Klaus Ostermann in 2014-06-(09-11) at <https://www.informatik.uni-marburg.de/~pgiarrusso/papers/pldi14-ilc-author-final.pdf>,"Incremental λ-Calculus" <https://www.informatik.uni-marburg.de/~pgiarrusso/ILC/> was the paper i was thinking about |

2021-02-25 09:59:30 +0100 | <edwardk> | https://danel.ahman.ee/papers/types13postproc.pdf |

2021-02-25 09:29:55 +0100 | <edwardk> | https://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf goes into the naturality vs. parametricity issue more deeply but it does get mathy fast |

2021-02-22 00:50:05 +0100 | <MarcelineVQ> | jackdk: I just see it called "zero-one-many semiring" https://bentnib.org/quantitative-type-theory.pdf |

2021-02-21 04:09:56 +0100 | <MarcelineVQ> | https://www.cs.dartmouth.edu/~doug/nfa.pdf makes me even more suspicious about it |

2021-02-21 02:19:35 +0100 | <monochrom> | https://www.cs.dartmouth.edu/~doug/nfa.pdf |

2021-02-21 01:47:41 +0100 | <monochrom> | The most competitive solution may be https://themonadreader.files.wordpress.com/2014/04/fizzbuzz.pdf |

2021-02-19 04:37:37 +0100 | <inkbottle> | This might be related to my Epsilon/Counit question: "How many adjunction give rise to the same monad?" That could explain why I've failed to pinpoint one counit. https://cpb-us-e1.wpmucdn.com/s.wayne.edu/dist/d/10/files/2018/02/kleisli6c-10zk5wx.pdf |

2021-02-16 17:20:49 +0100 | <fresheyeball> | https://ifl2014.github.io/submissions/ifl2014_submission_13.pdf |

2021-02-16 09:18:58 +0100 | <siraben> | more introductory paper on expressing physics concepts in Haskell: https://arxiv.org/pdf/1412.4880.pdf |

2021-02-15 17:08:17 +0100 | <merijn> | maerwald: The original is here: https://www.haskell.org/cabal/proposal/pkg-spec.pdf |

2021-02-12 21:13:19 +0100 | <merijn> | __minoru__shirae: http://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf |

2021-02-12 20:00:22 +0100 | <boxscape> | (https://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf) |

2021-02-12 17:33:22 +0100 | <pja> | Even older: this paper from FLOPS95 :) https://www.cs.york.ac.uk/plasma/publications/pdf/MatsushitaRuncimanFLOPS95.pdf |

2021-02-09 00:27:31 +0100 | <mjacob> | i'm working through the paper "Functional Programming with Structured Graphs" (https://www.cs.utexas.edu/~wcook/Drafts/2012/graphs.pdf) |

2021-02-07 14:35:00 +0100 | <zebrag> | There are very interesting quotes there, by the way: "Free Applicative Functors" https://arxiv.org/pdf/1403.0749.pdf, like this one "an applicative functor is just a functor that knows how to lift functions of arbitrary arities." |

2021-02-07 14:31:34 +0100 | <merijn> | zebrag: The Selective Functors paper from 2019 discusses the "static analysis" power of Applicative and Monad (and how this leads to the idea of Selective functors), it's an interesting read: https://eprints.ncl.ac.uk/file_store/production/258640/4FF2555F-0AEC-4876-9701-C83A3E5FFF52.pdf |

2021-02-04 01:37:05 +0100 | <monochrom> | Axman6: As it happens, I'm reading https://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf out of a different conversation, but it brings up "monoid semiautomaton" as an automaton without a designated start state. Perhaps you could use that name. |

2021-02-03 21:48:17 +0100 | <dolio> | The congruence stuff is discussed in this paper: https://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf |

2021-02-03 17:22:15 +0100 | <merijn> | ski: https://personal.cis.strath.ac.uk/conor.mcbride/so-pigworker.pdf |

2021-02-03 05:38:27 +0100 | <dolio> | https://u.math.biu.ac.il/~katzmik/bishop18bb.pdf |

2021-02-03 05:23:35 +0100 | <ski> | another influential thing was ISWIM, introduced by Peter Landin in 1966 in his paper "The Next 700 Programming Languages" at <https://www.cs.cmu.edu/~crary/819-f09/Landin66.pdf> |

2021-02-03 05:19:50 +0100 | <lambdabot> | award_winners/backus_0703524.cfm>,<http://www.thocp.net/biographies/papers/backus_turingaward_lecture.pdf> |

2021-02-02 18:43:51 +0100 | <geekosaur> | https://www.cs.cmu.edu/~rwh/theses/okasaki.pdf |

2021-01-29 17:26:59 +0100 | <edrx> | hi ski! I've put a "Thx to ski @ #haskell" here: http://angg.twu.net/LATEX/2021excuse.pdf#page=9 =) |

2021-01-28 02:06:40 +0100 | <edrx> | I have some proofs on Heyting Algebras with a modal operator - the ones in page 9 here: http://angg.twu.net/LATEX/2020J-ops-new.pdf - that I want to formalize in Idris at some point. But I am trying to learn Idris and I was progressing very slowly - and I realized that it would be better to learn Haskell first... |

2021-01-27 23:01:13 +0100 | <ski> | hpc : Epigram ASCII-arts inference rule lines, and sub-boxes. e.g. see groups and sheds in <http://www.strictlypositive.org/epigram-notes.pdf> |

2021-01-27 21:20:43 +0100 | <ski> | the paper "Exceptional Syntax" by Nick Benton,Andrew Kennedy in 2001 at <https://www.cs.tufts.edu/~nr/cs257/archive/nick-benton/exceptional-syntax.pdf> talks about this |

2021-01-26 17:15:05 +0100 | <zebrag> | Really nice. I'm spending a heck lot of time reading something likely far less difficult than Amr Sabry ;) (https://legacy.cs.indiana.edu/~sabry/papers/rational.pdf) |

2021-01-24 05:38:50 +0100 | <zebrag> | ski: if we can deduce `exists x.P` from `Gamma`, and we can deduce `Q` from `P[t/x], then we can deduce `Q` from `Gamma`. I agree with that NatDed formulation, which seems also similar to what we see page 13 of https://www.cs.cmu.edu/~fp/courses/atp/handouts/ch2-natded.pdf |

2021-01-24 04:05:32 +0100 | <zebrag> | monochrom: :set -XGADTs -XRankNTypes; data X a = forall b . X a b; xs = [X 1 'a', X 2 2]; { f :: forall b . b -> Int; f b = 3}; { fs [] = 2; fs (X a b : _) = f b }; fs xs -- returns 3. It suits well with the existential elimination p. 5 of https://courses.cs.washington.edu/courses/cse321/10wi/natural-deduction.pdf |

2021-01-24 03:29:04 +0100 | <zebrag> | Really I'm reading p. 9 of https://arxiv.org/pdf/1403.0749.pdf "free applicative functors", and I already have enough on my plate, but I think, a must understand what the `forall` is for in that circumstance |

2021-01-23 05:09:38 +0100 | <zebrag> | _deepfire: https://arxiv.org/pdf/1403.0749.pdf |

2021-01-21 04:54:32 +0100 | <ski> | see e.g. "On the meaning of the logical constants and the justifications of the logical laws" by Per Martin-Löf in 1996 at <https://intuitionistic.files.wordpress.com/2010/07/martin-lof-meaning.pdf> |

2021-01-18 08:29:13 +0100 | <siraben> | gaussian: i first saw it in Hutton's work https://www.cs.nott.ac.uk/~pszjlh/metrics.pdf |

2021-01-17 18:00:40 +0100 | <bor0> | Just found https://www.cl.cam.ac.uk/archive/mjcg/HoareLogic/Lectures/AllLectures.pdf, might be useful as something to start with.. |

2021-01-13 16:56:36 +0100 | <ij> | http://okmij.org/ftp/papers/LogicT.pdf or the library documentation? |

2021-01-13 05:28:29 +0100 | <pie_> | is https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/comserve.pdf still worth reading? its about ffi to COM |

2021-01-13 03:06:37 +0100 | <iridescent> | oh just trying to do exercise 5 here: https://www.seas.upenn.edu/~cis194/spring13/hw/10-applicative.pdf |

2021-01-13 02:39:13 +0100 | <iridescent> | I'm doing the parser exercise from cis194 (https://www.seas.upenn.edu/~cis194/spring13/hw/10-applicative.pdf), and I'm stuck trying to combine two parsers |

2021-01-09 00:34:05 +0100 | <monochrom> | I might use https://www.cs.dartmouth.edu/~doug/nfa.pdf , its "union" and "xprod" functions, and write "az = ['a'..'z'] ++ xprod (:) ['a'..'z'] az" |

2021-01-08 01:55:27 +0100 | <ephemient> | interesting. https://www.cin.ufpe.br/~haskell/papers/Scripting_.NET_using_Mondrian-Meijer&Perry&Yzendoorn.pdf is quite Haskell-like |

2021-01-04 16:45:44 +0100 | <dminuoso> | kritzefitz: It is described by the original paper https://simonmar.github.io/bib/papers/conc-ffi.pdf |

2021-01-02 22:49:01 +0100 | <gentauro> | b4er: def generated by AI: https://multix.sfo2.cdn.digitaloceanspaces.com/Category%20Theory%20TallCat.pdf (nobody would ever write this BS) |

2021-01-02 01:16:55 +0100 | <halbGefressen> | https://www21.in.tum.de/teaching/fpv/WS20/assets/ex07.pdf |

2021-01-01 11:14:33 +0100 | <gentauro> | I personally like how code reads, specially with the `pipe operator` (slide 9) -> http://blog.stermon.com/assets/talks/2020-11-01_Domain_Driven_Design_DDD_with_Algebraic_Data_Types… |

2020-12-30 13:46:54 +0100 | <Mrbuck> | I think this http://www.cs.cmu.edu/~rwh/theses/okasaki.pdf bookmarked it |