siraben

29 ms·

301.
by siraben 5y ago
The title should correct the spelling to "Buddhist" from "Buddist" EDIT: now it has been corrected, thank you!
302.
by siraben 5y ago
This discussion reminds me of the style guide for a Coq PL formalization project: > No unicode or infix operators for judgement forms. When I use them in my proofs they make perfect sense, but when you use them in yours they're com
303.
by siraben 5y ago
Yeah it might help to see how things are implemented, for instance, even SICP can be a good foundation for this, since they also have interpreters and compilers and talk about things like "primitives" and "derived forms"
304.
by siraben 5y ago
As others have said, I also recommend Types and Programming Languages. > What's the relationship between programming language theory and type theory? I'd say programming language theory is more broad than type theory, for insta
305.
by siraben 5y ago
Yeah, Essentials of Programming Languages is also another great implementation-oriented text, it has some formal things like inductive sets (which pop up in PLT anyway) and also lots of programming exercises.
306.
by siraben 5y ago
Many introductory texts, such as Types and Programming Languages explain the notation thoroughly and start really simple, even starting from the inference rule notation, then talking about reduction of untyped arithmetic expressions, buil
307.
by siraben 5y ago
I study type systems and programming language theory at university, and I encourage friends studying CS to at least have some understanding of type theory, such as well-known type systems (simply-typed, System F) and properties like soundne
308.
by siraben 5y ago
It is quite a new (and unexpected ) change and I haven't seen such a post yet, but someone is probably writing one up now.
309.
Freenode removes hate speech rule(github.com)
30 points by siraben 5y ago|17 comments
310.
by siraben 5y ago
C++ template metaprogramming is a purely functional language embedded in C++, which lets you do crazy things like embed λ-calculus[0] in it. [0] https://matt.might.net/articles/c++-template-meta-programmin...
311.
by siraben 5y ago
One of my favorite esolangs is FRACTRAN[0], because at first glance it seems impossible to write any programs in, but a little insight from number theory (concerning prime factorization) makes it tractable. I even wrote a compiler for FRACT
312.
by siraben 5y ago
Yes! I love the consistency of dependent types. You don't need separate declarations for type aliases or a dozen language extensions to do some type-level evaluation, it's quite uniform. > It's an explosion of possibilitie
313.
by siraben 5y ago
I like that GADTs are a good example of "lightweight dependent types". You don't need to use full-blown dependent types to achieve the following: - type-safe AST representations of a language - type-safe encoding of lambda ca
314.
by siraben 5y ago
One thing that I'd like to add is that using the typed GADT encoding of the AST lets you write a total eval function such as eval :: AST r → r, no need to return a Maybe or Either! In the case without GADTs you couldn't return a b
315.
by siraben 5y ago
As a math and CS student, switching to an e-ink tablet (reMarkable 1 specifically) has made a world of difference in increasing organization and I can freely use it as a scratchpad without worrying about waste or misplacing it. This semeste
316.
by siraben 5y ago
I'm studying programming language semantics and papers like these are quite valuable in understanding type systems of real languages, see also Featherweight Java[0] and Featherweight Go[1]. At first it looks like a lot to take in, but
317.
by siraben 5y ago
I think of it like a dynamic programming type situation. You have notes to be assigned fingers to and the metric is minimizing uncomfortable/awkward hand movements. So the specifics can vary from person to person (and hand to hand), bu
318.
by siraben 5y ago
Sure, for Un Sospiro there were definitely sections that were easy (first few pages are quite repetitive) so not much issue there, but there are runs in the middle where I practiced slowly for a while until it came naturally.
319.
by siraben 5y ago
Can't speak for everyone, but for me, I realized I didn't use my right pinkie to hit backspace or left pinkie to hit tab, and likewise for my 4th fingers, so I would end up moving my wrist. After a bit of practice I didn't ne
320.
by siraben 5y ago
On the TI-84+, assembly programs still work and it's still a test-approved device. I wrote a Forth interpreter[0] that can interop with the syscalls as well [0] https://github.com/siraben/ti84-forth
321.
by siraben 5y ago
Classically trained pianist here (since 7 years old), I like the article's advice. > Use the correct fingering, dynamics, articulation, etc. from the very beginning; you are never going to get around to “fixing” it later. When I was
322.
Mathematical Folklore(en.wikipedia.org)
3 points by siraben 5y ago|0 comments
323.
by siraben 5y ago
See also blynn-compiler[0], made by the same contributors, that bootstrap a Haskell compiler from C (which in term is bootstrapped from hex). [0] https://github.com/oriansj/blynn-compiler
324.
by siraben 5y ago
gccemacs is amazing! I've been using for more than a year on macOS and NixOS, and it's been superb (though from time to time I clear downloaded packages and the native cache just in case). It's definitely an impressive feat
325.
by siraben 6y ago
What systems are you referring to in the "YAML driven world"?
326.
by siraben 6y ago
Could you elaborate what you mean by this? Nix has lazy evaluation so as Nixpkgs grows it doesn't perceptibly change how long package installations, building, etc. take.
327.
by siraben 6y ago
FYI nix-env operations are atomic and can be rolled back instantly, including upgrades. $ nix-env --rollback > The suggestion in the github issue was to instead use an unofficial third party package for basic package management. S
328.
by siraben 6y ago
Regular Nix user here, I agree with your points regarding the language's peculiarities, and adding on a few points: > 1. Where does the semicolon go? Reading code makes it feel arbitrary, but really the only time a semicolon is used
329.
by siraben 6y ago
The Scheme dialect of Lisp is perhaps my favorite for how small the core is (and hygienic macros are an elegant solution to avoiding accidental captures). The R5RS language report also specifies the formal denotational semantics of the lang
330.
by siraben 6y ago
I think sheet music is a great way to see how a piece works since things are laid out spatially, and complex or subtle patterns can be teased out (e.g. voices in a Bach fugue). I often follow the sheet music as I listen as well.

More ›