curryhoward

12 ms·

61.
by curryhoward 7y ago
I believe they are just saying that tail calls can be used in a mutually recursive way without consuming unbounded memory. They said "self tail recursion" is not necessary but you interpreted it as "tail recursion is not nece
62.
Show HN: Docuum – LRU Eviction of Docker Images(github.com)
10 points by curryhoward 7y ago|0 comments
63.
by curryhoward 7y ago
> all those things you're mentioning are side effects and are captured by the same concept, of representing effects by carrying a parameter through a chain of function calls No. The state and environment monads fall under that rubri
64.
by curryhoward 7y ago
> by carrying a "world" parameter that represents the state being modified From this, it's clear you've never read and understood Moggi's seminal paper. Monads are functors with some extra monoidal structure. The
65.
by curryhoward 7y ago
> In a typical PL context "effects" is always short for algebraic effects The word "effects" has a long and storied history in programming language theory that predates algebraic effects/handlers by decades. The
66.
by curryhoward 7y ago
The author makes it crystal clear that she is not advocating this as a mental model for the execution of the query: Database engines don’t actually literally run queries in this order because they implement a bunch of optimizations to make
67.
by curryhoward 7y ago
> Afaik, Haskell is a realization of the (typed!) lambda calculus. Lisps aren't because they don't do lazy evaluation. Lazy evaluation is just one possible operational semantics for a lambda calculus. Eager evaluation is anothe
68.
by curryhoward 7y ago
No. One can come up with a PEG for a language consisting only of strings with balanced parentheses. That language cannot be described by a regular grammar.
69.
by curryhoward 7y ago
In a previous life when I was at MIT, I took a course from Gerry Sussman called Structure and Interpretation of Classical Mechanics [1]. There was one lecture where he taught us Scheme, which is a simple enough language that it can be taugh
70.
Show HN: Toast – A tool for running tasks in containers(github.com)
10 points by curryhoward 7y ago|0 comments
71.
by curryhoward 8y ago
I made this a few years ago and use it to memorize phone numbers, API keys, etc. Here's a short writeup about how it works: https://www.stephanboyer.com/post/111/huffgram-convert-strin... Happy to answer any
72.
Show HN: Huffgram helps you memorize data(huffgram.com)
9 points by curryhoward 8y ago|3 comments
73.
by curryhoward 8y ago
I think this article makes a simple concept seem unnecessarily convoluted. The first paragraph says: > This very complex object coming from the Category Theory is so important in functional programming that is very hard to program withou
74.
Typeclasses in perspective(diogocastro.com)
2 points by curryhoward 8y ago|0 comments
75.
by curryhoward 8y ago
This is actually the Z combinator, which is the eta expansion of the Y combinator. The Y combinator only works in languages with non-strict semantics, but JavaScript is call-by-value.
76.
by curryhoward 8y ago
I think it's only more difficult to read initially, when you aren't used to it. I actually find it more natural than the more mainstream function call syntax after having used it for a while. When I look at code in C-family langua
77.
by curryhoward 8y ago
> How does "map inc [1, 2, 3]" know not to do "inc [1, 2, 3]" and then pass the result to "map"? I'm guessing it's a language rule, but it could be the type system. That is a lot like saying: in th
78.
Show HN: Noteref – Maintain references to notes in your codebase(github.com)
1 points by curryhoward 8y ago|1 comments
79.
by curryhoward 9y ago
> Do you have an example of a language that does what you're looking for? Dependently typed programming languages such as Coq and Idris let you write proofs about your programs. These languages are fairly academic, and most engineer
80.
by curryhoward 9y ago
By making the master branch protected in GitHub and making the CI check for Travis required. Docs: https://help.github.com/articles/enabling-required-status-ch...
81.
by curryhoward 9y ago
* but it rules out some legitimate programs which terminate. (Typo, but too late to edit the original comment.)
82.
by curryhoward 9y ago
> Do any mainstream languages have a sound foundation like that? I can think of a few languages that started from a formal theory (e.g., Eff [1]), but none of them are "mainstream". There was a mostly successful attempt [2] at
83.
by curryhoward 9y ago
> I believe Coq uses a variant of a bidirectional type inference engine, which is quite usable in practice. Edit (too late to edit the original comment): After thinking about the kinds of type errors I've seen in my proofs, I think
84.
by curryhoward 9y ago
Wow, this is amazing. Can you share a link to the full module with proofs? I'd love to compare it to the Coq version.
85.
by curryhoward 9y ago
> I prefer Isabelle myself, as I find its proofs more readable in a traditional mathematical sense. Just curious, what makes Isabelle easier to read? I haven't tried it.
86.
by curryhoward 9y ago
Practically all of mathematics can be formalized in Coq. One notable exception is the internal consistency of Coq itself (due to Gödel's first incompleteness theorem, I believe). Coq's logic is intuitionistic, which means it'
87.
by curryhoward 9y ago
> so why can't we have a programming language that gives you a full blown logic system Most dependently typed programming languages, including Coq, give you the ability to basically "do logic" in a mostly unrestricted way
88.
by curryhoward 9y ago
There are two languages to discuss here: 1) The underlying pure functional language that forms the logical basis for Coq (called "Gallina"). It is not possible to write a program which runs forever in this language, because all re
89.
by curryhoward 9y ago
> Unfortunately, on the other, I've never been able to read Coq proofs the way I can read programs. Probably a lack of experience, I guess. I don't think it's a lack of experience on your part. I worked with some people at
90.
by curryhoward 9y ago
My experience is: formally proving something in Coq is not a prerequisite for understanding it, but understanding it is a prerequisite for formally proving it in Coq. So if you get Coq to accept your proof, it's a good sign that you un

More ›