Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why Type Systems Matter

matthias-endler.de

Post reply on HN
Print view View original

81–90 of 103 posts

Re: Why Type Systems Matter

#81

Post by naasking »

kmill wrote: post #77
naasking wrote: post #75

Earlier quoted context omitted.

> Is in inconceivable that a programmer can check their types manually, using an ad hoc intuitive type system? Sure, if you don't mind an ad-hoc, informally specified, bug-ridden, slow implementation of half of a type checker that no one but you knows (and so is "intuitive" only to you... until you read this same code 3 months later).

What are you addressing? My position is that automatic type checkers are nice to have but not essential, and it is possible to prototype software without one. I am not arguing against their use, just what seemed to be your assertion that it is impossible to prototype/develop software without an automatic type checker. Anyway, I understand the pitfalls of not using one, but I also understand how type systems tend not…

> My position is that automatic type checkers are nice to have but not essential, and it is possible to prototype software without one.

Sure, it's possible to prototype in the untyped lambda calculus too, or in Brainfuck. Why would you want to though?

> I am not arguing against their use, just what seemed to be your assertion that it is impossible to prototype/develop software without an automatic type checker.

I never said it was impossible, I merely implied that it was bizarre to even want to do so (among other things). Programming is hard enough as it is, why waste your time and mental energy checking properties that can be checked for you?

> I was talking about a programmer with a type theory, not implementing an automatic type checker from scratch.

A type theory in their head, in the intuitionistic sense, that they check as they're programming, not one that's actually checked by a tool is what I assumed.

And certainly you're working within limitations dictated by your language, but you can take typically it further than most think. See for instance, the paper lightweight static capabilities.

Re: Why Type Systems Matter

#82

Post by sqeaky »

rocky1138 wrote: post #50
seanwilson wrote: post #11

Earlier quoted context omitted.

Can you give an example? I don't find this personally. I find static strong typing speeds me up because I don't have to restart the app, click some buttons etc. to figure out some code was wrong. This is true even for prototypes. Most of the time any type declarations you need are straightforward and once you know your code better you can start introducing more exotic types to capture more errors later.

A really basic example would be the "as GameObject" part of this statement in C#: `GameObject gameObject = GameObject.Instantiate(MyGameObject, Vector3.zero, Quaternion.Identity) as GameObject;". It's annoying to have to type "as GameObject" when very clearly I am creating a GameObject type (the first thing in the entire statement). Programming languages should be smart enough to figure out that's what I'm trying to…

Have an upvote for being perfectly reasonable and attempting to provide examples and reason, even if I disagree with them.

Rather than deflect away from C#, I will take the unpopular stance of defending verbosity.

Does typing that really represent a large waste of time? Do you spend more time physically typing than doing anything else while coding?

I spend most my time thinking or reading old code. I might type that once and read it 100 times and pass the debugger over it 6 or 7 times and adjust the line a similar amount in the lifespan of that of the code.

For reading it is entirely clear and leaves little ambiguity about what kinds of operations are allowed on GameObject (presuming I know something about the GameObject class and the Entity Component System in place). I know its location and its rotation and I know that those are unlikely to be the source of bugs.

I might need to reference `MyGameObject` to get the specifics of the behavior, but if I am troubleshooting location or rotation errors, I know what code I am not looking at. If I am troubleshooting any other behavior I again know about whole regions of code I don't need to look at.

It can be hard to internalize all that a type system buys for you because none of it is immediate, it is more about all the time you don't spend doing unproductive things. I find that in more dynamically typed languages I spend two the three times as much time debugging than in static languages.

Re: Why Type Systems Matter

#83

Post by mamcx »

My dream is a static-first (like with inmutable-first) language with a way to do dynamic.

