Another commenter already said that Common Lisp indeed does have a type system. It's possible to circumvent, but that's Lisp for you.
You can very easily write an assembler in Haskell that doesn't verify any of that stuff statically. Learning to do advanced kinds of static verification with Haskell's type system is actually rather difficult, and usually requires language extensions.
Using a macro that checks those things seems like it could be a very pragmatic way to provide safety. It might also let you verify properties that would be hard to figure out how to verify using only Haskell-style type checking.
Indeed, Haskell programmers often use QuickCheck to do ad-hoc verification of type class laws, for example, since they can't be proven in the type system.
You can write Lisp that is de facto statically typed, and good compilers take advantage of it. If we write (cons a b), that piece of program text has a type, which is a cons. Given (let ((c (cons a b))) ... (car c) ...) the Lisp compiler can generate efficient code to access c, without a run-time type check that c is a cons, based on c inheriting the type from the cons expression, and not being subject to any assignment in its scope. If we regard it as a parametrized type, not knowing what a and b is, it is the expression "for all types x, for all types y, the type of (cons x y) is: cons cell of x and y".
> Learning to do advanced kinds of static verification with Haskell's type system is actually rather difficult
Perhaps. But it benefits greatly from being a consistent way of doing things: everyone does their static verification the same way, because the language supports exactly one way of doing it.
> and usually requires language extensions.
Sometimes. But again at least those extensions are relatively standardized, rather than completely ad-hoc as a macro can be.
> Indeed, Haskell programmers often use QuickCheck to do ad-hoc verification of type class laws, for example, since they can't be proven in the type system.
Yeah, that's one of the reasons I'm excited about Idris. But even in your example, QuickCheck is again a standardized way of doing this.
Well, all you need to do in a macro to provide error checking is to assert or raise a condition when something is wrong. That's pretty standard.
In Haskell land, you can do wonderful things like Servant, the statically verified API server—but that kind of code is very advanced, and written by a shadowy cabal of type level wizards. I think there is less of a standardized way of doing this stuff than one might expect.
I'm not really sure what you mean by "standardized." Common Lisp is an actual ANSI standard... But you seem to be referring to the existence of common practices.
I'm not convinced that the problem you describe is actually a problem, and I'm not convinced that Haskell or Idris will end up being more successful in the mainstream than Lisp.
(I'm a huge fan of Haskell, Agda, and static/dependent typing, for the record.)
> Well, all you need to do in a macro to provide error checking is to assert or raise a condition when something is wrong. That's pretty standard.
Sure, but the conditions that lead you to do that can be arbitrary Turing-complete code. IIRC in unextended Haskell what you can do at type-level is more restricted; certainly you're guided towards a particular way of structuring your constraints. That in turn makes it more practical for other tools to support your constrained sublanguage.
I think the future of programming lies in constrained (BWIM non-Turing-complete) languages and provably correct code. I guess we'll find out.
I didn't respond to that because I don't debate with thinkers who equate "type" with "static type". Not that I don't want to, but I haven't historically found it possible (at least in a productive way).
You can very easily write an assembler in Haskell that doesn't verify any of that stuff statically. Learning to do advanced kinds of static verification with Haskell's type system is actually rather difficult, and usually requires language extensions.
Using a macro that checks those things seems like it could be a very pragmatic way to provide safety. It might also let you verify properties that would be hard to figure out how to verify using only Haskell-style type checking.
Indeed, Haskell programmers often use QuickCheck to do ad-hoc verification of type class laws, for example, since they can't be proven in the type system.