Live data from Hacker News

Use Your Type System

dzombak.com

211–220 of 357 posts

Re: Use Your Type System

#211
My team recently did this to some C++ code that was using mixed numeric values. It started off as finding a bug. The bug was fixed but the fixer wanted to add safer types to avoid future bugs. They added them, found 3 more bugs where the wrong values were being used unintentionally.

Re: Use Your Type System

#212

Earlier quoted context omitted.

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

I recall a type theorist once defined the terms as follows (can't find the source): "A strongly typed language is one whose type system the speaker likes. A weakly typed language is one whose type system the speaker dislikes." Related Stack Overflow post: https://stackoverflow.com/questions/2690544/what-is-the-diff... So yeah I think we should just give up these terms as a bad job. If people mean "static" or "dynamic…

I think you might be thinking of https://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wr...

It says:

> I give the following general definitions for strong and weak typing, at least when used as absolutes:

> Strong typing: A type system that I like and feel comfortable with

> Weak typing: A type system that worries me, or makes me feel uncomfortable

Re: Use Your Type System

#213
post #38

Earlier quoted context omitted.

irb(main):001:0> a = 1 => 1 irb(main):002:0> a = '1' => "1" It doesn't seem that strong to me.

It would be weak if that was actually mutating the first “a”. That second declaration creates a new variable using the existing name “a”. Rust lets you do the same[1]. [1] https://doc.rust-lang.org/book/ch03-01-variables-and-mutabil...

Rust lets you do the same because the static typing keeps you safe. In Rust, treating the second 'a' like a number would be an error. In ruby, it would crash.

Re: Use Your Type System

#214
post #25
post #3

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…

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…

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.

Re: Use Your Type System

#215
I've used the approach described for uuids on a project and I liked it. We were using typescript so we went further using template literal types [1]

    type UserId = `user:${uuid}`;
    type OrgId = `org:${uuid}`;
This had the benefit that we could add validation (basic begins with kind of logic) and it was obvious upon visual inspection (e.g. in logs/debugging).

1. https://www.typescriptlang.org/docs/handbook/2/template-lite...

Re: Use Your Type System

#216

they constantly try to escape from the darkness outside & within by dreaming of type systems so perfect that no one will need to be good but the strings that are will shadow the abstract datatype that pretends to be

[deleted]

Re: Use Your Type System

#217
post #201

Earlier quoted context omitted.

And that's my point: I'm usually getting AccountIDs from strings (passed in via HTTP requests) so the whole thing becomes a pointless exercise.

You just accept raw strings without doing any kind of validation? The step that performs validation should encode that step in the form of a type.

i pride myself in never doing any validation ever

never escape anything, either

just hand my users a raw SQL connection

Re: Use Your Type System

#218

Earlier quoted context omitted.

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

The full-blown version that guarantees no bounds-check errors at runtime requires dependent types (and consequently requires programmers to work with a proof assistant, which is why it's not very popular). You could have a more lightweight version that instead just crashes the program at runtime if an out-of-range assignment is attempted, and optionally requires such fallible assignments to be marked as such in the c…

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.

Re: Use Your Type System

#219

I've used the approach described for uuids on a project and I liked it. We were using typescript so we went further using template literal types [1] type UserId = `user:${uuid}`; type OrgId = `org:${uuid}`; This had the benefit that we could add validation (basic begins with kind of logic) and it was obvious upon visual inspection (e.g. in logs/debugging). 1. https://www.typescriptlang.org/docs/handbook/2/template-li…

I assume you used these against a relational database? Did you commit those ids with the prefix still attached? or did you `.split()[1]` or something?

I think it's a pretty good idea. I'm just wondering how this translated to other systems.

Re: Use Your Type System

#220
post #116

Earlier quoted context omitted.

> 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. Presumably you need to know what an Account and a User are to use that software in the first place. I can't imagine a reasonable person easily understanding a getAccountById function which takes one argument of type UUID, but having trouble understanding a getAccountById func…

UserID and AccountID could just as well be integers. What he means is that by introducing a layer of indirection via a new type you hide the physical reality of the implementation (int vs. string). The physical type matters if you want to log it, save to a file etc. So now for every such type you add a burden of having to undo that indirection. At which point "is it worth it?" is a valid question. You made some (but…

Well...yeah. That's the point. We want there to be a layer of indirection to prevent mistakes. Otherwise you get things like this: https://www.columbia.edu/~ng2573/zuggybuggy_is_2scale4ios.pd...

> There is a UI for memorialising users, but I assured her that the pros simply ran a bit of code in the PHP debugger. There’s a function that takes two parameters: one the ID of the person being memorialised, the other the ID of the person doing the memorialising. I gave her a demo to show her how easy it was....And that’s when I entered Clowntown....I first realised something was wrong when I went back to farting around on Facebook and got prompted to login....So in case you haven’t guessed what I got wrong yet, I managed to get the arguments the wrong way round. Instead of me memorialising my test user, my test user memorialised me.

Post reply on HN