catnaroek

6 ms·

1.
by catnaroek 8y ago
Calling HLists “collections” is misleading. In spite of their name, HLists are actually record types. The only actual list involved is a compile-time list of component types used to form a record type. To give a perhaps odious but relatable
2.
by catnaroek 8y ago
In general, Haskell does not do parametric polymorphism through monomorphization. In particular, higher-rank polymorphism becomes unusable if polymorphism is implemented through monomorphization. On the other hand, if I recall correctly, Ru
3.
by catnaroek 8y ago
Two words: loop invariant. Implement a system that figures out the right loop invariant given a problem description (expressed however you want), and you will have made a lot of progress.
4.
by catnaroek 8y ago
That's actually Brian Kernighan. Dijkstra would have never advocated debugging to begin with.
5.
by catnaroek 8y ago
Oops, sorry, yes.
6.
by catnaroek 8y ago
Optionals are a better alternative to null. They compose better (i.e., they nest) and play nicely with data abstraction (i.e., you can define an abstract type that hides the fact that its underlying representation is optional), unlike null.
7.
by catnaroek 8y ago
Typed Racket is more ambitious than other attempts at adding types to an underlying untyped language. Namely, Typed Racket guarantees that typed code is never to blame for certain contract violations, and, if any such contract violation hap
8.
by catnaroek 8y ago
> It doesn't try to analyze and compare existing programming languages. It does. For example, this theory identifies when and how incorrectly designed programming languages fail to enforce abstractions, very much like how the theory
9.
by catnaroek 8y ago
I don't understand in what sense programs can be called “differentiable”. Is the space of programs modulo observational equivalence a manifold to begin with? (I don't think it's Hausdorff or even T1, but I could be wrong.) Th
10.
by catnaroek 8y ago
> Safety > Variables are immutable by default, globals are not allowed, functions are pure. This is a huge non-sequitur.
11.
by catnaroek 8y ago
You are badly conflating some issues here. How to implement automatic memory management is a runtime design issue. How to enforce proper non-memory resource management is a language design issue. Nothing forbids an implementation of a s
12.
by catnaroek 8y ago
> The problem is, functional programming languages are almost always harder to read than other languages. Haskell is the obvious example There are many legitimate reasons to dislike Haskell, such as being hard to parse mechanically, but
13.
by catnaroek 8y ago
I don't see anything wrong with rose trees: datatype 'a tree = T of 'a * 'a tree list Do you?
14.
by catnaroek 8y ago
Not too long was it figured out how to reconcile subtyping with type inference. However, this requires doing subtyping in a very specific way, which most users of languages with subtyping will not find pleasing. In particular, the design o
15.
by catnaroek 8y ago
Lately, I am of the idea that the real problem with how we do concurrency is that we have yet to figure out a way to do it without first-class procedures. When we spawn a thread, even in a low language such as C, we use something to the eff
16.
by catnaroek 8y ago
> Java's semantics are pass-by-value only of you consider that the "values" that are being passed are pointers. All values in Java are indeed either primitives or pointers. You cannot define your own values! How is anyone
17.
by catnaroek 8y ago
> However, I am considering an even more general scheme, where it is possible to define what is meant by addition, multiplication, etc., for new datatypes unimagined by the language designer So, um, like this? signature RING =
18.
by catnaroek 8y ago
With mere “guidelines”, there is no practical, unambiguous way to establish without a shadow of doubt that a function implemented using unsafe Rust upholds the safety guarantees of safe Rust. So I want a proper formal semantics, maybe not f
19.
by catnaroek 8y ago
Will there ever be a formal semantics for unsafe Rust?
20.
by catnaroek 8y ago
> Heck, R isn't really that accessible to most programmers either. R is objectively a bad programming language. However, it is by no means inaccessible. I have no statistics background whatsoever, and I managed to learn enough R to
21.
by catnaroek 8y ago
Type soundness is always relative to a kind of error that a type system is designed to rule out. So any type system can be made trivially sound by decreeing that its purpose is not to eliminate any kind of error. This is why “mathematically
22.
by catnaroek 8y ago
> You can't isolate unsafe operations from only having isolated effects to the block of code flagged. You can focus your manual verification efforts on unsafe code. That is pragmatic. “Well, shit happens, and I can do nothing abou
23.
by catnaroek 8y ago
> Programmers often use other verification tools like unit testing or contracts to get strong assurances of similar properties. Neither unit testing nor contracts are verification tools.
24.
by catnaroek 8y ago
I don't need to “hope” for anything. All I have to do is document the program's preconditions.
25.
by catnaroek 8y ago
> But at the same time, people often call either flawed proofs or purported proofs formal proofs in a looser sense. They are wrong. A purported proof is only a proof if it is actually correct. If you cannot reliably come up with a proof,
26.
by catnaroek 8y ago
Automated, huh? There is no replacement for using your brain, and reasoning abstractly about the preconditions and postconditions of program fragments.
27.
by catnaroek 8y ago
Yes! This is the nice moment when the other party in the debate starts to back off from their original position, which, I shall remind you, was: > My reasoning skills exceed that of my compiler and I can thus determine that certain desig
28.
by catnaroek 8y ago
Unit tests don't constitute “formalization” by any stretch of the term's meaning.
29.
by catnaroek 8y ago
Nah, Standard ML will do just fine.
30.
by catnaroek 8y ago
You can only deem it obvious if you can actually prove it. --- @winstonewert > True, but the key word is "can". I could write a proof that my dynamically typed programs are correct If you could actually write the proof, then yo

More ›