Hacker News Reader

Comment by toolslive | Hacker News Reader

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.

View on HN

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

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.

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?

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

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.

This is the approach that Kotlin takes (albeit with boxed primitive types). Float, Integer, Long - all are subtypes of Number.

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.

If it isn't the type problem, then what is the type signature of the shift operator?

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?

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.

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.

Wouldn't

   << :: Integer -> Integer -> Integer

be good enough?

Use union types. (Which are different from sum types, confusingly.)

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?

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.

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.

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

Reply on news.ycombinator.com