[pclowes]

I like this. Very much falls into the "make bad state unrepresentable".

The issues I see with this approach is when developers stop at this first level of type implementation. Everything is a type and nothing works well together, tons of types seem to be subtle permutations of each other, things get hard to reason about etc.

In systems like that I would actually rather be writing a weakly typed dynamic language like JS or a strongly typed dynamic language like Elixir. However, if the developers continue pushing logic into type controlled flows, eg:move conditional logic into union types with pattern matching, leverage delegation etc. the experience becomes pleasant again. Just as an example (probably not the actual best solution) the "DewPoint" function could just take either type and just work.

[josephg]

Yep. For this reason, I wish more languages supported bound integers. Eg, rather than saying x: u32, I want to be able to use the type system to constrain x to the range of [0, 10).

This would allow for some nice properties. It would also enable a bunch of small optimisations in our languages that we can't have today. Eg, I could make an integer that must fall within my array bounds. Then I don't need to do bounds checking when I index into my array. It would also allow a lot more peephole optimisations to be made with Option.

Weirdly, rust already kinda supports this within a function thanks to LLVM magic. But it doesn't support it for variables passed between functions.

[mcculley]

Ada has this ability to define ranges for subtypes. I wish language designers would look at Ada more often.

[nikeee]

I proposed a primitive for this in TypeScript a couple of years ago [1].

While I'm not entirely convinced myself whether it is worth the effort, it offers the ability to express "a number greater than 0". Using type narrowing and intersection types, open/closed intervals emerge naturally from that. Just check `if (a > 0 && a < 1)` and its type becomes `(>0)&(<1)`, so the interval (0, 1).

I also built a simple playground that has a PoC implementation: https://nikeee.github.io/typescript-intervals/

[1]: https://github.com/microsoft/TypeScript/issues/43505

[archargelod]

Nim[0] supports subrange types:

  type
    Foo = range[1 .. 10]
    Bar = range[0.0 .. 1.0] # float works too
  
  var f:Foo = 42       # Error: cannot convert 42 to Foo = range 1..10(int)
  var p = Positive 22  # Positive and Natural types are pre-defined

[0] - https://nim-lang.org/docs/manual.html#types-subrange-types

[ninetyninenine]

This can be done in typescript. It’s not super well known because of typescripts association with frontend and JavaScript. But typescript is a language with one of the most powerful type systems ever.

Among the popular languages like golang, rust or python typescript has the most powerful type system.

How about a type with a number constrained between 0 and 10? You can already do this in typescript.

    type onetonine = 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9

You can even programmatically define functions at the type level. So you can create a function that outputs a type between 0 to N.

    type Range<N extends number, A extends number[] = []> =
  A['length'] extends N ? A[number] : Range<N, [...A, A['length']]>;

The issue here is that it’s a bit awkward you want these types to compose right? If I add two constrained numbers say one with max value of 3 and another with max value of two the result should be max value of 5. Typescript doesn’t support this by default with default addition. But you can create a function that does this.

   // Build a tuple of length L
   type BuildTuple<L extends number, T extends unknown[] = []> =
  T['length'] extends L ? T : BuildTuple<L, [...T, unknown]>;

   // Add two numbers by concatenating their tuples
   type Add<A extends number, B extends number> =
  [...BuildTuple<A>, ...BuildTuple<B>]['length'];

   // Create a union: 0 | 1 | 2 | ... | N-1
   type Range<N extends number, A extends number[] = []> =
  A['length'] extends N ? A[number] : Range<N, [...A, A['length']]>;

   function addRanges<
     A extends number,
     B extends number
   >(
     a: Range<A>,
     b: Range<B>
   ): Range<Add<A, B>> {
     return (a + b) as Range<Add<A, B>>;
   }

The issue is to create these functions you have to use tuples to do addition at the type level and you need to use recursion as well. Typescript recursion stops at 100 so there’s limits.

Additionally it’s not intrinsic to the type system. Like you need peanno numbers built into the number system and built in by default into the entire language for this to work perfectly. That means the code in the function is not type checked but if you assume that code is correct then this function type checks when composed with other primitives of your program.

[steveklabnik]

In my understanding Rust may gain this feature via “pattern types.”

[librasteve]

in raku, that’s spelled

  subset OneToTen of Int where 1..10:

[fny]

But wouldn't that also require code execution? For example even though the compiler already knows the size of an array and could do a bounds check on direct assigment (arr[1] = 1) in some wild nested loop you could exceed the bounds that the compiler can't see.

