4 ms·

I suppose it depends on what you mean by "static types" since you can optionally specify types in Common Lisp. SBCL even does precise type checking[1]: "If a v

I suppose it depends on what you mean by "static types" since you can optionally specify types in Common Lisp. SBCL even does precise type checking[1]: "If a variable is declared to be (integer 3 17) then its value must always be an integer between 3 and 17. If multiple type declarations apply to a single variable, then all the declarations must be correct; it is as though all the types were intersected producing a single and type specifier." [1] http://www.sbcl.org/manual/#Handling-of-Types http://www.sbcl.org/manual/#Handling-of-Types

maydup-nem 5y ago
I would like to add that optimizations may also be performed in addition to type-checking (type-checking, by the way, depends on safety optimization level). What's also handy is that you can specify the optimization levels (space, safety, speed, debug) per function or per file (or in a `locally' block). Function return types may also be specified, with serapeum's ->, it may be as simple as (-> f (fixnum fixnum) boolean) for instance, right above the function. Classes and structs let you specify types for slots. Expressions may be typed with `the' special operator aka (the fixnum (first list)). PS CL has gradual typing.
christophilus 5y ago
Dang. I didn’t know sbcl did this. I’ve never used it, but now I want to try. Thanks!
bitwize 5y ago
Type systems at least as rich as Hindley-Milner are pretty much table stakes in 2022. Common Lisp's type system is not as rich as Hindley-Milner. I believe it doesn't even support user-defined parametric types (so it's kind of like pre-generics Go in that regard). It lets you type function args, but it doesn't incorporate the args' types into the function type. So no, Common Lisp's type system, even with static type checking enabled, is not adequate for software engineering in the present day. Coalton, however, solves many of these problems.
- deleted 5y ago
  [deleted]
- KerrAvon 5y ago
  What languages in common use in 2022 support a Hindley-Milner type system? This sounds a bit like pointless academic gatekeeping…
  - bitwize 5y ago
    Basically, any statically typed language with parametric polymorphism, so Ada, C++, Java, C#, Rust, TypeScript, Python with static-typing support, post-Delphi Pascal, and recently Go all qualify.
    - reikonomusha 5y ago
      Parametric polymorphism != Hindley-Milner, not even basically. H-M is a construction for describing and ascertaining types of terms in a lambda calculus. Many of those languages don't even typically idiomatically achieve polymorphism through generic types (though of course it's possible), but instead from subtype and ad hoc polymorphism. I don't think it's accurate to imply their designs orbit H-M. I don't want to belabor on technicalities. Your original point was about "table stakes" for type systems in order to be relevant for modern-day software engineering. While I agree a language that attempts to incorporate fashionable computational constructs (like variable binding and lambda terms) ought to derive its type system from something H-M-esque—if only because it's so well understood—it's certainly not a requirement for the language to be taken seriously, and it's certainly not without significant peril in the presence of mutation constructions. I honestly think C, vanilla Common Lisp, and pre-generic Go are sufficiently disparate examples of that.
      - dbmacqueen 5y ago
        Type inference is hinted at in a 1934 paper by Haskell Curry on "functionality" (i.e. types) for combinatory logic. Max Newman (Turning mentor and leader of the Colossus project at Bletchley Park) published a paper in 1943 giving the first algorithm for type inference for the lambda calculus that I know of.

maydup-nem 5y ago

I would like to add that optimizations may also be performed in addition to type-checking (type-checking, by the way, depends on safety optimization level). What's also handy is that you can specify the optimization levels (space, safety, speed, debug) per function or per file (or in a `locally' block). Function return types may also be specified, with serapeum's ->, it may be as simple as (-> f (fixnum fixnum) boolean) for instance, right above the function. Classes and structs let you specify types for slots. Expressions may be typed with `the' special operator aka (the fixnum (first list)). PS CL has gradual typing.

christophilus 5y ago

Dang. I didn’t know sbcl did this. I’ve never used it, but now I want to try. Thanks!

bitwize 5y ago

Type systems at least as rich as Hindley-Milner are pretty much table stakes in 2022. Common Lisp's type system is not as rich as Hindley-Milner. I believe it doesn't even support user-defined parametric types (so it's kind of like pre-generics Go in that regard). It lets you type function args, but it doesn't incorporate the args' types into the function type. So no, Common Lisp's type system, even with static type checking enabled, is not adequate for software engineering in the present day. Coalton, however, solves many of these problems.

deleted 5y ago
[deleted]
KerrAvon 5y ago
What languages in common use in 2022 support a Hindley-Milner type system? This sounds a bit like pointless academic gatekeeping…
- bitwize 5y ago
  Basically, any statically typed language with parametric polymorphism, so Ada, C++, Java, C#, Rust, TypeScript, Python with static-typing support, post-Delphi Pascal, and recently Go all qualify.
  - reikonomusha 5y ago
    Parametric polymorphism != Hindley-Milner, not even basically. H-M is a construction for describing and ascertaining types of terms in a lambda calculus. Many of those languages don't even typically idiomatically achieve polymorphism through generic types (though of course it's possible), but instead from subtype and ad hoc polymorphism. I don't think it's accurate to imply their designs orbit H-M. I don't want to belabor on technicalities. Your original point was about "table stakes" for type systems in order to be relevant for modern-day software engineering. While I agree a language that attempts to incorporate fashionable computational constructs (like variable binding and lambda terms) ought to derive its type system from something H-M-esque—if only because it's so well understood—it's certainly not a requirement for the language to be taken seriously, and it's certainly not without significant peril in the presence of mutation constructions. I honestly think C, vanilla Common Lisp, and pre-generic Go are sufficiently disparate examples of that.
    - dbmacqueen 5y ago
      Type inference is hinted at in a 1934 paper by Haskell Curry on "functionality" (i.e. types) for combinatory logic. Max Newman (Turning mentor and leader of the Colossus project at Bletchley Park) published a paper in 1943 giving the first algorithm for type inference for the lambda calculus that I know of.