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

41–50 of 83 posts

Re: Typing Is Hard

#41

Post by elmo2you »

gpm wrote: post #12
rtpg wrote: post #9

After hearing "but Typescript is unsound!" a billion times.... kinda glad to se that being unsound is the "state of the art". I do wonder how far you can go without letting go of unsound-ness in practice though. Convenience is nice, guarantees are very very nice

I don't see how this article supports the idea that "unsoundness" is state of the art?

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 decade has been mostly a red herring. What I mean with that is that it appears to try solve the "wrong" problem. While strong typing certainly can solve a whole class of bugs, my impression is that where this has been required most, ended up always situations where horrible overall design and code quality were the actual main problems (not typing).

Coming from a (embedded) assembly and C direction myself, I have nothing against strong typing. But what has consistently rubbed me the wrong way about this modern strong typing "movement", both intuitively and rationally, is how it appears to fix something that is essentially broken on a whole different level. No amount of strong typing is going to fix that.

I know, nothing much actionable or concrete here. Just my opinion. Regardless, this old geezer certainly agrees with the overall impression that "unsound" is pretty much the state of this art, these days.

Re: Typing Is Hard

#42

Post by curryhoward »

leni536 wrote: post #40
curryhoward wrote: post #34

Earlier quoted context omitted.

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.

Non-Turing complete doesn't mean that you can't create too high complexity algorithms out of O(1) primitives.

Did you mean to reply to a different comment? You seem to be restating the correct part of orthoxerox's comment. I was merely refuting the incorrect part.

Re: Typing Is Hard

#45

Post by johncolanduoni »

Kutta wrote: post #38
bmc7505 wrote: post #33

Earlier quoted context omitted.

Just because the current implementation of the Idris type checker always terminates due to the size change termination heuristic does not mean that type checking Idris is decidable. If the type system as specified allows an author to express undecidable statements, it should not be considered decidable, regardless of whether one type checking implementation terminates on all inputs. If some type checker does not impl…

Incorrect. Whether the language as a logic is capable of expressing undecidable statements, is orthogonal to whether type checking is decidable. Type checking is analogous to checking proof validity in logics. Commonly used proof systems for first-order or higher-orders logics admit decidable proof validity, and already many first-order theories allow expressing undecidable statements. ZFC is a rather obvious example…

This is not true, as MLTT-style type theories have a different syntactical notion of proof than first order logical theories like ZFC. Proof of termination of type checking for Idris is equivalent to proof that all terms can be reduced to a normal form: for any given term, you can construct another term which when type checked requires fully normalizing the first term. It is well known that proving that the normal form evaluation of all terms in a MLTT type theory terminates is equivalent to the system’s consistency (because the false type has no constructors). This is how proofs of relative consistency of these type theories are usually proved.

Re: Typing Is Hard

#46

Post by remexre »

choeger wrote: post #43
xiaodai wrote: post #10

What Julia?

Julia has no (what some call "static" but that's actually the only form that matters) type system. It also has lisp-like macros.

Having no type system (e.g. Forth) is different from having dynamic checking for your types (e.g. JavaScript, Python, Julia iirc), though.

Julia also has Common Lisp-like multimethods, which are pretty nice, especially for linear algebra sorts of stuff, where you might be multiplying a scalar by a tensor, or a tensor by a tensor, and don't want to have to specify different syntax for the two operations.

Re: Typing Is Hard

#47

Post by p0llard »

> There exist many type inference algorithms, the best known one is the so-called Algorithm W.

Is this correct? I dug out Milner's paper [1] where he states that Algorithm J is more efficient (which was what I had been led to believe), but that Algorithm W is more suited to functional (as opposed to imperative) implementations.

Edit: Actually I think I'm parsing this sentence incorrectly, "best known" means literally that as opposed to "most efficient known".

[1] https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/...

Re: Typing Is Hard

#48

Post by bitwize »

elmo2you wrote: post #41
gpm wrote: post #12

Earlier quoted context omitted.

I don't see how this article supports the idea that "unsoundness" is state of the art?

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, because while a mediocre programmer's reach is extended, a great programmer's reach is even further extended. Mediocre programmers can thus meaningfully contribute to embedded and kernel-level code under the tutelage of a good programmer without risking blowing the whole thing up, and increase their skill.

Re: Typing Is Hard

#49

Post by throwaway894345 »

remexre wrote: post #46
choeger wrote: post #43

Earlier quoted context omitted.

Julia has no (what some call "static" but that's actually the only form that matters) type system. It also has lisp-like macros.

Having no type system (e.g. Forth) is different from having dynamic checking for your types (e.g. JavaScript, Python, Julia iirc), though. Julia also has Common Lisp-like multimethods, which are pretty nice, especially for linear algebra sorts of stuff, where you might be multiplying a scalar by a tensor, or a tensor by a tensor, and don't want to have to specify different syntax for the two operations.

I don’t see how JS or Python (not so sure about Julia) meaningfully have “dynamic checking for types”. If I have a function ‘def foo(a): return a.startswith(“foo”)’ and I pass an int in, Python doesn’t insert something like ‘if not isinstance(a, str): raise TypeError(“...”)’, partly because Python doesn’t even know that a str is expected; only that the param has a method called startswith(). And fair enough, maybe the type isn’t str in a statically typed language, but a Go-like structurally typed interface with a startswith() method; however, the function also isn’t inserting any meaningful check until the last possible moment when there is nothing left to do but blow up anyway, so I don’t see how this can meaningfully be called “dynamic type checking” when the types are all implicit and maximally abstract and the “check” is only dynamic dispatch. Pretty sure this all applies equally to JS except that a failed dynamic dispatch doesn’t raise an AttributeError but “undefined is not a function” IIRC. Not sure about Julia behavior, but I would guess that it also isn’t going to be sprinkling dynamic checks all over given its aspirations toward performance.

Re: Typing Is Hard

#50

Post by fluffy87 »

rtpg wrote: post #9

After hearing "but Typescript is unsound!" a billion times.... kinda glad to se that being unsound is the "state of the art". I do wonder how far you can go without letting go of unsound-ness in practice though. Convenience is nice, guarantees are very very nice

The state of the art is Idris, which has a sound, decidable, and extremely powerful type system. Most state of the art mainstream languages like Rust have sound but undecidable type systems.

Many older languages with ad-hoc type systems are unsound, but there are also some older relatively used languages with powerful and sound type systems like Haskell.

Post reply on HN