News for hackers. Stuff that matters.
Re:An Introduction to Type Level Programming in Haskell by 12thwonder on Thursday September 09, 2021 @06:51PM (#28475617)
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.

Re:An Introduction to Type Level Programming in Haskell by ebingdom on Thursday September 09, 2021 @06:55PM (#28475651)
> 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).

Re:An Introduction to Type Level Programming in Haskell by 12thwonder on Thursday September 09, 2021 @07:00PM (#28475702)
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.

Re:An Introduction to Type Level Programming in Haskell by tikhonj on Thursday September 09, 2021 @10:30PM (#28477129)
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.

Re:An Introduction to Type Level Programming in Haskell by philosopher1234 on Friday September 10, 2021 @01:22AM (#28478070)
>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.

Re:An Introduction to Type Level Programming in Haskell by 12thwonder on Friday September 10, 2021 @12:01AM (#28477666)
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.

Re:An Introduction to Type Level Programming in Haskell by heavyset_go on Friday September 10, 2021 @01:10PM (#28484456)
> 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.

Re:An Introduction to Type Level Programming in Haskell by dmitriid on Saturday September 11, 2021 @02:24AM (#28489815)
> 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.

Re:An Introduction to Type Level Programming in Haskell by mixedCase on Thursday September 09, 2021 @11:53PM (#28477627)
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.

Re:An Introduction to Type Level Programming in Haskell by friendzis on Friday September 10, 2021 @02:19AM (#28478368)
Types are tests. On top of being unit tests that are forcibly run, they are formal and apply everywhere a datum is used.
Re:An Introduction to Type Level Programming in Haskell by 12thwonder on Friday September 10, 2021 @12:08AM (#28477717)
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?

Re:An Introduction to Type Level Programming in Haskell by ebingdom on Friday September 10, 2021 @02:22AM (#28478387)
> 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.

Re:An Introduction to Type Level Programming in Haskell by chriswarbo on Monday September 13, 2021 @11:03AM (#28512371)
> 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
Re:An Introduction to Type Level Programming in Haskell by Jtsummers on Friday September 10, 2021 @12:48AM (#28477919)
You can with Ada. Though not many other languages.
Re:An Introduction to Type Level Programming in Haskell by the_duke on Friday September 10, 2021 @01:31AM (#28478130)
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.

Re:An Introduction to Type Level Programming in Haskell by mixedCase on Friday September 10, 2021 @09:46AM (#28481487)
> 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.

Re:An Introduction to Type Level Programming in Haskell by quickthrower2 on Friday September 10, 2021 @12:47AM (#28477912)
If you have types it is easy to refactor the code. So the throwing away bit is actually easier!
Re:An Introduction to Type Level Programming in Haskell by 12thwonder on Friday September 10, 2021 @01:26AM (#28478097)
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
Re:An Introduction to Type Level Programming in Haskell by scns on Friday September 10, 2021 @03:18AM (#28478650)
Lazyness as the motivation for creating machines/typecheckers to do the boring work.
Re:An Introduction to Type Level Programming in Haskell by domnomnom on Friday September 10, 2021 @11:22AM (#28482825)
Lazyness is actually a great feature of Haskell.
Re:An Introduction to Type Level Programming in Haskell by scns on Saturday September 11, 2021 @06:57AM (#28490919)
SPJ begs to differ, he thinks it was a mistake.
Re:An Introduction to Type Level Programming in Haskell by ourcat on Thursday September 09, 2021 @07:30PM (#28475962)
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.

Re:An Introduction to Type Level Programming in Haskell by iamevn on Thursday September 09, 2021 @07:10PM (#28475797)
> 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.

Re:An Introduction to Type Level Programming in Haskell by jkhdigital on Thursday September 09, 2021 @09:26PM (#28476757)
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.

Re:An Introduction to Type Level Programming in Haskell by dboreham on Thursday September 09, 2021 @10:41PM (#28477185)
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.
Re:An Introduction to Type Level Programming in Haskell by scns on Friday September 10, 2021 @04:15AM (#28478967)
In TypeScript you can define your discriminated union with strings, they call it literal types:

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