[currymj]

There’s the technical aspects of the fact that every language has to have some notion of “type”. And seemingly interpreted languages might be JIT-compiled etc. This is of interest if you care about the implementation of languages.

Then there’s the opinions that users of languages with more elaborate, expressive type systems have, like how some people really enjoy Haskell or Elm because they feel that the type system helps them express their ideas clearly, avoid errors, and aids refactoring and maintenance.

If you’re worried about this one, don’t I guess? If you can use dynamic languages to achieve your goals, and you like them, then that’s fine! There are plenty of languages you can play with if you want to get a feel for programming with types. Even Java 8 and C++11 are decent at this point (I’m sure a Haskell programmer is fuming right now).

Then there’s like, a few thousand people in the world who have well-informed opinions on research into the theory of programming languages, the Curry-Howard correspondence between types and proofs. Also a lot of Hacker News posters who have heard these words. Some of them pretend like they know what they’re talking about.

[acchow]

> There’s the technical aspects of the fact that every language has to have some notion of “type”

This isn't true. There are no types in lisp or untyped lambda calculus.

[lispm]

Common Lisp has a primitive type system. Some implementations use that for compile-time type checks:

An integer type I1 from 0 to 65535.

    (deftype i1 (&optional (min 0) (max 65535))
      `(integer ,min ,max))

The function foo gets an integer and returns an I1:

    (declaim (ftype (function (integer) i1)
                    foo))

    (defun foo (i)
      (mod i 65536))

    (defun test ()
      (foo 6712312)       ; okay
      (foo 311212.2))     ; wrong call

Let's compile it in SBCL, a Common Lisp compiler:

    ; compiling file "/private/tmp/test.lisp" (written 08 JUL 2017 11:10:09 AM):
    ; compiling (DEFTYPE I1 ...)
    ; compiling (DECLAIM (FTYPE # ...))
    ; compiling (DEFUN FOO ...)
    ; compiling (DEFUN TEST ...)
    ; file: /private/tmp/test.lisp
    ; in: DEFUN TEST
    ;     (FOO 311212.2)
    ; 
    ; note: deleting unreachable code
    ; 
    ; caught WARNING:
    ;   Constant 311212.2 conflicts with its asserted type INTEGER.
    ;   See also:
    ;     The SBCL Manual, Node "Handling of Types"
    ; 
    ; compilation unit finished
    ;   caught 1 WARNING condition
    ;   printed 1 note

As you can see that it detects the type error.

The type system has been defined for Common Lisp with its first version in 1984. It had been used to allow the compiler to generate optimized code or to do more precise runtime checks. Early on in the mod 80s the CMUCL compiler then added the idea to use these type declarations as type assertions and to check those at compile time.

[naasking]

Actually, there's one type.

[acchow]

If you're going to shove the system into a typed model, then sure there is one type. But then you've kind of missed the point...

[naasking]

If you're going to answer the question of whether a language has types, then you're already trying to see how it can be shoved into types. It's presupposed by the question itself.

You literally have to count the types by analyzing the grammar. So for the lambda calculus, you have lambda=1, halt. So does a single type mean no types or literally one type?

What's the advantage of thinking that 1 type actually equals 0 types? I don't see any, so in my mind, all languages are unityped or have a richer type structure. Whether a richer type structure is desirable is a separate question.