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

11–20 of 83 posts

Re: Typing Is Hard

#11

Post by gpm »

tlb wrote: post #8
kps wrote: post #7

If you have some form of Turing-complete macros, then macro processing might not terminate. I don't see why this is anything but trivial, or a compelling argument against Turing-complete macros.

I don't think it's a compelling argument against having such a language. But you might want to know what you're up against if, say, you decide to write an autocompleter for your editor that needs to know types.

If you're writing an autocompleter, you have the bigger problem that it has to function when the program isn't valid syntax, or is valid syntax but has just plain contradictory type information and doesn't typecheck. Non-terminating typechecking seems easy to handle in comparison.

Re: Typing Is Hard

#12

Post by gpm »

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?

Re: Typing Is Hard

#13

Post by greggman3 »

kps wrote: post #7

If you have some form of Turing-complete macros, then macro processing might not terminate. I don't see why this is anything but trivial, or a compelling argument against Turing-complete macros.

Because turing complete macros are super powerful. See lisp

Re: Typing Is Hard

#14

Post by jolux »

kps wrote: post #7

If you have some form of Turing-complete macros, then macro processing might not terminate. I don't see why this is anything but trivial, or a compelling argument against Turing-complete macros.

This page isn't arguing against anything though.

Re: Typing Is Hard

#15

Post by ekidd »

Pretty much any language supporting something like C++'s "template metaprogramming" will allow the programmer to perform arbitrary computation at compile time. This is, of course, "undecidable", because it's Turing complete.

This is not necessarily the end of the world. If you go out of your way to write an actual compile-time program by abusing your type system, and that program contains an endless loop, you probably shouldn't be surprised that your compiler hangs.

Unsound type systems cause more headaches in practice. For example, TypeScript types are only trustworthy if your program is careful about boundaries with the outside world. In larger, older systems, I occasionally do get bit by this.

Re: Typing Is Hard

#16

Post by minerjoe »

tlb wrote: post #8
kps wrote: post #7

If you have some form of Turing-complete macros, then macro processing might not terminate. I don't see why this is anything but trivial, or a compelling argument against Turing-complete macros.

I don't think it's a compelling argument against having such a language. But you might want to know what you're up against if, say, you decide to write an autocompleter for your editor that needs to know types.

In lisp and in other languages you just ask the running process.

Re: Typing Is Hard

#17

Post by clashmeifyoucan »

singhrac wrote: post #6
clashmeifyoucan wrote: post #4

Ah, I recently started using type hints in Python. Would've loved to see how that compares even though it's not inherently a statically typed language!

Python's type system is an instance of "gradual typing" (like e.g. TypeScript). PEP 483 is actually a nice introduction to this: https://www.python.org/dev/peps/pep-0483/

Right, it should still be possible to statically type it for the purpose of testing. Wouldn't really be close to practical usage but I'd still be interested in seeing how it compares.

Re: Typing Is Hard

#20

Post by guerrilla »

ekidd wrote: post #15

Pretty much any language supporting something like C++'s "template metaprogramming" will allow the programmer to perform arbitrary computation at compile time. This is, of course, "undecidable", because it's Turing complete. This is not necessarily the end of the world. If you go out of your way to write an actual compile-time program by abusing your type system, and that program contains an endless loop, you probabl…

> Pretty much any language supporting something like C++'s "template metaprogramming" will allow the programmer to perform arbitrary computation at compile time.

It depends on what you mean by "something like" because Idris' dependent types are arguably equally as useful in practice but type checking remains decidable due to totality. This goes for Agda, Coq and Epigram (if it still exists?) as well for different technical reasons each, not that they are as convenient to program with.

Post reply on HN