5 ms·

It's an interesting question. It seems that developers are quite able to cope with weird type systems, moreover most of them don't even think about it or even c

It's an interesting question. It seems that developers are quite able to cope with weird type systems, moreover most of them don't even think about it or even care. A simple example of python2 that would make developers brought up on a healthy diet of haskell cringe is this: >>> for x in range(100): print type(1<<x) And yet, pythonistas seem to mind nor bother.

barrkel 9y ago
That example isn't a type problem. With a numeric tower and polymorphic arithmetic operators, it's to be expected in a dynamic type system. The type systems we're talking about in the OP article are about proofs that can be made over the code before it is ever executed. Dynamic type systems make few claims here so they don't cause issues. What does cause issues is asserting something to be proven true, but having compositions in the language that make the assertion false.
- toolslive 9y ago
  If it isn't the type problem, then what is the type signature of the shift operator?
  - nothrabannosir 9y ago
    No type expert, but: << :: Int -> Int | Long -> Int | Long << :: Long -> Int | Long -> Long ? If you can express a dynamic type system at all, then this seems intuitive?
    - toolslive 9y ago
      Yes, and it means (<<) is not closed over Int, which means that you will need to be able to compare instances of Int to instances of Long. Before you know it you're wondering what the result is of >>> -1j * -1j == -1 and >>> f(-1j * -1j) == f(-1) where f is some pure function. Some people think it's the road to perdition.
      - acjohnson55 9y ago
        Are you basically saying that programmers want intuitive interpretation of numeric literals, without having to suffix them to indicate their type? This strikes me as a situation where editing programs as plain text holds is back. Most languages have complex and error prone implicit type conversions between numeric types so to keep the text representation of the program looking clean. But if there were a way for the source to contain explicit type annotations on numbers without necessarily requiring the programmer to have to look at them or specify them in most cases, that seems like a much better situation. I think there are many such ways we are held back by plain text representation.
  - deleted 9y ago
    [deleted]
  - guipsp 9y ago
    Wouldn't << :: Integer -> Integer -> Integer be good enough?
  - kccqzy 9y ago
    Use union types. (Which are different from sum types, confusingly.)
    - uryga 9y ago
      Could you expand on the difference? I heard those two terms used interchangeably. edit: saw union/intersection types mentioned in another comment - I guess that's what you were referring to?
      - kccqzy 9y ago
        Yes. Sum types are essentially discriminated unions. Given a value of a sum type, it is possible to tell which alternative it is. This is commonly done through pattern matching. Union types are a bit like C's undiscriminated unions in that you cannot tell what the actual type is. This makes them significantly less useful, and thus very few functional languages have them. Essentially when you get back a union type of A | B, you can only perform actions that make sense on both of them. This essentially means functions with a type variable (parametrically polymorphic) in typical functional languages. If we additionally have subtyping (which ML-like languages don't) this can be more useful. Side note: things like the `typeof` operator in JavaScript is muddling the water a bit. But I'm talking about the theoretical perspective.
  - barrkel 9y ago
    Its static type is something like: dynamic -> dynamic -> dynamic That's because that's how dynamic type systems work, from a static typing perspective. They defer typing until runtime. Properties of the code proven before execution aren't usually very interesting.
- CodeArtisan 9y ago
  Isn't it known as weak typing? When a type system allows to break its soundness. https://en.wikipedia.org/wiki/Strong_and_weak_typing https://en.wikipedia.org/wiki/Strong_and_weak_typing
jwilk 9y ago
For those who don't know how Python 2 integers work and don't have a Python 2 interpreter at hand: type(1 << x) is int for small x, but long for large x. https://docs.python.org/2/library/stdtypes.html#numeric-types-int-float-long-complex https://docs.python.org/2/library/stdtypes.html#numeric-type... "Plain integers (also just called integers) are implemented using long in C, which gives them at least 32 bits of precision (sys.maxint is always set to the maximum plain integer value for the current platform, the minimum value is -sys.maxint - 1). Long integers have unlimited precision." The distinction between plain and long integers is gone in Python 3.
pjc50 9y ago
This kind of thing is why I'd favour two different types of numeric types: - "Number", which would be the generic DWIM arithmetic type. In your example both x and the literals would be Number. - Hyper-specified arithmetic types. Not just number of bits and signedness, but also overflow and trap behaviour. Less convenient to use - you can't easily add a "32bit signed wrap on overflow" to "16 bit unsigned saturate on overflow", but have the advantage that there is no unspecified behaviour. This also allows the user to make use of machine-provided saturate and overflow behaviour where present.
- mannykannot 9y ago
  I see where you are coming from, but C offers a cautionary tale: It offers more choices than most languages, and that creates a number of traps for the unwary. Maybe, however, that is only because it allows mixed-type expressions?
  - pjc50 9y ago
    Choice for the programmer, or choice for the implementer? Part of the problem of C is the amount of stuff with was left as a choice for the implementers on a particular platform and therefore could not be safely assumed to be universal. Forcing the programmer to enumerate what they actually want from their "fast machine integers" avoids that. C offers a fairly small choice of types to the programmer, certainly compared to one of the ML/Haskell style of language. It doesn't even have a proper "string" type! C doesn't exactly allow mixed-type expressions, it just performs a lot of type coercion and reinterpretation. Which is another one of those things that trades safety for convenience in so many languages. Type flexibility is responsible for most of the wtf type moments in Javascript: https://www.destroyallsoftware.com/talks/wat https://www.destroyallsoftware.com/talks/wat
