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

Typing Is Hard

typing-is-hard.ch

Post reply on HN
Print view View original

61–70 of 83 posts

Re: Typing Is Hard

#61

Post by potiuper »

Kutta wrote: post #59
bmc7505 wrote: post #58

Earlier quoted context omitted.

I think you might be confusing the language and the type system. Not saying anything about the runtime characteristics of the language (which is obviously Turing Complete), but the type system itself, which is TC. If the type system allows you to encode a TM, then it is undecidable, regardless of whether it terminates due to an incomplete type checker. Since the Idris type system allows you to encode a TM, then the t…

A type system cannot be TC. What you seem to talk about, is that if a type checker can simulate arbitrary TM's through an encoding of its input, then the type checker is necessarily non-total. This is correct. But the Idris checker is total and it is not possible to use it to simulate TMs. The Idris type system does allow you to specify and formalize TMs internally, but that has no bearing on decidability of type che…

A type system can be TC. A type system is a logical system comprising a set of rules that assigns a property called a type to the various constructs of a computer program, such as variables, expressions, functions or modules. If those rules can encode a Turing complete system, then the system is Turing complete. Type checking is the process of verifying and enforcing the constraints of types. Type assignment is different from verification.

Re: Typing Is Hard

#62

Post by Roboprog »

Reminder: strict type checking is more trouble than it’s worth for some of us.

Ask yourself why dynamic type languages keep appearing, despite a fanatical resolve to purge them from the face of the earth? It’s almost as if some people prefer them.

But I guess the knowledge of salvation by compile time binding must be brought to the late binding heathens, to use a poor analogy.

On the other hand, I’m willing to admit that strict Compile time type checking is what many or most people prefer.

Re: Typing Is Hard

#63

Post by Roboprog »

Lammy wrote: post #25

The headline made me hope for an article about ergonomics.

I was expecting something about carpal tunnel syndrome or Dvorak keyboards as well.

