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

341–350 of 357 posts

Re: Use Your Type System

#341

Post by pjmlp »

jayd16 wrote: post #331
pjmlp wrote: post #330

Earlier quoted context omitted.

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?

For the customer the difference hardly matters, they cannot fulfill what they intended to do, because someone somewhere forgot to catch an exception, going all the way out of the MVC controller, providing a very bad UI/UX, and from security point of view, a possible DOS attack vector.

I prefer an happy customer, and not having to deal with support calls.

Re: Use Your Type System

#342

Post by ragnese »

Jtsummers wrote: post #50
abraxas wrote: post #37

An adjacent point is to use checked exceptions and to handle them appropriate to their type. I don't get why Java checked exceptions were so maligned. They saved me so many headaches on a project where I forced their use as I was the tech lead for it. Everyone hated me for a while because it forced them to deal with more than just the happy path but they loved it once they got in the rhythm of thinking about all the…

Setting aside the objections some have to exceptions generally: Checked exceptions, in contrast to unchecked, means that if a function/method deep in your call stack is changed to throw an exception, you may have to change many function (to at least denote that they will throw that exception or some exception) between the handler and the thrower. It's an objection to the ergonomics around modifying systems. Think of…

> Setting aside the objections some have to exceptions generally: Checked exceptions, in contrast to unchecked, means that if a function/method deep in your call stack is changed to throw an exception, you may have to change many function (to at least denote that they will throw that exception or some exception) between the handler and the thrower. It's an objection to the ergonomics around modifying systems.

And if you change a function deep in the call stack to return a different type on the happy path? Same thing. Yet, people don't complain about that and give up on statically type checking return values.

I honestly think the main reason that some people will simultaneously enjoy using Result/Try/Either types in languages like Rust while also maligning checked exceptions is because of the mental model and semantics around the terminology. I.e., "checked exception" and "unchecked exception" are both "exceptions", so our brains lumped those two concepts together; whereas returning a union type that has a success variant and a failure variant means that our brains are more willing lump the failure return and the successful return together.

To be fair, I do think it's a genuine design flaw to have checked and unchecked exceptions both named and syntactically handled similarly. The return type approach is a better semantic model for modelling expected business logic "failure" modes.

Re: Use Your Type System

#343

Post by worldsayshi »

alex_smart wrote: post #303
worldsayshi wrote: post #190

Earlier quoted context omitted.

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

Sure

I point it out because I think the distinction is interesting.

Can we build tools that helps us work with the boundary between isosemantic and isomorphic? Like any two things that are isosemantic should be translatable between each other. And so it represents an opportunity to make the things isomorphic.

Re: Use Your Type System

#344

Post by dabears »

voidhorse wrote: post #249
tylerhou wrote: post #176

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…

Hello! I was curious if you would happen to have any advice or particular comp sci papers you would point as aspiring compiler developer towards.

I think I'm sort of who you're talking about. I have no formal education and I am excited to have my compiler up to the point I can run a basic web server. I think it's a fairly traditional approach with a lexer, recursive decent parser, static analysis, then codegen. I'm going for a balance between languages like Ruby and Rust to get the best of both worlds.

You'll probably find it funny that I don't know the name for the technique Im using for dynamic dispatch. The idea is that as long as a collection doesn't have mixed types then the compiler statically knows the type even in loops and such. Only for mixed type collections, or maybe trait functions, will the compiler be forced to fall back to runtime dynamic dispatch. I find this cool because experts can write fast static code, but beginners won't be blocked by the compiler complaining about things they shouldn't have to care about yet. But, syntax highlighting or something may hint there are improvements to be made. If there is a name for this, or if it's too small a piece to deserve one, I would be very curious to know!

On Refinement Types, I not sure they are a good idea for general purpose languages and would love to be challenged on this. Succinctly, I think it's a leaky abstraction. To elaborate, having something like a `OneThroughTen` type seems helpful at first, but in reality it's spreading behaviour potentially all over the app as opposed to having a single function with the desired behaviour. If a developer has multiple spots they're generating a number and one spot is missing a check and causes a bug, then hopefully a lesson was learned not to do that and instead have a single spot for that logic. The heavy handed complexity of Refinement Types is not worth it to solve this situation.

If there are any thoughts out there they would be greatly appreciated!

Re: Use Your Type System

#345

Post by [deleted] »

pjmlp wrote: post #341
jayd16 wrote: post #331

Earlier quoted context omitted.

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?

For the customer the difference hardly matters, they cannot fulfill what they intended to do, because someone somewhere forgot to catch an exception, going all the way out of the MVC controller, providing a very bad UI/UX, and from security point of view, a possible DOS attack vector. I prefer an happy customer, and not having to deal with support calls.

[deleted]

Re: Use Your Type System

#346

Post by balamatom »

kazinator wrote: post #49
pclowes wrote: 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…

Also known as "make bad state unexperimentable".

Hahaha. Nice coinage! Funny they set out to do the former then we have to deal with how they've achieved the later

Re: Use Your Type System

#347

Post by mcculley »

fny wrote: post #267
mcculley wrote: post #55

Earlier quoted context omitted.

Ada has this ability to define ranges for subtypes. I wish language designers would look at Ada more often.

Range checks in Ada are basically assignment guards with some cute arithmetic attached. Ada still does most of the useful checking at runtime, so you're really just introducing more "index out of bounds". Consumer this example: procedure Sum_Demo is subtype Index is Integer range 0 .. 10; subtype Small is Integer range 0 .. 10; Arr : array(Index) of Integer := (others => 0); X : Small := 0; I : Integer := Integer'Val…

The comment to which I replied is about two concepts: Defining subtypes and an optimization made possible by them.

I get a lot of value out of compile time enforcement of subtypes (e.g., defining a function as requiring a parameter be Index instead of Integer) finding errors in my thinking. It is more than "cute" to me.

As for the possible optimization of the array bounds check and it happening at runtime instead of compiletime, isn't that a failure of GNAT and not Ada? Can't a sufficiently smart compiler detect the problem in your example?

Regardless, I am not convinced that getting around the compiletime type safety by casting with Integer'Value(Integer'Image(X)) proves anything. I will still prefer having subtypes over not having them.

Re: Use Your Type System

#349

Post by ninetyninenine »

owebmaster wrote: post #348
giraffe_lady wrote: post #154

Earlier quoted context omitted.

(derogatory)

I hope in 10 years we look to this typescript phase the way we see the coffeescript hype.

Coffeescript went obsolete because many of the features were directly folded into JS ES6.

If you think typescript will go the way of coffeescript. Well. First off, coffeescript was waaay less popular than typescript. Second, if it does it just means types will get folded directly into js.

Re: Use Your Type System

#350

Post by munificent »

mrkeen wrote: post #337
munificent wrote: post #88

Earlier quoted context omitted.

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

Nullability doesn't have anything to do with object-oriented programming.
Post reply on HN