Otherwise you could have type level asserts more generally. Why stop at a range check when you could check a regex too? This makes the difficulty more clear.

For the simplest range case (pure assignment) you could just use an enum?

[someone_19]

You can do this quite easily in Rust. But you have to overload operators to make your type make sense. That's also possible, you just need to define what type you get after dividing your type by a regular number and vice versa a regular number by your type. Or what should happen if when adding two of your types the sum is higher than the maximum value. This is quite verbose. Which can be done with generics or macros.

[vmchale]

ATS does this. Works quite well since multiplication by known factors and addition of type variables + inequalities is decidable (and in fact quadratic).

[bakul]

Pascal had range types such as 0..9 (as of 1970). Subranges could also be defined for any scalar type. Further, array index types were such ranges.

[scottgg]

The generic magic for this is called “dependant types” I believe - generics that can take values as well as types as parameters. Idris supports these

[0_gravitas]

Clojure does bounded values/regex natively in Clojure Spec, and also the Malli library from Metosin

[arrowsmith]

FYI: Ruby is strongly typed, not loosely.

    > 1 + "1"
    (irb):1:in 'Integer#+': String can't be coerced into Integer (TypeError)
     from (irb):1:in '<main>'
     from <internal:kernel>:168:in 'Kernel#loop'
     from /Users/george/.rvm/rubies/ruby-3.4.2/lib/ruby/gems/3.4.0/gems/irb-1.14.3/exe/irb:9:in '<top (required)>'
     from /Users/george/.rvm/rubies/ruby-3.4.2/bin/irb:25:in 'Kernel#load'
     from /Users/george/.rvm/rubies/ruby-3.4.2/bin/irb:25:in '<main>'

[kitten_mittens_]

There seem to be two competing nomenclatures around strong/weak typing where people mean static/dynamic instead.

[pclowes]

Oops, I meant weakly typed as in JS or strongly typed as in Ruby. But decided to switch the Ruby example to Elixir and messed up the sentence

[js2]

Good luck with this fight. I've had it on HN most recently 7 months ago, but about Python:

https://news.ycombinator.com/item?id=42367644

A month before that:

https://news.ycombinator.com/item?id=41630705

I've given up since then.

[johnfn]

    irb(main):001:0> a = 1
    => 1
    irb(main):002:0> a = '1'
    => "1"

It doesn't seem that strong to me.

[jevndev]

The “Stop at first level of type implementation” is where I see codebases fail at this. The example of “I’ll wrap this int as a struct and call it a UUID” is a really good start and pretty much always start there, but inevitably someone will circumvent the safety. They’ll see a function that takes a UUID and they have an int; so they blindly wrap their int in UUID and move on. There’s nothing stopping that UUID from not being actually universally unique so suddenly code which relies on that assumption breaks.

This is where the concept of “Correct by construction” comes in. If any of your code has a precondition that a UUID is actually unique then it should be as hard as possible to make one that isn’t. Be it by constructors throwing exceptions, inits returning Err or whatever the idiom is in your language of choice, the only way someone should be able to get a UUID without that invariant being proven is if they really *really* know what they’re doing.

(Sub UUID and the uniqueness invariant for whatever type/invariants you want, it still holds)

[munificent]

> This is where the concept of “Correct by construction” comes in.

This is one of the basic features of object-oriented programming that a lot of people tend to overlook these days in their repetitive rants about how horrible OOP is.

One of the key things OO gives you is constructors. You can't get an instance of a class without having gone through a constructor that the class itself defines. That gives you a way to bundle up some data and wrap it in a layer of validation that can't be circumvented. If you have an instance of Foo, you have a firm guarantee that the author of Foo was able to ensure the Foo you have is a meaningful one.

Of course, writing good constructors is hard because data validation is hard. And there are plenty of classes out there with shitty constructors that let you get your hands on broken objects.

But the language itself gives you direct mechanism to do a good job here if you care to take advantage of it.

Functional languages can do this too, of course, using some combination of abstract types, the module system, and factory functions as convention. But it's a pattern in those languages where it's a language feature in OO languages. (And as any functional programmer will happily tell you, a design pattern is just a sign of a missing language feature.)

[MoreQARespect]

I've recently been following red-green-refactor but instead of with a failing test, I tighten the screws on the type system to make a production-reported bug cause the type checker to fail before making it green by fixing the bug.