Then I realized it was Haskell zealotry :-(

Re: Typing Is Hard

#64

Post by jcelerier »

intortus wrote: post #53
jcelerier wrote: post #35

Earlier quoted context omitted.

> Sure, you don't have to go out of your way to challenge your type system, but it still means that you're a single typo away from sending your compiler and yourself on a wild goose chase. the alternative would be writing bash or python or ... scripts to generate the code, and for those : - you likely don't have any error message at all (ugh) - they won't have knowledge of the type system of the language you're opera…

There are mainstream languages with decidable static type systems. They compile quickly and give obvious short error messages.

names ! we want names !

also, decidable likely implies total - and my experience with total languages is that more often than not you need to add another turing-complete "scripting" layer on top of it (for instance, a TC language to generate expressions in the total language) as it's so cumbersome to write otherwise when you have actually business rules and not simple math examples

Re: Typing Is Hard

#65

Post by elmo2you »

bitwize wrote: post #48
elmo2you wrote: post #41

Earlier quoted context omitted.

It may depend on age, overall knowledge of CS (including its history) and level of experience with multiple programming languages. Maybe the article itself does not literally support the idea, but it might still be inferred from it. It might also be the resulting discussion and responses, or additional field experience, that might give rise to this conclusion. I personally think the whole typing movement of the last…

Static typing takes the burden of verifying certain forms of program correctness off the programmer and puts it in the compiler where it belongs, thus expanding the space of correct code the same programmer can write per unit cognitive load. The more kinds of things you check for in the type system (static lifetimes in Rust, for instance), the more benefits you get. It doesn't serve as a substitute for good taste, be…

I get you point(s) and I guess you mean well. Statically typed languages do essentially what you said. They mostly (if not only) move data validation from run time to compile time. In dynamically typed languages, this often doesn't happen in the first place, while with static typing you are pretty much forced to.

I have a little over 30 years of programming experience, the majority of it in statically typed languages (and quite a few). I have absolutely nothing against them (on the contrary).

I still remember the rise in popularity of dynamically types languages, and how/why they were promoted. Faster development and code simplification, by only doing data validation where it was really needed (at run time), among them. Whether that was a good development, depends on where you stand. Do you care about correct software? Are you a business making software for profit, minimizing development costs? Are you part of a constantly growing market, where programmers who properly understand CS fundamentals are increasingly harder to find (or just more expensive)?

Either way, to me it's no surprise that dynamically typed languages became as popular as they did, nor would I say that it is totally without merit (depending on your perspective). Sadly, it's also a heck of a lot easier to make utter garbage with dynamically typed languages. Not in the least because a programmer would no longer be confronted with their intellectual excrement at compile time. Unless all edge cases are properly tested during dev time, those usually become "user problems" during run time.

People like me have frequently warned consultancy clients about the dangers of technologies and languages based on dynamically typed data, but more often than not other factors that were deemed more important. Fair enough, at least from a business perspective. Maybe not so much from an ethic and/or legal liability standpoint, but somehow the software industry has managed to create itself a rather unique immunity from legal consequence as the result of horrendous software quality (so good luck selling a need for better software).

Sure, the contemporary static typing movement (as I like to call it) does appear to have genuine intentions to assist programmer (some of which should probably not even be allowed to code) to write substantially less buggy code. But I certainly do not agree with this idea that static typing will extend both mediocre and great programmers. In fact, if any of contemporary statically typed languages (or worse: ad-hoc extensions to dynamically typed languages) make somebody write substantially better software, then I firmly believe that this person either has fundamental CS related problems, or is being rushed/pressured too much to ever produce anything of considerable quality. I sincerely doubt that a statically typed language (or language add-on) will ever fix either of those.

Such programmers will nonetheless still be good enough for a lot of regular programming gigs though. But, for the love of the gods, please keep those people miles away from anything embedded or kernel-level code.

Again, I think you mean nothing but good. You may even know far more on the subject than I can expect, just based on your response. Either way, I certainly don't mean to offend you. Still, whenever I read a response like your's, I can't escape the feeling that it sounds more like a repeated mantra than that in comes from a deep understanding of the actual problem, including its long/complicated history.

Re: Typing Is Hard

#66

Post by Kutta »

johncolanduoni wrote: post #60
Kutta wrote: post #54

Earlier quoted context omitted.

I don't see that "normalization implies consistency", which I'm aware of, relates to my previous comment in any relevant way. ZFC and MLTT do not differ in that decidability of proof validity is not related to logical expressiveness. It's not even true that for type theories, decidability of proof validity implies normalization. Normalization is not logically equivalent to decidable type checking. For example, we can…

You’ve actually hit on the difference here: in the type theory the witness term plus the reduction trace is equivalent to the ZFC proof. It’s true that checking this combination is decidable, regardless of consistency. The intentionality does not eliminate the limitations of this property, it only provides that the reduction trace is implicit given the witness term. The actual proofs of decidability of type checking…

What you say is kind of interesting but I get the impression that we are talking past each other.

id(X): ==(X, rec_0(0, X))

Sorry, what's this supposed mean, is it a definition? The propositional equality type has two or three arguments, I only see one (X) here, if as you say "id" is propositional equality.

In any case, nothing peculiar happens when we check a trace-annotated proof of bottom. We are free to use any particular finite-step unfolding of the non-normalizing proof.

We also don't need any paradox or inconsistency for a non-normalizing term, it is enough to work in ETT in a typing context which implies bottom, or which contains an undecidable equational theory, e.g. the rules of the SK-calculus.

> The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem

Decidability of type checking is always relative to a particular surface/raw syntax. A trace-annotated raw syntax does not need a normalization assumption for type checking.

Re: Typing Is Hard

#67

Post by joshuamorton »

curryhoward wrote: post #34
orthoxerox wrote: post #32

Earlier quoted context omitted.

A Turing-incomplete macro system will always terminate, but it may terminate in 2 years.

That's true in practice, but technically speaking it's false. You could imagine a contrived system which is not Turing complete but still contains a (rather useless) primitive that causes an infinite loop.

Arguably that would still terminate with an error message.

Re: Typing Is Hard

#68

Post by johncolanduoni »

Kutta wrote: post #66
johncolanduoni wrote: post #60

Earlier quoted context omitted.

You’ve actually hit on the difference here: in the type theory the witness term plus the reduction trace is equivalent to the ZFC proof. It’s true that checking this combination is decidable, regardless of consistency. The intentionality does not eliminate the limitations of this property, it only provides that the reduction trace is implicit given the witness term. The actual proofs of decidability of type checking…

What you say is kind of interesting but I get the impression that we are talking past each other. id(X): ==(X, rec_0(0, X)) Sorry, what's this supposed mean, is it a definition? The propositional equality type has two or three arguments, I only see one (X) here, if as you say "id" is propositional equality. In any case, nothing peculiar happens when we check a trace-annotated proof of bottom. We are free to use any p…

I left the first argument of the equality type implicit, written fully it’s ==(0, X, rec_0(0, X)) since those terms are both of type 0.

The overall expression is shorthand for any term whose typechecking involves that type assertion. For example, type checking passing the term to the left of the colon to an identity lambda with argument type of the term to the right of the colon (λ(x: ==(0, X, rec_0(0, X))).x)(id(X)) will pass iff the left term’s type is right term.

I’m not talking about extensional type theories here (as Idris/MLTT is not extensional), so I don’t think I understand the relevance of the trace annotated proof. Idris will let you write the term I have above without any trace annotations so its typechecker must do something with it.

You’re right that a trace-annotated raw syntax doesn’t need normalization assumptions, but Idris is not trace annotated; the type checking algorithm is required to perform any normalization required without further direction from the user.

Re: Typing Is Hard

#69

Post by lostmyoldone »

Roboprog wrote: post #62

Reminder: strict type checking is more trouble than it’s worth for some of us. Ask yourself why dynamic type languages keep appearing, despite a fanatical resolve to purge them from the face of the earth? It’s almost as if some people prefer them. But I guess the knowledge of salvation by compile time binding must be brought to the late binding heathens, to use a poor analogy. On the other hand, I’m willing to admit…

I generally agree, except if I don't. Whether or not that is the case, I'm entirely uncertain about!

Generalizing to transportation one might ask: What is the better transportation device, a boat or a horse?

... of which one can somewhat reasonably conclude, that whether the question itself is the right question, is the real question.

Few oppose types if they don't have to do anything at all and if it doesn't take any of their time either in runtime, compile time, or otherwise. Realities being what they are, there is always at least some parts of the aforementioned that is false for any type system that is actually useful.

Because of this, and for a few other similar characteristics of types and computation, it boils down to nothing but a question of which kind of tradeoffs people find palatable.

Given that premise, there should be no surprise that the answers are subjective no matter the responder. The question of better is here nothing but an entirely subjective question veiled as an ostensibly objective one.

Post reply on HN