[12thwonder]

back in the days, I had this infatuations with the idea of having everything checked at compile time by using type system. and I see many people following this kind of path with type system of Haskell, rust, and maybe typescript. granted, it feels good, at first.

I don't do that any more. simply because I'm very lazy and also in a lot of cases, those types that I wrote will be replaced by more dynamic representation (e.g. strings) at some point.

[ebingdom]

> I don't do that any more. simply because I'm very lazy

I'm lazy too, but that's exactly why I use static types. So that when I refactor code, I can let the type checker tell me all the places that need to be updated instead of trying to piece that together from test failures (and praying that the tests didn't miss anything).

[12thwonder]

yeah, but my point is that checking system that you had created will be thrown away at some point in my experience. so why bother writing types? that is my attitude at least at very early stage of a project.

later in a project where you know for sure something can be known at compile time, of course I love to check them at compile time.

[tikhonj]

My experience is that all my code gets thrown away or rewritten at some point. I've seen what code that doesn't get rewritten looks like; I'm intent on never inflicting anything like that on the world.

As far as types go, I've found that types actually help more during prototyping than later on. (At least for code I've written myself; types are great for helping me navigate other people's long-term codebases!)

Types give me a way to sketch out and iterate on an overall design without needing to implement anywhere near all the logic I'd need; then, when I start in on the logic, it naturally lays down on the skeleton the types provide. Compared to my experience with Python—where I still use some types!—I've found it easier to start and quickly try different designs in Haskell.

[philosopher1234]

>My experience is that all my code gets thrown away or rewritten at some point. I've seen what code that doesn't get rewritten looks like; I'm intent on never inflicting anything like that on the world.

I believe most code is old. You mostly notice code that changes.

[12thwonder]

good point. Yes, during prototype phase, rigid typing actually helps quite a bit. I still do that myself, simply because I don't have to "run" the program to see if I'm on the right path when I'm just sketching things out.

I guess what I wanted to say is that, in the long run, compile-time checks may become runtime checks, especially something like enum values where at the beginning, enums are fine choice but soon you will find yourself where you have to store that to a DB etc.

Problem is, moving from compile-time check to runtime check isn't that straightforward in a lot of cases.

[heavyset_go]

> so why bother writing types?

Types are the cheapest semantic documentation you can write, and your compiler/type checker can provide additional guarantees based on them.

Not only that, they're notes to future contributors/yourself about how a program works, so they/you don't have to reverse engineer code that was written a while ago in order to modify it with confidence.

[dmitriid]

> Types are the cheapest semantic documentation you can write

They are not.

Unfortunately, especially Haskell world seems to think they replace documentation, that's why so much of "documentation" for a lot of Haskell libs are just a dump of types with no explanation of what they mean, how they interact, what the functions using them do, or how they can be used.

> they're notes to future contributors/yourself about how a program works

They are not. Types do not describe how a program works.

> so they/you don't have to reverse engineer code that was written a while ago in order to modify it with confidence.

Yes, you will have to reverse engineer code that was written a while ago. Because types only describe, well, types. You code contains logic. And logic is the hardest part to understand.

Personal anecdote: worked on a system that was transitioning from original ad-hoc implementation to a better designed one. Some functions would accept a Person. Others would accept a Contact. Why? How to convert between the two? What are the differences? What was behind the decision? Why did `is_empty(new_contact())` returned `false`? And so on.

Thank god it had types, right? No need to reverse engineer.

[mixedCase]

Does your argument extend to automated tests? If not, why not?

I see types as mere tests. More robust, yet more limited in scope. FWIW it's much easier to see them that way once you introduce dependent types into the discussion, but it applies to the simplest type systems just as well.

[friendzis]

Types are tests. On top of being unit tests that are forcibly run, they are formal and apply everywhere a datum is used.

[12thwonder]

sort of. I don't write tests at early stages, do you?

I don't see types as serious tests and I don't think they are robust. let's say that some integer must be between 10 and 100, do you use type checks for this?

[ebingdom]

> I don't write tests at early stages, do you?

I definitely do. In my experience, it's much easier to adopt a discipline of testing (and static typing) early on than it is to try to retroactively add that to an existing system, which may or may not be written in a way that is even testable.

But I do appreciate that viewpoints can differ on this topic. Regarding types, I studied type theory academically, so types are natural to me and don't really add any extra cognitive work (and perhaps they eliminate some). So I might as well use and benefit from them if they basically cost me nothing. But for someone who thinks of static typing as just trying to make the compiler happy (perhaps because they don't really understand the type system or because the type system is not ergonomic), I can see why they might have a more pessimistic view of it.