I still follow TDD-with-a-test for all new features, all edge cases and all bugs that I can't trigger failure by changing the type system for.

However, red-green-refactor-with-the-type-system is usually quick and can be used to provide hard guarantees against entire classes of bug.

[pclowes]

I like this approach, there are often calls for increased testing on big systems and what they really mean is increased rigor. Don't waste time testing what you can move into the compiler.

It is always great when something is so elegantly typed that I struggle to think of how to write a failing test.

What drives me nuts is when there are testing left around basically testing the compiler that never were “red” then “greened” makes me wonder if there is some subtle edge case I am missing.

[eyelidlessness]

I found myself following a similar trajectory, without realizing that’s what I was doing. For a while it felt like I was bypassing the discipline of TDD that I’d previously found really valuable, until I realized that I was getting a lot of the test-first benefits before writing or running any code at all.

Now I just think of types as the test suite’s first line of defense. Other commenters who mention the power of types for documentation and refactoring aren’t wrong, but I think that’s because types are tests… and good tests, at almost any level, enable those same powers.

[atoav]

As you mentioned correctly: if you go for strongly typed types in a library you should go all the way. And that means your strong type should provide clear functions for its conversion to certain other types. Some of which you nearly always need like conversion to a string or representation as a float/int.

The danger of that is of course that you provide a ladder over the wall you just built and instead of

   temperature_in_f = temperature_in_c.to_fahrenheit()

They now go the shortcut route via numeric representation and may forget the conversion factor. In that case I'd argue it is best to always represent temperature as one unit (Kelvin or Celsius, depending on the math you need to do with it) and then just add a .display(Unit:: Fahrenheit) method that returns a string. If you really want to convert to TemperatureF for a calculation you would have to use a dedicated method that converts from one type to another.

The unit thing is of course an example, for this finished libraries like pythons pint (https://pint.readthedocs.io/en/stable/) exist.

One thing to consider as well is that you can mix up absolute values ("it is 28°C outside") and temperature deltas ("this is 2°C warmer than the last measurement"). If you're controlling high energy heaters mixing those up can ruin your day, which is why you could use different types for absolutes and deltas (or a flag within one type). Datetime libraries often do that as well (in python for example you have datetime for absolute and timedelta for relative time)

[kazinator]

Also known as "make bad state unexperimentable".

[balamatom]

Hahaha. Nice coinage! Funny they set out to do the former then we have to deal with how they've achieved the later

[tossandthrow]

This can usually be alleviated by structural types instead of nominal types.

You can always enforce nominal types if you really need it.

[reactordev]

Union types!! If everything’s a type and nothing works together, start wrapping them in interfaces and define an über type that unions everything everywhere all at once.

Welcome to typescript. Where generics are at the heart of our generic generics that throw generics of some generic generic geriatric generic that Bob wrote 8 years ago.

Because they can’t reason with the architecture they built, they throw it at the type system to keep them in line. It works most of the time. Rust’s is beautiful at barking at you that you’re wrong. Ultimately it’s us failing to design flexibility amongst ever increasing complexity.

Remember when “Components” where “Controls” and you only had like a dozen of them?

Remember when a NN was only a few hundred thousand parameters?

As complexity increases with computing power, so must our understanding of it in our mental model.

However you need to keep that mental model in check, use it. If it’s typing, do it. If it’s rigorous testing, write your tests. If it’s simulation, run it my friend. Ultimately, we all want better quality software that doesn’t break in unexpected ways.

[valenterry]

union types are great. But alone they are not sufficient for many cases. For example, try to define a datastructure that captures a classical evaluation-tree.

You might go with:

    type Expression = Value | Plus | Minus | Multiply | Divide;
    
    interface Value    { type: "value"; value: number; }
    interface Plus     { type: "plus"; left: Expression; right: Expression; }
    interface Minus    { type: "minus"; left: Expression; right: Expression; }
    interface Multiply { type: "multiply"; left: Expression; right: Expression; }
    interface Divide   { type: "divide"; left: Expression; right: Expression; }

And so on.

That looks nice, but when you try to pattern match on it and have your pattern matching return the types that are associated with the specific operation, it won't work. The reason is that Typescript does not natively support GADTs. Libs like ts-pattern use some tricks to get closish at least.

And while this might not be very important for most application developers, it is very important for library authors, especially to make libraries interoperable with each other and extend them safely and typesafe.