catnaroek

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 analogy, a form is a list of questions, but a filled form is not a list of answers - it is a record of answers to the questions in the form.

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, Rust only supports higher-rank polymorphism for lifetimes, which neither have nor need a runtime representation. This is why monomorphization is a viable implementation strategy for Rust generics.

(Aside: Type checkers essentially see recursive function definitions as applications of a fixed point operator to non-recursive functions. If your function has a rank-1 type but uses polymorphic recursion, the type checker sees it as the application of a rank-2 fixed point operator to a non-recursive function. This is why I see polymorphic recursion as “morally higher-rank polymorphism”, even when the type signatures in your code are ostensibly rank-1 ones. Polymorphic recursion is widely used in Haskell.)

However, IMO, you only need rank-1 polymorphism 95% of the time anyway, so optimizing for the common use case is a good strategy. By far, the main use case for generics is implementing efficient and reasonably reusable data structures and algorithms in a reasonably type-safe way. For this use case, monomorphization and aggressive inlining of small functions are evidently the right things to do. Other uses of generics (say, streaming I/O frameworks) strike me as a lot more questionable.

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.

That's actually Brian Kernighan. Dijkstra would have never advocated debugging to begin with.

Oops, sorry, yes.

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.

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 happens, it will be properly traced back to an offending piece of untyped code. This is what makes gradual types gradual (as opposed to merely optional), alas, it is also what has been found to have unacceptable overhead.

Relevant paper and talk:

http://www.ccis.northeastern.edu/home/types/publications/gra...

https://www.youtube.com/watch?v=1u1JGwmW0IQ

> 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 of database normalization identifies when and how incorrectly designed database schemata fail to enforce data integrity constraints.

But perhaps what you mean is “it doesn't try to view existing programming languages under an unwarranted positive light”.

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.)

The examples given in the article are merely derivatives of ordinary mathematical functions defined by ordinary mathematical expressions - in particular, there are no sequencing, no conditionals and no loops. So why call them “differentiable programs” when you are actually dealing with ordinary differentiable functions from good old 19th century analysis? We need urgent improvements in the intellectual honesty department.

> Safety

> Variables are immutable by default, globals are not allowed, functions are pure.

This is a huge non-sequitur.

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 safe-Rust-like language with a garbage collector. Destructors would still be called deterministically, and destructed objects would still be unusable afterwards, as mandated by the language's semantics. But memory will only be reclaimed during the next garbage collection cycle.

There are other (better!) reasons against cross-language interoperability, though, such as the reduction in static guarantees to an unusable lowest common denominator.

> 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 being hard to read is not one of them.

> F# and other languages ML-style syntax are probably the easiest to read.

The syntax of ML's module language is pretty complicated. You cannot look at those “where type” (SML) and “with type” (OCaml) clauses and tell me with a straight face that they were meant to be easy to read. This syntax makes translucent ascription harder to read than it ought to be. It is so bad that many[0] people work around it in various ways, like using the combination of generative datatypes and transparent ascription as a poor man's translucent ascription.

As for F#, I would not call it ML-style, precisely due to the inability to express modular abstraction.

[0] Relative to the size of the ML community, of course.

I don't see anything wrong with rose trees:

    datatype 'a tree = T of 'a * 'a tree list

Do you?

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 of the type system must pay very close attention to issues of polarity and existence of certain universal objects in the categories of types. This work caters more to designers and users of ML-style languages who want to add subtyping, than to designers and users of more traditional languages who want to add type inference.

https://news.ycombinator.com/item?id=13781467

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 effect of:

    launch_thread(function, perhaps, some, initial, data);

The trouble with this approach to concurrency is twofold:

