33 ms·

> Those concerns seem worlds away from the kinds of things type theorists care about. It’s true there’s a tradition, voiced by Dijkstra, that emphasizes correc

> Those concerns seem worlds away from the kinds of things type theorists care about. It’s true there’s a tradition, voiced by Dijkstra, that emphasizes correctness at a point in time, sometimes at the expense of long-term adaptability. > “Unfathomed misunderstanding is further revealed by the term software maintenance, as a result of which many people continue to believe that programs – and even programming languages themselves – are subject to wear and tear. Your car needs maintenance too, doesn’t it? Famous is the story of an oil company that believed that its PASCAL programs did not last as long as its FORTRAN programs ‘because PASCAL was not maintained’. “ (Dijkstra, “On the cruelty of really teaching computer science“, EWD1036 (1988)) As for Gödel, I’d say invoking incompleteness is like invoking Russell’s paradox — important for foundations, but often a distraction in practice. And ironically, type theory itself arose to tame Russell’s paradox. So while Gödel tells us no system can prove everything, that doesn’t undercut the usefulness of partial, checkable systems — which is the real aim of most type-theoretic tools. Among the “three poisons,” I’m most comfortable rejecting “correct” code. If a system can’t see your reasoning, how sure are you it’s correct? Better to strengthen the language until it can express your argument. And since that relies on pushing the frontiers of our knowledge, then there are times when you need an escape hatch --- that is 50% of how I understand "dynamicism". The intrinsic vs. extrinsic view of types cuts to the heart of this. The extrinsic (Curry) view — types as sets of values --- aligns with tools like abstract interpretation, where we overlay semantic properties onto untyped code. The intrinsic (Church) view builds meaning into the syntax itself. In practice, we need both: freedom to sketch, and structure to grow. ----- On the cognitive load of remembering names like `EllipticCurveAdd(P1, P2)` vs. just writing `P1 + P2` --- that pain is real, but I don't really see it as being about static typing. It’s more about whether the system supports good abstraction. Having a single name like `+` across many domains is possible in static systems --- that’s exactly what polymorphism and type classes are for. The most comfortable system for me has been Julia, because of pervasive multiple dispatch, and this focus on generic programming correctness. I don't think this works well unless the multiple dispatch is indeed pervasive (which requires attention paid to performance), and I'm pretty sure CLOS falls short here (I am no expert on this). The difference between Julia and "static types" here is more about whether you are forced to content with precisely the meaning of `+`. In the type class view, you bundle operations like `+` and `*` into something like "Field". Julia is much more sloppier and simultaneously flexible. It does not have formal interfaces (yet), which allows interfaces to emerge organically in the ecosystem. It is also a pretty major footgun in very large production use cases.... FWIW, I have been a huge fan of "Lisping at JPL" for many years now and it is validating in many ways. I especially enjoyed the podcast with Adam Gordon Bell. This is also validating: https://mihaiolteanu.me/defense-of-lisp-macros https://mihaiolteanu.me/defense-of-lisp-macros (discussed on HN).

lisper 1y ago
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 misunderstanding. That said... > invoking incompleteness is like invoking Russell’s paradox — important for foundations, but often a distraction in practice Yes, but the operative word here is "often". "Often a distraction" is logically equivalent to "sometimes relevant". The problem is that whether or not it is relevant to you depends on your goals, and different people have different goals. For example, one of my goals is pedagogy, and so it's really handy for me to be able to fire up a CL REPL and do this: Clozure Common Lisp Version 1.12.1 (v1.12.1-10-gca107b94) DarwinX8664 ? (expt (sqrt -1) (sqrt -1)) #C(0.20787957 0.0) so that I can tell a student, "See? i to the i is a real number! Isn't that cool?" But if your goal is to build a social media site that has no value for you. Different strokes. > The intrinsic (Church) view builds meaning into the syntax itself. This is what I don't get. I can't even wring any coherent meaning out of the phrase "build meaning into the syntax itself". Programs don't have meaning, they are descriptions of processes. Programs don't mean things, they do things. Even for natural language sentences, which do mean things, I don't understand what it could possibly mean to build meaning into the syntax. "The dog ate my license plate" has meaning but "The dog ate my car crash" does not despite the fact that those two sentences are syntactically identical. (BTW, imbuing syntax with meaning sounds more like Chomsky than Church to me. But what do I know?) > I’m most comfortable rejecting “correct” code. Again, one of my goals is pedagogy. Towards that goal I once wrote this: https://flownet.com/ron/lambda-calculus.html https://flownet.com/ron/lambda-calculus.html After writing that, I thought this might be a good time to learn Haskell. If CL is good for showing off the lambda calculus surely Haskell will be even better? I'm guessing I don't need to explain to you why that did not go to plan. And BTW, thanks for the kind words.
- 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

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 misunderstanding. That said... > invoking incompleteness is like invoking Russell’s paradox — important for foundations, but often a distraction in practice Yes, but the operative word here is "often". "Often a distraction" is logically equivalent to "sometimes relevant". The problem is that whether or not it is relevant to you depends on your goals, and different people have different goals. For example, one of my goals is pedagogy, and so it's really handy for me to be able to fire up a CL REPL and do this: Clozure Common Lisp Version 1.12.1 (v1.12.1-10-gca107b94) DarwinX8664 ? (expt (sqrt -1) (sqrt -1)) #C(0.20787957 0.0) so that I can tell a student, "See? i to the i is a real number! Isn't that cool?" But if your goal is to build a social media site that has no value for you. Different strokes. > The intrinsic (Church) view builds meaning into the syntax itself. This is what I don't get. I can't even wring any coherent meaning out of the phrase "build meaning into the syntax itself". Programs don't have meaning, they are descriptions of processes. Programs don't mean things, they do things. Even for natural language sentences, which do mean things, I don't understand what it could possibly mean to build meaning into the syntax. "The dog ate my license plate" has meaning but "The dog ate my car crash" does not despite the fact that those two sentences are syntactically identical. (BTW, imbuing syntax with meaning sounds more like Chomsky than Church to me. But what do I know?) > I’m most comfortable rejecting “correct” code. Again, one of my goals is pedagogy. Towards that goal I once wrote this: https://flownet.com/ron/lambda-calculus.html https://flownet.com/ron/lambda-calculus.html After writing that, I thought this might be a good time to learn Haskell. If CL is good for showing off the lambda calculus surely Haskell will be even better? I'm guessing I don't need to explain to you why that did not go to plan. And BTW, thanks for the kind words.

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