Hacker News Reader

If I make an assembler in Lisp, compile it and ship it to you so that you can apply it to your assembly language programs, it wouldn't work so well for me to be diagnosing your assembly language problems in my compile time.

I'd prefer a language where I don't have to write a domain language from scratch and write a program that can enforce its rules at runtime. Rather I'd like to be able to express my domain code in the language itself, so that my users don't have to learn (and I don't have to create) a new language. That requires a consistent way of restricting things at compile time, which is very hard to retrofit - if I ever want to be able to enforce that programs don't do certain things, the language needs to not offer unrestricted access to those things.

If you express your domain code in the language yourself, users still have to learn and understand what you have done.

What you write in a language has its own de facto language, whether you capture its conventions in a notation or not.

Simply knowing the elements of the language in which that work is done isn't enough. Otherwise you could just memorize a language reference manual and call yourself a software engineer.

Or could just argue that since the program in any modern language is written in UTF-8, and the users know that already, they have nothing to learn.

There are still things to learn, and you may still need to adapt tools, but it's a lot easier to work with an "embedded" DSL than an "external" one. You still need to define the nouns and verbs of your domain, but you don't have to define a whole new grammar.

Lisp isn't any one thing, it's a language family. One could create a Lisp that is statically typed.

> Lisp isn't any one thing, it's a language family.

Which is rather the problem. Types, in particular, are only useful if everyone has them - optional add-on typing has been tried for many languages, but I've never known it be successful.

My point was that making generalizations about Lisp is like making generalizations about languages with C-like (perhaps more correct ALGOL-like) syntax. Most people wouldn't make a statement about Java and assert that it applied to C++, too. This is why saying that Lisp has no type system doesn't make much sense. There are many completely different languages that use s-expression notation, and they all have different feature sets, much like all the C-like languages.

Typed Racket <https://docs.racket-lang.org/ts-guide/> is pretty successful in the Racket community. It's also prompted some pessimistic papers about gradual sound typing, since it's hard to avoid a performance hit when imposing type safety on untyped code using contracts. On the other hand, that performance hit is in part typechecker/compiler implementation dependent and in part dependent on the granularity of the added typing (e.g. typing modules or functions vs typing subexpressions).

Typed Racket code often gains a speedup over untyped Racket, since sound typing allows the elision of contracts and other runtime overheads for safety. There is no penalty at all for invoking Typed Racket code from untyped code, either in terms of performance or in terms of what the untyped-language programmer needs to know.

Note that we've made big improvements in the performance of Typed Racket's generated contracts just since that paper was written, so many things are now better.

Common Lisp has an optional type system and many compilers have excellent type inference engines for optimization.

Common Lisp's type system isn't optional. The language is strongly typed. Type goes away (in a sense) when you add declarations. That is to say, if you tell Lisp that, say, some variable contains a fixnum, then (in code compiled with safety 0) it just believes your declaration, and it's up to you to ensure that it's not a lie (else the behavior is undefined). The type system isn't optional in any other sense.

It's optional for an implementation to provide static checks and optimizations based on type, which is different. "Static type" and "type" are not synonyms.

Common Lisp code is safe by default; you can't use an object of type X as if it were one of type Y.

Thanks for the explanation. Never really thought of it that way.

A spec that says adding a fixnum to a string produces a possibly-runtime error isn't a type system, it's just a particular instance behaviour. Types are by definition associated to terms in a language.

(That isn't to say that that kind of runtime behaviour isn't valuable or doesn't provide (some of) the same functionality as a type system. But it's not what the word "type" means).

> Types are by definition associated to terms in a language.

This is true, within a particular paradigm, which isn't the be-all and end-all of what "type" means in computer science.

All kinds of things are type. For instance, "JPEG file" or "alphanumeric character" are both type terms.

You don't get to dictate to everyone one narrow definition of a term that has an obviously broad applicability in numerous contexts.

If we are discussing Common Lisp, and you want to get properly pedantic about what "type" means, the way you can do that is to look up its definition in the ANSI CL glossary, which says:

"type n. 1. a set of objects, usually with common structure, behavior, or purpose."

Or you can use it in a broader way which is compatible with this concept.

If you insist that it means something else which is not compatible with the glossary definition, and you still want to talk about Lisp, then I'm afraid it's not productive; you are more interested in engaging in a conflict about word semantics: which "camp" gets to "own" the ideologically precious word, such as "type".

Usually how we can resolve that conflict is to split our vocabulary into different words. You can have "type", I don't need it; I will call it this other thing that the CL glossary refers to "genus". Now type can be the property of a syntactic term in a program, and genus refers to sets of objects which have something in common.

I'm mostly interested in genus systems, and type systems in their context (agreement between the type of a program term, and the genus of the run-time thing it operates on).

I don't think Lisp could even be said to have a genus system - to have a "system" for dealing with sets of objects implies having a way to talk about those sets, do set operations (intersection/union/product) etc.

But in any case, any genus-but-not-type system is irrelevant to my original point: that when writing an x86-64 assembler in lisp (as an embedded DSL), any enforcement of restrictions at compile time would have to be expressed as ad-hoc macros, because there is no (language-standard) type system in which to declare them.

Common Lisp in fact has type expressions with set operations.

  $ clisp -q
  [1]> (typep nil '(and symbol list))
  T
  [2]> (typep :foo '(and symbol list))
  NIL
  [3]> (typep '(1 2) '(and symbol list))
  NIL
  [4]> (typep '(1 2) '(or symbol list))
  T
  [5]> (typep 3 '(or symbol list)

I.e. I can in fact talk about sets of objects, in a formal way, with the Lisp system.

Ever seen ACL2 used for assembler verification?

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.

> 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 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".

  But [Lisp] won't enforce those things at compilation time
  in the type system, because it doesn't have one.

What Lisp implementation do you have in mind? I ask because Common Lisp has type system that includes compile-time type checking. For example, SBCL:

http://sbcl.org/manual/index.html#Handling-of-Types

My guess: some instructor's "one weekend lisp" that he or she had to study for a fraction of a semester.