Note: This channel on freenode is currently not being logged anymore. The logs are reproduced here for posterity.

Show unique PDF links →

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 +0200ski. 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 +0100ski. 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