Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Use Your Type System

dzombak.com

Post reply on HN
Print view View original

331–340 of 357 posts

Re: Use Your Type System

#331

Post by jayd16 »

pjmlp wrote: post #330
jayd16 wrote: post #329

Earlier quoted context omitted.

For something like a web request, all the frameworks catch the exception at the request level. Prod should not be going down. Maybe you mean requests are failing on uncaught exceptions, in which case I'd say it's working well.

For the customer there is hardly any difference that the server keeps running if a critical workflow, especially with a payment in flight, crashes and burns. Or if they are unable to work, because they keep getting a maintenance page, as the load balancer redirects them after several HTTP 500 responses.

There're a huge different between a broken feature and the whole server crashing every time that feature is attempted.

Anyway, you prefer critical workflow like payment to show a success but actually be an unhandled error?

Re: Use Your Type System

#332

Post by steveklabnik »

ijustlovemath wrote: post #255
steveklabnik wrote: post #32

Earlier quoted context omitted.

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

Where can I sign?

Gonna be honest, at this point, I don't know how this all works in the Rust Project. https://github.com/rust-lang/types-team/issues/126

Re: Use Your Type System

#333

Post by arrowsmith »

0x457 wrote: post #174
josephg wrote: post #34

Earlier quoted context omitted.

Some people mistakenly call dynamic typing "weak typing" because they don't know what those words mean. PSA: Static typing / dynamic typing refers to whether types are checked at compile time or runtime. "Static" = compile time (eg C, C++, Rust). "Dynamic" = runtime (eg Javascript, Ruby, Excel) Strong / weak typing refers to how "wibbly wobbly" the type system is. x86 assembly language is "weakly typed" because regis…

It's strongly typed, but it's also duck typed. Also, in ruby everything is an object, even the class itself, so type checking there is weird. Sure it stops you from running into "'1' + 2" issues, but won't stop you from yeeting VeryRawUnvalidatedResponseThatMightNotBeAuthorized to a function that takes TotalValidatedRequestCanUseDownstream. You won't even notice an issue until: - you manually validate - you call a me…

You just described why I fell out of love with Ruby.

Re: Use Your Type System

#334

Post by ameliaquining »

ameliaquining wrote: post #229
tialaramex wrote: post #218

Earlier quoted context omitted.

AIUI WUFFS doesn't need a full blown proof assistant because instead of attempting the difficult problem "Can we prove this code is safe?" it has the programmer provide elements of such a proof as they write their program so it can merely ask "Is this a proof that the program is safe?" instead.

This is also approximately true of Idris. The thing that really helps Wuffs is that it's a pretty simple language without a lot of language features (e.g., no memory allocation and only very limited pointers) that complicate proofs. Also, nobody is particularly tempted to use it and then finds it unexpectedly forbidding, because most programmers don't ever have to write high-performance codecs; Wuffs's audience is pe…

Also, Wuffs doesn't let you prove arbitrary correctness properties, it aims only to prove the absence of memory corruption. That reduces how expressive the proof system has to be.

Re: Use Your Type System

#335

Post by IshKebab »

Ey7NFZ3P0nzAe wrote: post #283
IshKebab wrote: post #281

Earlier quoted context omitted.

I don't get it. If you already have type annotations just run Pyright surely?

No, pyright is called on static code. Beartime is called during the python process. Basically all my functions are decorated. See for example in wdoc, my advanced personal RAG system: https://github.com/thiswillbeyourgithub/wdoc/blob/main/wdoc/...

But why do you need to check types at runtime if you've already checked them statically?

Re: Use Your Type System

#336

Post by SAI_Peregrinus »

9rx wrote: post #248
SAI_Peregrinus wrote: post #246

Earlier quoted context omitted.

Unfortunately many languages treat exceptions as a primary control flow mechanism. That's part of why Rust calls its exceptions "panics" and provides the "panic=abort" compile-time option which aborts the program instead of unwinding the stack with the possibility of catching the unwind. As a library author you can never guarantee that `catch_unwind` will ever get used, so its main purpose of preventing unwinding acr…

> Unfortunately many languages Just Java (and Javascript by extension, as it was trying to copy Java at the time), really. You do have a point that Java programmers have infected other languages with their bad habits. For example, Ruby was staunchly in the "return errors as values and leave exception handling for exceptions" before Rails started attracting Java developers, but these days all bets are off. But the "pu…

Python as well. E.g. FileNotFoundError is an exception instead of a returned value.

Re: Use Your Type System

#337

Post by mrkeen »

munificent wrote: post #88
jevndev wrote: post #73

Earlier quoted context omitted.

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…

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

You have it backwards from where I'm standing.

'null' (and to a large extent mutability) drives a gigantic hole through whatever you're trying to prove with correct-by-construction.

You can sometimes annotate against mutability in OO, but even then you're probably not going to get given any persistent collections to work with.

The OO literature itself recommends against using constructors like that, opting for static factory pattern instead.

Re: Use Your Type System

#338

Post by iLemming »

0_gravitas wrote: post #268
josephg wrote: post #25

Earlier quoted context omitted.

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 ch…

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

Spec and Malli in Clojure feel like effing magic - so expressive, so simple - "data as code" philosophy means validations schemas are first-class citizens that can be manipulated, stored, transmitted, and reasoned about like any other data and that's just beautiful. For some type checks you can express in them, it is nearly impossible to achieve in TS, Rust or even Haskell. Clojure makes the complex feel simple because the language itself is designed around data transformation.

That power of course does come with a price, there does not exist a static analyzer that automatically checks things, even though you can pretty much generate beautiful tests based on specs. I think e.g. Rust teams can have more junior devs safely contribute due to enablement of less variability in code quality - the compiler enforces discipline. Clojure teams need higher baseline discipline but can move incredibly fast when everyone's aligned.

It's saddening to see when Clojure gets outright dismissed for being "untyped", even though it absolutely can change one's perspective about type systems.

Re: Use Your Type System

#339

Post by Ey7NFZ3P0nzAe »

throwaway290 wrote: post #319
Ey7NFZ3P0nzAe wrote: post #301

Earlier quoted context omitted.

Let me give you an example from just a minute ago: in plenty of cases np.array works on arrays as well as on lists. So you can have for example: ``` import numpy as np def func(inputA: np.ndarray, inputB: np.ndarray) -> np.ndarray: return np.concat(inputA, inputB) ``` But then you want to modify the code for some reason way later and do this: ``` def func(inputA: np.ndarray, inputB: np.ndarray) -> np.ndarray: if len(…

It makes sense I guess mostly if Python doesn't have good third party library typechecking... But how would beartype catch it? I mean a runtime error is a runtime error... You trade one for another?

Beartype does not catch errors, it checks before they happen.

Basically it's pure python ultra optimized code that calls "isinstance(a, b)" all the time everywhere. If there is a mismatch it crashes.

Note that you can also set it to warn instead of crash.

Re: Use Your Type System

#340

Post by Ey7NFZ3P0nzAe »

IshKebab wrote: post #335
Ey7NFZ3P0nzAe wrote: post #283

Earlier quoted context omitted.

No, pyright is called on static code. Beartime is called during the python process. Basically all my functions are decorated. See for example in wdoc, my advanced personal RAG system: https://github.com/thiswillbeyourgithub/wdoc/blob/main/wdoc/...

But why do you need to check types at runtime if you've already checked them statically?

Not all code can be checked statically. See the other child of the parent post for my example :)!
Post reply on HN