The thing is not available (as far I know) is to build a dynamic object and "close it" for further modification so the compiler can optimize well. Other, that requiere good metaprograming, is to build a dynamic object AT COMPILE TIME (macro?) and close it, then the type-system work after that (F# type provider is almost this)

A use case is reflect a database/data storage like JSON or relational table. I wish, like with python, to do:

    class Customer = @build(table("Customer"))
and after this line :

    c = Customer()
    print c.name
to 'c' be a static type. If at compile time, it check the type, let say the field change to c.fullname, to mark as a type error.

If in runtime, like a interpreter, to "close" Customer and be certain that it never will mutate.

AKA: Inmutable types/clases, but the posibility to mutate it in some discret places.

Make sense?

Re: Why Type Systems Matter

#84

Post by Veedrac »

jerf wrote: post #29
Veedrac wrote: post #23

Earlier quoted context omitted.

> If you can find the right type, you can solve the problem. Do you actually believe this?

What's the most advanced type system you've used? It's quite difficult to explain how much work a very strong type system can do for you if you're used to something like C as your definition of "static typing". I mean this comment comment completely straight and polite, and I'm trying to help people answer your very reasonable question by asking you for some details that will help calibrate the answer.

Technically that would be something like Haskell's, but I only have surface-level fluency. More to the point would be the most complex stuff I've had reason to do with a type system, which caps at around this generic state machine:

https://play.rust-lang.org/?gist=3fdb20c34d589a2576c6bb137b9...

(TL;DR: A type that encodes a state machine (and is generic over the implementation) that allows you to guarantee reaching a terminating state.)

In practice I rather my types looking much plainer, though:

https://github.com/llogiq/bytecount/blob/master/src/lib.rs

Re: Why Type Systems Matter

#85

Post by kazinator »

dozzie wrote: post #63
msla wrote: post #14

Earlier quoted context omitted.

The conflation between 'strong' and 'static', and 'weak' and 'dynamic', is probably terminal at this point, but maybe I can do something to, at least, explain the position of the people who don't conflate those terms: Strong typing is about creating, expressing, and enforcing a contract which determines which operations are valid on which values. Not variables, values . Having the semantics of the value in the compil…

> The conflation between 'strong' and 'static', and 'weak' and 'dynamic', is probably terminal at this point, Type system of C is weak and static. Type system of JavaScript is weak and dynamic. Type system of Lisp is strong and dynamic. Type system of OCaml is strong and static. Type system of Python is dynamic. It may be strong or weak, depending on your opinion about duck typing (does it weaken the type system or n…

The "weak" terminology has a flaw because it sometimes means "leaves type errors undetected, with undefined behavior" and sometimes it refers to a situation whereby a character string like "3.14" can be treated as a number and such.

Awk and Perl are not weakly typed in the same sense that C is weakly typed.

Re: Why Type Systems Matter

#86

Post by Veedrac »

naasking wrote: post #47
Veedrac wrote: post #23

Earlier quoted context omitted.

> If you can find the right type, you can solve the problem. Do you actually believe this?

Absolutely. It's little different than asking whether you can solve a problem once you have the appropriate data structure. Solving the problem when the right data structure is available becomes almost trivial -- most of the difficult of programming is recognizing what data structures are needed. Very few of the problems we encounter in every day programming don't fall when the right data structure is available.

It's not the same at all; data structures frequently actually are half the problem, though that's not to say that insight buys you anything.

Let's say I want to stream logging data at a massive rate (~peak core-core bandwidth) to another core and perform complex queries and visualisations on it in sub-frame times. If I have the data structure for that, the rest is bookwork. If I have the type... what have I gained?

Let's say I want to find the best way to represent my data in a way that's amiable to GPU operations. If I find a data structure for that, I'm left with the other half of the job in mapping the transformations I need to GPU calls. If I write some types for it, it's not like GPUs start being any less buggy.

Let's say I'm writing an extension for a Java program with an API not designed for my use-case, and I want to work out how to access stuff that's not directly intended to be exposed. A data structure design isn't much good, since it's an exploratory problem, but neither is assigning types to random things. I still need to figure out how to abuse the API.

Let's say I'm trying to solve the Halting Problem. If I have a data structure for that, I've pretty much proven FALSE, and literally everything is provable. Conversely, I can already give you the type and I'm no closer to solving it.

Re: Why Type Systems Matter

#87

Post by gumby »

shakna wrote: post #39
gumby wrote: post #16

Some languages mix static and dynamic typing. For example MACLISP used this to great effect to make MACSYMA super fast. All the numeric code was statically typed and the compiler built code that was as fast as hand crafted assembly. Yet you could write conventional Lisp code that called this static code just like any other code. MACLISP derivatives like lisp machine lisp also implemented this stuff and used it for sy…

C++ is in this boat now. Most of the time I'd recommend the new type-safe union std::variant, but std::any is there. It is kinda a static type, but as a container-type of anything in the type system, it may as well be a dynamic type. --- > All that survived into Common Lisp but I am not up on the current state of lisp implementations and have no idea if people bother to take advantage of it any more. Typed Racket use…

> Most of the time I'd recommend the new type-safe union std::variant

Neither g++ 7 nor Clang/LLVM 4.0.1 support std::variant yet :-(. We started a new (blank buffer) codebase earlier this year and decided to use C++17 as the implementation language, which has exposed us to the gaps...which are surprisingly few! But sadly this is one of them.

Re: Why Type Systems Matter

#88

Post by h_r »

mamcx wrote: post #83

My dream is a static-first (like with inmutable-first) language with a way to do dynamic. The thing is not available (as far I know) is to build a dynamic object and "close it" for further modification so the compiler can optimize well. Other, that requiere good metaprograming, is to build a dynamic object AT COMPILE TIME (macro?) and close it, then the type-system work after that (F# type provider is almost this) A…

This sounds similar to F# type providers.

Re: Why Type Systems Matter

#89

Post by 62747478182 »

mamcx wrote: post #83

My dream is a static-first (like with inmutable-first) language with a way to do dynamic. The thing is not available (as far I know) is to build a dynamic object and "close it" for further modification so the compiler can optimize well. Other, that requiere good metaprograming, is to build a dynamic object AT COMPILE TIME (macro?) and close it, then the type-system work after that (F# type provider is almost this) A…

You may be interested in Crystal.

https://crystal-lang.org/

Re: Why Type Systems Matter

#90

Post by dmux »

seanwilson wrote: post #11
rocky1138 wrote: post #2

Strong typing is great when I've already made sense of how the logic should flow and I'm ready to solidify my work into something stable and extensible over time. It's not so great when I'm trying something new and am still trying to work out if what I want to do is even possible, since I find myself trying to identify the right type to use in a given situation rather than proving that I'm even able to do it. A lot o…

Can you give an example? I don't find this personally. I find static strong typing speeds me up because I don't have to restart the app, click some buttons etc. to figure out some code was wrong. This is true even for prototypes. Most of the time any type declarations you need are straightforward and once you know your code better you can start introducing more exotic types to capture more errors later.

> I find static strong typing speeds me up because I don't have to restart the app, click some buttons etc.

I'd blame this more on our current programming environments than anything. Smalltalk is exceptionally productive and doesn't require restarting to test things.

Post reply on HN