(0) It forces a hierarchical structure where one continuation of the branching point is deemed the “parent” and the others are deemed the “children”. In particular, if the forking procedure was called by another, only the “parent” continuation may return to the caller. This is unnatural and unnecessarily limiting. Even if you have valid reasons to guarantee that only one continuation will yield control back to the caller (e.g., to enforce linear usage of the caller's resources), the responsibility to yield back to the caller is in itself as a resource like any other, whose usage can be “negotiated” between the continuations.

(1) It brings the complication of first-class procedures when it is often not needed. From a low-level, operational point of view, all you need is the ability to jump to two (or more) places at once, i.e., a multigoto. There is no reason to require each continuation to have a separate lexical scope, which, in my example above, one has to work around by passing “perhaps some local data” to `launch_Thread`. There is also no reason to make “children” continuations first-class objects. If you need to pass around the procedure used to launch a thread between very remote parts of your program, chances are your program's design is completely broken anyway. These things distract the programmer from the central problem in concurrent programming, namely, how to coordinate resource usage by continuations.

> 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 supposed to call this a high-level language?

> 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 =
    sig
      type t
      val + : t * t -> t
      val * : t * t -> t
      val ~ : t -> t
    end

> Extensible generic operations are not for the faint of heart. The ability to extend operators after the fact gives both extreme flexibility and ways to make whole new classes of bugs!

This is precisely why parametric polymorphism is superior to ad-hoc polymorphism as a way to enable programs to work in previously unanticipated situations. Don't work with concrete use cases, work with the minimum abstract requirements that allow your program to work!

> On the other hand, some mutations will be extremely valuable. For example, it is possible to extend arithmetic to symbolic quantities.

So, for example, like this?

    functor PolynomialRing (R : RING) : RING =
    struct
      type t = R.t list
      
      fun xs + nil = xs
        | nil + ys = ys
        | (x :: xs) + (y :: ys) = R.+ (x, y) :: xs + ys
      
      (* define multiplication and negation too... *)
    end

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 for all of Rust, but at least for a fragment interesting enough to express lifetime and mutability concerns. In particular, I want a formal account of interior mutability.

Will there ever be a formal semantics for unsafe Rust?

> 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 be dangerous in a mere week. Other than the 1-based indexing and the utterly disgusting dynamic dispatch mechanism (you could simply not to use the latter), R is surprisingly pleasant to use. What I enjoyed the most is that vectors and matrices are first-class values, not objects that are referred to through pointers. It's probably copy-on-write under the hood, but I don't need to care. Hallelujah!

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 civilized” is a much better term. For example, even if you don't mind null pointer exceptions, it is not mathematically civilized to add one extra case to everyone's case analyses.

> 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 about it” is not.

> 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.

I don't need to “hope” for anything. All I have to do is document the program's preconditions.

> 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, not mere purported proofs, then just be honest and say so. We are not in a consultant-client relationship, so you gain nothing by lying about your skills to me.

> You know that my point was that a manually verified proof might still be wrong.

Only if you cannot reliably come up with correct proofs.

> And yet rather than addressing that point you decide to evade it by an ill-considered nit pick on whether an incorrect proof is still a proof.

It is not an “ill-considered nitpick”. It is essential to my point. If you can prove that your assertions hold, you do not need to check them dynamically. (Of course, this is logically a triviality, and it is awful that I need to explicitly make this point.)

Automated, huh? There is no replacement for using your brain, and reasoning abstractly about the preconditions and postconditions of program fragments.

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 designs are type-safe that my compiler cannot.

Anyhow. Back to your last comment:

> Even if I write a formal proof, I'm not guaranteed that my program won't index out of bounds.

If you actually come up with a proof, you are completely guaranteed that the proven statement is true.

> Formals proofs have errors in them all the time.

Correction: Purported proofs often actually aren't proofs. It is not a proof if it is wrong.

> I want dynamic checks to catch me in those cases.

Thanks for making my point for me! Self-quotes are decidedly not tasteful, but this situation calls for a reminder:

> It is useful (again, according to proponents, not me) to consider these inconsistent attempts valid programs so that programmers can obtain example-based feedback about the consequences of their designs. Logic and abstract reasoning are not everyone's forte, after all.

Anyhow. Back to your last comment:

> Further to the point, let me reiterate: programmers do not (in almost all cases) write these proofs you are talking about.

This is just a statement of fact, which is true, indeed. But it doesn't support your original position in any way.

Unit tests don't constitute “formalization” by any stretch of the term's meaning.

Nah, Standard ML will do just fine.

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 you would not want the dynamic checks, as all they offer is protection against errors that you can prove you have not made.

> or that my functions do not index out of bounds, but I don't.

Are you actually sure you can?

---

@AnimalMuppet

> By a certain point, you've seen enough of them that you don't have to prove it, you can just see it.

If all your loops are so similar to each other that you can “just see” that an iteration pattern is correct, you should consider writing an iterator library, so that others can benefit from your hard-earned wisdom without going through the pain themselves.

Or else, if you are implying that you could be given an arbitrary loop and “just see” that it is correct, I am afraid you are wrong.

> But of course, everybody thinks they're at that point well before they actually are...

I have never even entertained the possibility.