Live data from Hacker News

Use Your Type System

dzombak.com

301–310 of 357 posts

Re: Use Your Type System

#301

Earlier quoted context omitted.

If you have a TypeError it's already too late. Decorating everything with beartype means I can catch things way in advance. It also forces me to specify types to all my functions which really helps LLM. See for example in wdoc, my advanced personal RAG library: https://github.com/thiswillbeyourgithub/wdoc/blob/main/wdoc/...

In advance but at runtime? I don't get the point still...

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(inputB.shape) == 1: return np.concat(inputA, inputB) else: return inputB ```

Now imagine that inputB is directly received from some library you imported. So pyright might not be able to check its type and inputB is actually a List. Then you will never get a crash in the version 1. But its types are wrong as inputB is a List.

The version 2 on the other hand will crash as List don't have a shape attribute. Notice also how func returns inputB, propagating the wrong type.

Sure that means the code still works until you modify version 1, but any developpers or LLM that reads func would get the wrong idea about how to modify such code. Also this example is trivial but it can become much much more complicated of course.

This would not be caught in pyright but beartype would. I'm basically using beartype absolutely everywhere I can and it really made me way more sure of my code.

If you're not convinced I'm super curious about your reasoning!

PS: also try/except in python are extremely slow so figuring out types in advance is always AFAIK a good idea performance wise.

Re: Use Your Type System

#302
post #250

Earlier quoted context omitted.

I think most complaints about checked exceptions in Java ultimately boil down to how verbose handling exceptions in Java is. Everytime the language forces you to handle an exception when you don't really need to makes you hate it a bit more. First, the library author cannot reasonably define what is and isn't a checked exception in their public API. That really is up to the decision of the client. This wouldn't be su…

That’s the same conclusion I’ve come too. I’ve commented on it a little bit here: https://news.ycombinator.com/item?id=44551088 https://news.ycombinator.com/item?id=44432640 > Your code probably shouldn't be throwing IOExceptions. But Java makes converting exceptions unnecessarily verbose The problem just compounds too. People start checking things that they can’t handle from the functions they’re calling. The caller…

There usually are more specific exceptions, at least when it's easy enough to distinguish the root cause from OS APIs. But it often isn't. A more practical concern is that it is not always easy to find out which type it is. The identity of the specific types might not be part of the public API interface, perhaps intentionally so.

Re: Use Your Type System

#303

Earlier quoted context omitted.

Ok please help me understand, what is the difference between - R method() throws L, and - Either method() To me they seem completely isomorphic?

Don't you mean "isosemantic"? Since the same concept is represented with different syntax.

Sure

Re: Use Your Type System

#304

Earlier quoted context omitted.

Academic language designers do! But it takes a while for academic features to trickle down to practical languages—especially because expressive-enough refinement typing on even the integers leads to an undecidable theory.

Eh, idk. I think the reasons are predominantly social, not theoretical. For every engineer out there that gets excited when I say the words "refinement types" there are twenty that either give me a blank stare or scoff at the thought, since they a priori consider any idea that isn't already in their favorite (primitivistic) language either too complicated or too useless. Then they go and reinvent it as a static analy…

<3

Re: Use Your Type System

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

> Functional languages can do this too, of course, using some combination of abstract types, the module system, and factory functions as convention

In Haskell:

1. Create a module with some datatype

2. Don't export the datatype's constructors

3. Export factory functions that guarantee invariants

How is that more complicated than creating a class and adding a custom constructor? Especially if you have multiple datatypes in the same module (which in e.g. Java would force you to add multiple files, and if there's any shared logic, well, that will have to go into another extra file - thankfully some more modern OOP languages are more pragmatic here).

(Most) OOP languages treat a module (an importable, namespaced subunit of a program) and a type as the same thing, but why is this necessary? Languages like Haskell break this correspondence.

Now, what I'm missing from Haskell-type languages is parameterised modules. In OOP, we can instantiate classes with dependencies (via dependency injection) and then call methods on that instance without passing all the dependencies around, which is very practical. In Haskell, you can simulate that with currying, I guess, but it's just not as nice.

Re: Use Your Type System

#306
post #289

Type systems, like any other tool in the toolbox, have an 80/20 rule associated with them. It is quite easy to overdo types and make working with a library extremely burdensome for little to no to negative benefit. I know what a UUID (or a String) is. I don't know what an AccountID, UserID, etc. is. Now I need to know what those are (and how to make them, etc. as well) to use your software. Maybe an elaborate type sy…

> I know what a UUID (or a String) is. I don't know what an AccountID, UserID, etc. is. It's literally the opposite. A string is just a bag of bytes you know nothing about. An AccountID is probably... wait for it... an ID of an Account. If you have the need to actually know the underlying representation you are free to check the definition of the type, but you shouldn't need to know that in 99% of contexts you'll wan…

The OP is the author of grugbrain.dev

Re: Use Your Type System

#307

Type systems, like any other tool in the toolbox, have an 80/20 rule associated with them. It is quite easy to overdo types and make working with a library extremely burdensome for little to no to negative benefit. I know what a UUID (or a String) is. I don't know what an AccountID, UserID, etc. is. Now I need to know what those are (and how to make them, etc. as well) to use your software. Maybe an elaborate type sy…

There are a few languages where this is not too tedious (although other things tend to be a bit more tedious than needed in those)

The main problem with these is how do you actually get the verification needed when data comes in from outside the system. Check with the database every time you want to turn a string/uuid into an ID type? It can get prohibitively expensive.

Re: Use Your Type System

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

in raku, that’s spelled subset OneToTen of Int where 1..10:

In Common Lisp it's

  (deftype One-To-Ten ()
    '(Integer 1 10))

Re: Use Your Type System

#309
post #161

Earlier quoted context omitted.

This seems like overkill. I’d prefer the few lines of code above to a whole library.

Is it "overkill" if it's already written and tested? Once you have several of these types, and they have validation and other concerns then the cost-benefit might flip. FYI, In modern c#, you could try using "readonly record struct" in order to get lots of equality and other concerns generated for you. It's like a "whole library" but it's a compiler feature.

Yes: more code to compile, more stuff to learn, more complexity. I gave like a 5-line-of-code example, I don’t understand why I’d want to replace that with a library.

Re: Use Your Type System

#310
post #34

Earlier quoted context omitted.

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

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…

[deleted]
Post reply on HN