- DoofusOfDeath 9y ago
  I've been thinking about something similar. My idea is to let programmers specify various constraints they care about on numeric-typed variables, including min/max value. Then the compiler has the freedom to choose any representation(s) it cares to that matches the constraints. For complicated constraints that are difficult to prove at static-compilation time, some checks might be deferred until linktime (when static call contexts are available) or runtime.

barrkel 9y ago

That example isn't a type problem. With a numeric tower and polymorphic arithmetic operators, it's to be expected in a dynamic type system. The type systems we're talking about in the OP article are about proofs that can be made over the code before it is ever executed. Dynamic type systems make few claims here so they don't cause issues. What does cause issues is asserting something to be proven true, but having compositions in the language that make the assertion false.

toolslive 9y ago
If it isn't the type problem, then what is the type signature of the shift operator?
- nothrabannosir 9y ago
  No type expert, but: << :: Int -> Int | Long -> Int | Long << :: Long -> Int | Long -> Long ? If you can express a dynamic type system at all, then this seems intuitive?
  - toolslive 9y ago
    Yes, and it means (<<) is not closed over Int, which means that you will need to be able to compare instances of Int to instances of Long. Before you know it you're wondering what the result is of >>> -1j * -1j == -1 and >>> f(-1j * -1j) == f(-1) where f is some pure function. Some people think it's the road to perdition.
    - acjohnson55 9y ago
      Are you basically saying that programmers want intuitive interpretation of numeric literals, without having to suffix them to indicate their type? This strikes me as a situation where editing programs as plain text holds is back. Most languages have complex and error prone implicit type conversions between numeric types so to keep the text representation of the program looking clean. But if there were a way for the source to contain explicit type annotations on numbers without necessarily requiring the programmer to have to look at them or specify them in most cases, that seems like a much better situation. I think there are many such ways we are held back by plain text representation.
- deleted 9y ago
  [deleted]
- guipsp 9y ago
  Wouldn't << :: Integer -> Integer -> Integer be good enough?
- kccqzy 9y ago
  Use union types. (Which are different from sum types, confusingly.)
  - uryga 9y ago
    Could you expand on the difference? I heard those two terms used interchangeably. edit: saw union/intersection types mentioned in another comment - I guess that's what you were referring to?
    - kccqzy 9y ago
      Yes. Sum types are essentially discriminated unions. Given a value of a sum type, it is possible to tell which alternative it is. This is commonly done through pattern matching. Union types are a bit like C's undiscriminated unions in that you cannot tell what the actual type is. This makes them significantly less useful, and thus very few functional languages have them. Essentially when you get back a union type of A | B, you can only perform actions that make sense on both of them. This essentially means functions with a type variable (parametrically polymorphic) in typical functional languages. If we additionally have subtyping (which ML-like languages don't) this can be more useful. Side note: things like the `typeof` operator in JavaScript is muddling the water a bit. But I'm talking about the theoretical perspective.
- barrkel 9y ago
  Its static type is something like: dynamic -> dynamic -> dynamic That's because that's how dynamic type systems work, from a static typing perspective. They defer typing until runtime. Properties of the code proven before execution aren't usually very interesting.
CodeArtisan 9y ago
Isn't it known as weak typing? When a type system allows to break its soundness. https://en.wikipedia.org/wiki/Strong_and_weak_typing https://en.wikipedia.org/wiki/Strong_and_weak_typing

jwilk 9y ago

For those who don't know how Python 2 integers work and don't have a Python 2 interpreter at hand: type(1 << x) is int for small x, but long for large x. https://docs.python.org/2/library/stdtypes.html#numeric-types-int-float-long-complex https://docs.python.org/2/library/stdtypes.html#numeric-type... "Plain integers (also just called integers) are implemented using long in C, which gives them at least 32 bits of precision (sys.maxint is always set to the maximum plain integer value for the current platform, the minimum value is -sys.maxint - 1). Long integers have unlimited precision." The distinction between plain and long integers is gone in Python 3.

pjc50 9y ago

This kind of thing is why I'd favour two different types of numeric types: - "Number", which would be the generic DWIM arithmetic type. In your example both x and the literals would be Number. - Hyper-specified arithmetic types. Not just number of bits and signedness, but also overflow and trap behaviour. Less convenient to use - you can't easily add a "32bit signed wrap on overflow" to "16 bit unsigned saturate on overflow", but have the advantage that there is no unspecified behaviour. This also allows the user to make use of machine-provided saturate and overflow behaviour where present.

mannykannot 9y ago
I see where you are coming from, but C offers a cautionary tale: It offers more choices than most languages, and that creates a number of traps for the unwary. Maybe, however, that is only because it allows mixed-type expressions?
- pjc50 9y ago
  Choice for the programmer, or choice for the implementer? Part of the problem of C is the amount of stuff with was left as a choice for the implementers on a particular platform and therefore could not be safely assumed to be universal. Forcing the programmer to enumerate what they actually want from their "fast machine integers" avoids that. C offers a fairly small choice of types to the programmer, certainly compared to one of the ML/Haskell style of language. It doesn't even have a proper "string" type! C doesn't exactly allow mixed-type expressions, it just performs a lot of type coercion and reinterpretation. Which is another one of those things that trades safety for convenience in so many languages. Type flexibility is responsible for most of the wtf type moments in Javascript: https://www.destroyallsoftware.com/talks/wat https://www.destroyallsoftware.com/talks/wat
DoofusOfDeath 9y ago
I've been thinking about something similar. My idea is to let programmers specify various constraints they care about on numeric-typed variables, including min/max value. Then the compiler has the freedom to choose any representation(s) it cares to that matches the constraints. For complicated constraints that are difficult to prove at static-compilation time, some checks might be deferred until linktime (when static call contexts are available) or runtime.