5 ms·

I think we are more or less in violent agreement here. Our disagreements are on the fringes, and could well just be a result of my ignorance or misunderstandin

• gugagore 1y ago
  Ah, your example reminds me of a quirk in Julia where some methods are type stable, and others are not. (This is just an aside. I'll provide a response in another comment.) ``` julia> sqrt(-1.0) ERROR: DomainError with -1.0: sqrt was called with a negative real argument but will only return a complex result if called with a complex argument. Try sqrt(Complex(x)). Stacktrace: ``` The justification is "type stability". The return type of a function should be constant across different values of the same input type. This is not a requirement, but a guidance that informs much of the design, including the DomainError on `sqrt(-1)`, instead of returning a complex result. However, the same choice is not made universally: ``` julia> sqrt([1 0; 0 1]) 2×2 Matrix{Float64}: 1.0 0.0 0.0 1.0 julia> sqrt([-1 0; 0 -1]) 2×2 Matrix{ComplexF64}: 0.0+1.0im 0.0+0.0im 0.0+0.0im 0.0+1.0im ```
  • lisper 1y ago
    > ERROR: DomainError with -1.0: > sqrt was called with a negative real argument but will only return a complex result if called with a complex argument. Try sqrt(Complex(x)). This is the sort of thing that drives me absolutely nuts. In no possible world that I can imagine is generating an error a more useful result than returning a complex value. I could forgive it if the system didn't know about complex numbers, but in this case it is clear that the system is perfectly capable of producing a correct and useful result, but it just refuses to do so in service of some stupid ideology. I have zero tolerance for this sort of nonsense.
    • gugagore 1y ago
      I'm not sure how familiar you are with Julia, but it is very spiritually aligned with lisp. The reason for the DomainError is "type stability" and it's not stupid ideology unless you consider high-performing numerical code stupid ideology. To your point, goals can differ.
      • lisper 1y ago
        I know very little about Julia. It is on my list of Things To Look Into Some Day. > type stability [is] not stupid ideology unless you consider high-performing numerical code stupid ideology. "Stupid ideology" may have been putting it a bit strongly, and there are times when I want numerical code to be performant. But I don't always want that, and I don't want a language that makes me pay for it even when I don't want it. Almost always I prefer high-fidelity [1] over speed. But even when I want speed, I always want to start with high-fidelity, get that working, and then make it fast if I need to. 99% of the time I don't need to because 99% of my code turns out to be I/O bound or memory-latency bound. It's extremely rare for my code to be compute-bound, and even in those cases I can almost always just find a C library somewhere that someone else has written that I can call through an FFI. So for me, a programming language that forces me to pay for run-time performance whether I want it or not has negative value. But honestly, I can't actually think of a single instance in my entire 40 year career when the run-time performance of my CL code was a limiting factor. The limiting factor to my productivity has almost always been my typing speed and the speed of my internet connection. --- [1] By "high fidelity" I mean how well the semantics of the language reflects the domain model, which, in the case of numerical code, is mathematics. Fixnums and floats are a fast but low-fidelity model because they don't actually behave like the integers and reals that they purport to model. Bignums and rationals are a high(er)-fidelity model. A really high fidelity model would let me do something like (* (sqrt 2) (sqrt 2)) and get back exactly 2 by having some sort of exact representation of algebraic numbers. I don't know of any programming language that provides that natively, but some languages, like CL and Python, let me extend the language to add that kind of capability myself. For me, that kind of extensibility is table stakes.
• gugagore 1y ago
  > The intrinsic (Church) view builds meaning into the syntax itself. I shouldn’t have phrased it that way --- the distinction between syntax and semantics is awkward for me, especially when there are discussions of "static" vs "dynamic" semantics. What I meant is closer to this: in intrinsic systems, the typing rules define which terms are meaningful at all. Terms (programs) that do not type do not have meaning. This is the sense in which "correct programs get rejected". > Programs don't have meaning, they are descriptions of processes. Despite my confusion about the previous point, one clear thing I can point to, however, is the funny realization that there are some programming languages where the primary point is not to run the program, but just to type check it. This is the case for many programs written in languages such as Lean and Rocq. In these situations, the programs do have meaning and are not descriptions of processes. A much more common example that makes it clear that programs aren't just descriptions of processes is in the "declarative" languages. In SQL different execution plans might implement the same logical query, and writing down the SQL is less about describing a process and more about assertion or specification. > depends on your goals That’s fair, and I agree (perhaps violently??) I focused on your mention of Gödel's incompleteness because it’s often brought up (as I think you did here) to cast doubt on the viability of static typing in practice, but I don't think it does that at all. I think what casts much more doubt is a connection that I have felt is missing for a while now, which is about interactivity or perhaps "live programming". The Lean and Rocq interactive theorem proving environments are very "live", but not with a REPL. It's fascinating. But it's also because those programs, in a sense, don't do anything... 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.
  • lisper 1y ago
    > 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/ https://coalton-lang.github.io/