Comment by lisper | Hacker News Reader

Comment by lisper | Hacker News Reader

Parent Full thread

> Lean and Rocq

Yep, I get that. But I don't think of these as programming languages, I think of them as proof assistants. Related for sure, but different enough that IMHO it is unwise to conflate them.

> SQL

Again, a whole different beast. Database query languages are distinct from programming languages which are distinct from proof assistants. All related, but IMHO they ought not to be conflated. There is a reason that SQLite3 is written in C and not in SQL.

> it’s often brought up (as I think you did here) to cast doubt on the viability of static typing in practice

I bring up Godel just to show that static typing cannot be a panacea. You are necessarily going to have false positives or false negatives or both. If you're OK with that, fine, more power to you. But don't judge me if I'm not OK with it.

> There is a type theory rabbit hole, for sure. I think there is also a Smalltalk and Lisp rabbit hole. I would like them to meet somehow.

You want Coalton :-)

https://coalton-lang.github.io/

> But I don't think of these as programming language

I don’t want to get too caught up in what counts as a programming language, but you can absolutely write programs in a language like Lean, e.g. computing factorial 10. The fact that you can also write proofs doesn’t negate a system's status as a programming language. It’s worth noting that the official Lean documentation reflects this dual use: https://lean-lang.org/documentation/.

So there’s no conflation... just a system that supports both orientations, depending on how you use it.

> SQL [...] ought not to be conflated

I agree that SQL isn’t a general-purpose programming language, but you said something to the effect of "I don't understand what meaning a program has beyond what it does", and if you know about SQL, then I think you do understand that a program can have "computational meaning" that is separate from its meaning when you run it through an interpreter or processor.

> You want Coalton :-)

Thanks for the pointer. I am going to read https://coalton-lang.github.io/20211212-typeclasses/ , hoping to eventually achieve clarity on the relation between multiple dispatch and type classes..

That said, my interest in generic programming pushes pretty hard toward dependent types. I’m increasingly convinced that many patterns in dynamic programs, especially those involving runtime dispatch, require dependent types in order to be typed. Coalton might help me understand better the relation also between interactivity and static typing. But it's not going to be a panacea either ;)

> I bring up Godel just to show that static typing cannot be a panacea. You are necessarily going to have false positives or false negatives or both. If you're OK with that, fine, more power to you. But don't judge me if I'm not OK with it.

If you want a static type system that is sound and decidable, it will necessarily reject some programs that would behave just fine at runtime. That’s not really Gödel’s fault. It follows more directly from the halting problem.

But that's a quibble, and I still know what to make of your stance. The thing you're not okay with is having the system "get in your way", which is your false positive (the polarity doesn't matter, if that's what I'm getting wrong). The point is you want to say "my program is correct, now run it for me", and you will hate if the system rejects it.

What you don't hate is runtime type errors.

There is no judgement on my side on the preferences. But I'm confused. If you don't have any static type checking, then it's like having a system that always gives negatives, and some of those will be false (again, assuming I got the polarity right. if not, just swap here and earlier). I'm pretty sure you're okay with this, even though the text of your last message leads me to believe otherwise.

To summarize, there’s a fundamental trade-off:

- If you want a sound type system (never accepts unsafe programs),

- And you want it to be decidable (terminates on all inputs),

- Then it must reject some safe programs.

If you're not okay with that, then... sorry :D

> you want to say "my program is correct, now run it for me"

No. I want to say "Run this program whether or not it is correct because I just want to see what it does in its current state." Sometimes I know that it will produce an error and what I want is the information in the backtrace.

> What you don't hate is runtime type errors.

It depends. I hate "NIL is not of the expected type" errors. So I have a bee in my bonnet about that too, it's just not something that comes up nearly as often as static-vs-dynamic. I think typed nulls are a good idea, but very few languages have those.

> If you don't have any static type checking

I love static type checking. The more information I can get at compile time the better. I just think that the output of the type checker should be warnings rather than errors.

Reply on news.ycombinator.com