Back

@Jose_A_Alonso "Part of what makes Lisp distinctive is that it is designed to evolve. As new abstractions become popular (object-oriented programming, for example), it always turns out to be easy to implement them in Lisp."

I wonder if we might implement static type checking (and patterns too.) in Common Lisp, turning it into a kind of ML.

@AmenZwa

@fl @Jose_A_Alonso Great stuff, ain't it?

I know a handful of LISP/Scheme implementations that support simply-typed 𝜆-calculus with pattern matching—the Typed Racket being the best known. But they all lean more toward Python 3 and less toward ML in their implementation of the type system.

I'd say though that much of what counts as the "traditional strengths" of LISP was derived from its homoiconicity, its functional core, and its imperative addons, but not from its typyness, for there was no type system, originally. This makes LISP way of working markedly different from ML way of working.

@dougmerritt
...variables don't have types, values have types...

I forgot the author but there was a great paper from the early 80s included in IPE something like Programming Environments Need Dynamic Types, the gist of which was that you simply don't know how much memory needs to be allocated for a type that is going to be invented tomorrow, and in statically typed languages, the practice is to fake dynamic typing using arrays or something anyway.
@AmenZwa @fl @Jose_A_Alonso

@dougmerritt @fl @Jose_A_Alonso Perhaps they conflated the “homoiconitity” concept with a “macro” based implementation, and had assumed that any language with a macro facility is homoiconic.

@AmenZwa @fl @Jose_A_Alonso
I like that your impulse is to look for a way to think the best of people.

@dougmerritt @fl @Jose_A_Alonso I like that.There is much truth in that insight, my friend.

@fl @dougmerritt @Jose_A_Alonso As Doug pointed out, we computer scientists must strive to be more measured when we speak, even on social media, especially given English’s inherent imprecision.

Yes, of course, C is statically typed, only not as strongly as Pascal. In some sense, even the binary code being executed (interpreted) by the ALU is "typed"—32-bit, 64-bit, Int, Float, Flag, etc.

It is often entertaining to hear FP gurus speak informally of LISP’s “untyped” nature, “removal” of type information by the compiler, and so on. I suppose to a staunch type theorist, anything less than homotopy might well be “untyped”.

@AmenZwa @dougmerritt @Jose_A_Alonso I know a language that is definitely untyped but it is not a programming language. It is TLAPLUS, a language and software designed by Lamport. The aim of this language and software is to design algorithms before coding them in a programming language. Very interesting. For many reasons.

It is untyped because Lamport didn't want types. He explains that types should be a proven feature not an enforcement. But I think we must say that it is almost untyped because it defers calculations on integers to the processor and then they are limited to 64 bits. He should remove this limitation in my opinion. It is not so difficult.

@AmenZwa @dougmerritt @Jose_A_Alonso Come to think of it, it is not the language to describe the algorithms that is "typed" (in the sense that the numbers must be 64 bits long), nor the proof system, it is the Model Checker. It is a side tool. But an important one.

@AmenZwa @dougmerritt @Jose_A_Alonso Types are often thought as a way to capture mistakes. But C makes it obvious that it is also used to tailor the eventual binary code as tightly as possible.

@AmenZwa @dougmerritt @Jose_A_Alonso In Common lisp with bignums you see that without those indications about the types you are forced to oversize your data and algorithms.