[chriswarbo]

> let's say that some integer must be between 10 and 100, do you use type checks for this?

Yep. In particular, I would use:

- A "wrapper" type around an unsigned byte (we don't need negatives, or a whole machine word)

- A "newtype" feature, to replace the wrapper with a Byte after type-checking (Haskell calls this "newtype"; Scala calls this "opaque type aliases").

- A private/unexported/scoped constructor, to prevent arbitrary Byte values getting wrapped

- A "smart constructor" which checks the bounds of a given Byte, returning a 'Maybe MyBoundedIntType' or some other type-checked error mechanism (Scala's 'Try[MyBoundedIntType]' works well).

- Polymorphism/overloading to call that smart constructor of various numeric types (char, int, long, signed, unsigned, etc.)

In Scala that would look something like:

    opaque type MyBoundedIntType = Char

    object MyBoundedIntType {
      def apply(c: Char): Try[MyBoundedIntType] =
        if (c >= 10 && c <= 100)
          Success(c)
        else
          Failure(new IllegalArgumentException(s"Value ${c.toInt} outside range [10, 100]"))

      def apply(i: Int ): Try[MyBoundedIntType] = Try(i.toChar).flatMap(MyBoundedIntType(_))
      def apply(l: Long): Try[MyBoundedIntType] = Try(l.toChar).flatMap(MyBoundedIntType(_))
    }

In Haskell:

    module MyModule (MyBoundedIntType(), toByte, MakeBounded(..)) where

    newtype MyBoundedIntType = MBIT { toByte :: Word8 }

    class MakeBounded t where
      mkBounded :: t -> Either String MyBoundedIntType

    instance MakeBounded Word8 where
      mkBounded b | b >= 10 && b <= 100 = Right (MBIT b)
      mkBounded b | otherwise           = Left ("Value " ++ show b ++ " not in range [10, 100]")

    instance MakeBounded Int where
      mkBounded i = toWord8 i >>= mkBounded

    instance MakeBounded Integer where
      mkBounded i = toInt i >>= mkBounded

[Jtsummers]

You can with Ada. Though not many other languages.

[the_duke]

You can do it in most languages by just using a wrapper type with fallible constructors.

A lot more awkward than dependent types, but no popular language has those.

[mixedCase]

> let's say that some integer must be between 10 and 100, do you use type checks for this?

Yes. I explicitly mentioned dependent types for this reason.

This is also expressable in a more limited fashion in a language like TypeScript, although some may argue it also employs a form of dependent typing.

[quickthrower2]

If you have types it is easy to refactor the code. So the throwing away bit is actually easier!

[12thwonder]

Throwing away is easy but remember, you have to do the runtime check instead of compile time check, and that is not so easy in a lot of cases

[scns]

Lazyness as the motivation for creating machines/typecheckers to do the boring work.

[domnomnom]

Lazyness is actually a great feature of Haskell.

[scns]

SPJ begs to differ, he thinks it was a mistake.

[ourcat]

I'm still in the 'feels good' stage with meticulously modelling the types of data I use in Angular with Typescript.

Initially, I couldn't really see the point, but if anything I find it helps with catching errors and response expectations before build-time and also auto-completion/pseudo-documentation/hinting in VSCode.

Now, I love it.

[iamevn]

> in a lot of cases, those types that I wrote will be replaced by more dynamic representation (e.g. strings) at some point. I would love to see a type system that lets me subtype string, restrict the domain, and automatically (with some hints from the programmer) get functions on my type based on string functions the compiler can prove would result in my type.

I've only seen type systems that work like this on numbers, and usually only a very few integers at that.

[jkhdigital]

The formal notion of subtype seems to be getting some solid research attention; see e.g. https://drops.dagstuhl.de/opus/volltexte/2021/13888/pdf/LIPI...

Hopefully we see these ideas make their way into functional languages soon.

[dboreham]

That laziness isn't so smart when it comes time to write all the tests to check there won't be runtime exceptions due to treating values as the wrong type.

[scns]

In TypeScript you can define your discriminated union with strings, they call it literal types:

  type Foo = "bar" | "baz" | "qux"