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

311–320 of 357 posts

Re: Use Your Type System

#311

Post by sparkie »

fellowniusmonk wrote: post #71

Complex types don't exist. Schemas do. There is no duck, just primitive types organized duck-wise. The sooner you embrace the truth of mereological nihilism the better your abstractions will be. Almost everything at every layer of abstraction is structure. Understanding this will allow you to still use types, just not abuse them because you think they are "real".

Arguably, you can get rid of "primitive types" entirely. xtc-lang's "Turtles type system" does so, where all the built-in types are defined in the standard library, where the definitions are infinitely recursive, but we have a fixpoint which we can use as if it were "primitive".

> The Ecstasy type system is called the Turtles Type System, because the entire type system is bootstrapped on itself, and -- lacking primitives -- solely on itself. An Int, for example, is built out of an Array of Bit, and a Bit is built out of an IntLiteral (i.e. 0 or 1), which is built out of a String, which is an Array of Char, and a Char is built out of an Int. Thus, an Int is built out of many Ints. It's turtles, the whole way down.

[1]:https://xtclang.blogspot.com/2019/06/an-introduction-to-ecst...

Re: Use Your Type System

#312

Post by arch_btw »

Wait until you find out about Julia, the typesystem is brilliant. It encourages this kind of thing to allow you to give more info about what the number represents. It ensures there are no downsides because you can define functions to run on families of types.

Re: Use Your Type System

#313

Post by sparkie »

somethingsome wrote: post #143

I'm curious about what you think about something, Supoose you make two simple types one for Kelvin K and the other for Fahrenheit F or degrees D. And you implement the conversions between them in the types. But then you have something like d: D = 10; For i=1...100000: k=f_Take_D_Return_K(d) d=g_Take_K_Return_D(k) end Then you will implicitly have many many automatic conversions that are not useful. How to handle this…

In F#, which has measure types, the types are checked at compile time but erased at runtime, so they have no additional runtime cost. Measures are a kind of painted type.

    [] type degC;
    [] type K;

    let degrees_to_kelvin (degrees : float) : float = 
        degrees * 1 + 273.15

    let d = 10.0
    let k : float = degrees_to_kelvin d
The .NET runtime only sees `float`, as the measures have been erased, and constant folding will remove the `*1` that we used to change the measure. The `degrees_to_kelvin` call may also be inlined by the JIT compiler. We could potentially add `[]` to force it to inline when possible, then constant folding may reduce the whole expression down to its result in the binary.

The downside to adding the SI into the type system is the SI is not a sound type system. For example:

    [] type m
    [] type s
    [] type kg
    [] type N = kg*m/s^2
    [] type J = kg*m^2/s^2
    [] type Nm = N*m

    let func_expecting_torque (t : float) = ...
 
    let x = 10.0
    func_expecting_torque x
The type system will permit this: using torque where energy is expected, and vice-versa, because they have the same SI unit, but they don't represent the same thing, and ideally it should be rejected. A potential improvement is to include Siano's Orientational Analysis[1], which can resolve this particular unsoundness because the orientations of Nm and J would be incompatible.

[1]:https://www.doc88.com/p-9099799188322.html

Re: Use Your Type System

#314

Post by xigoi »

alex_smart wrote: post #183
lock1 wrote: post #103

Earlier quoted context omitted.

If only Java also provided Either -like in the standard library... Personally I use checked exceptions whenever I can't use Either and avoid unchecked like a plague. Yeah, it's pretty sad Java language designer just completely deserted exception handling. I don't think there's any kind of improvement related to exceptions between Java 8 and 24.

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

Either allows you to do things like map, flatMap, getOrDefault, etc., whereas exceptions can only be handled via try/catch blocks.

Re: Use Your Type System

#315

Post by SideburnsOfDoom »

tyleo wrote: post #309
SideburnsOfDoom wrote: post #278

Earlier quoted context omitted.

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.

I completely agree that libraries do have to prove their worth, and that you should not add them as though they are all zero-cost and zero weight - that is not true.

However I disagree in this case - if you have the problem that the library solves and it is ergonomic, then why not use it. Your "5-line-of-code example" doers not cover validation, and serialisation and casting concerns. As another commenter put it: "a properly constructed ID type has a non-trivial amount of code".

If you don't need more lines of code than that, then do your thing. But in the example that I looked at, I definitely would. As I said elsewhere in the thread, it is where all customer ids are strings, but only very specific strings are customer ids.

The larger point is that people who write c# and are reading this thread should know that these toolkits exist - that url links to other similar libraries and further reading. So they can can then make their own informed choices.

Re: Use Your Type System

#316

Post by thfuran »

recursivedoubts wrote: post #217
Kranar wrote: post #201

Earlier quoted context omitted.

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

I prefer to just skip a few steps and email them my bank account number when they register an account.

Re: Use Your Type System

#318

Post by sparkie »

scottgg wrote: post #109
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…

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

There's refinement types, which are less general than dependant types, but sufficient to provide ranges, and simpler to implement because the type only needs to be associated with a predicate.

Re: Use Your Type System

#319

Post by throwaway290 »

Ey7NFZ3P0nzAe wrote: post #301
throwaway290 wrote: post #298

Earlier quoted context omitted.

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

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?

Re: Use Your Type System

#320

Post by Warwolt »

abujazar wrote: post #206

Separate types for each model id is an extremely tedious way of avoiding bugs that can easily be prevented by a single test.

Types give you static proof where tests only give partial inductive evidence. I cannot _fathom_ why people would prefer tests over types where types do the job, outside anything but sheer ignorance.
Post reply on HN