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

261–270 of 357 posts

Re: Use Your Type System

#261

Post by valenterry »

reactordev wrote: post #99
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…

Union types!! If everything’s a type and nothing works together, start wrapping them in interfaces and define an über type that unions everything everywhere all at once. Welcome to typescript. Where generics are at the heart of our generic generics that throw generics of some generic generic geriatric generic that Bob wrote 8 years ago. Because they can’t reason with the architecture they built, they throw it at the…

union types are great. But alone they are not sufficient for many cases. For example, try to define a datastructure that captures a classical evaluation-tree.

You might go with:

    type Expression = Value | Plus | Minus | Multiply | Divide;
    
    interface Value    { type: "value"; value: number; }
    interface Plus     { type: "plus"; left: Expression; right: Expression; }
    interface Minus    { type: "minus"; left: Expression; right: Expression; }
    interface Multiply { type: "multiply"; left: Expression; right: Expression; }
    interface Divide   { type: "divide"; left: Expression; right: Expression; }
And so on.

That looks nice, but when you try to pattern match on it and have your pattern matching return the types that are associated with the specific operation, it won't work. The reason is that Typescript does not natively support GADTs. Libs like ts-pattern use some tricks to get closish at least.

And while this might not be very important for most application developers, it is very important for library authors, especially to make libraries interoperable with each other and extend them safely and typesafe.

Re: Use Your Type System

#262

Post by fny »

This is also an incredibly useful technique with LLMs. If you alias types (e.g. str to DateStr) the LLM can better infer which functions to select and how to compose them

Re: Use Your Type System

#263

Post by fny »

josephg wrote: post #25
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…

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…

But wouldn't that also require code execution? For example even though the compiler already knows the size of an array and could do a bounds check on direct assigment (arr[1] = 1) in some wild nested loop you could exceed the bounds that the compiler can't see.

Otherwise you could have type level asserts more generally. Why stop at a range check when you could check a regex too? This makes the difficulty more clear.

For the simplest range case (pure assignment) you could just use an enum?

Re: Use Your Type System

#264

Post by m_a_u »

fny wrote: post #262

This is also an incredibly useful technique with LLMs. If you alias types (e.g. str to DateStr) the LLM can better infer which functions to select and how to compose them

How would you do this? Don't you have to define your types using JSON schema which supports only a limited set?

Re: Use Your Type System

#265

Post by [deleted] »

josephg wrote: post #225
someone_19 wrote: post #181

Earlier quoted context omitted.

You can do this quite easily in Rust. But you have to overload operators to make your type make sense. That's also possible, you just need to define what type you get after dividing your type by a regular number and vice versa a regular number by your type. Or what should happen if when adding two of your types the sum is higher than the maximum value. This is quite verbose. Which can be done with generics or macros.

You can do it at runtime quite easily in rust. But the rust compiler doesn’t understand what you’re doing - so it can’t make use of that information for peephole optimisations or to elide array bounds checks when using your custom type. And you don’t get runtime errors instead of compile time errors if you try to assign the wrong value into your type.

[deleted]

Re: Use Your Type System

#266

Post by someone_19 »

josephg wrote: post #225
someone_19 wrote: post #181

Earlier quoted context omitted.

You can do this quite easily in Rust. But you have to overload operators to make your type make sense. That's also possible, you just need to define what type you get after dividing your type by a regular number and vice versa a regular number by your type. Or what should happen if when adding two of your types the sum is higher than the maximum value. This is quite verbose. Which can be done with generics or macros.

You can do it at runtime quite easily in rust. But the rust compiler doesn’t understand what you’re doing - so it can’t make use of that information for peephole optimisations or to elide array bounds checks when using your custom type. And you don’t get runtime errors instead of compile time errors if you try to assign the wrong value into your type.

Here is example of compile time error with wrong newtype argument:

https://play.rust-lang.org/?version=stable&mode=debug&editio...

rust-analyzer gives an error directly in IDE.

Re: Use Your Type System

#267

Post by fny »

mcculley wrote: post #55
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…

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'Value(Integer'Image(X));  -- runtime evaluation
begin for J in 1 .. 11 loop I := I + 1; end loop;

   Arr(I) := 42;  -- possible out-of-bounds access if I = 11
end Sum_Demo;

This compile, and the compiler will tell you: "warning: Constraint_Error will be raised at run time".

It's a stupid example for sure. Here's a more complex one:

    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'Value(Integer'Image(X));  -- runtime evaluation
    begin
       for J in 1 .. 11 loop
          I := I + 1;
       end loop;
 
       Arr(I) := 42;  -- Let's crash it
    end Sum_Demo;
This again compiles, but if you run it: raised CONSTRAINT_ERROR : sum_demo.adb:13 index check failed

It's a cute feature, but it's useless for anything complex.

Re: Use Your Type System

#268

Post by 0_gravitas »

josephg wrote: post #25
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…

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

Re: Use Your Type System

#269

Post by ninalanyon »

tylerhou wrote: post #176
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.

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.

Pascal had this many decades ago, how long do we have to wait?

Re: Use Your Type System

#270

Post by paulddraper »

kjksf wrote: post #116
tshaddox wrote: post #100

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…

I recommend adding a serialization method to your types, namely to text, but optionally to JSON as well.
Post reply on HN