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

Static Typing is not enough

blog.fogus.me

Post reply on HN
Print view View original

21–30 of 65 posts

Re: Static Typing is not enough

#21

Post by prodigal_erik »

jerf wrote: post #9
tomp wrote: post #4

Sometimes, I wish I could downvote stories... Accidentially, almost everything that the author suggests, except luck and user testing, can be provided by static type systems - e.g. Haskell's type system is Turing-complete, so you can make up any kind of contracts/tests and embed them into the type system...

With appropriate compiler flags, you can make up any sort of contracts you like in Haskell. But there's no guarantee that the compilation process will terminate if you do, even putting aside the impenetrability of the resulting code. Haskell is not a general purpose proof assistant, and the typing definitely has limits both practical and theoretical. Abstractly, static types can represent anything, however we (by whi…

Why do people worry about compilers hanging or giving up? If I know how to kill the failed compile and fix my program so that it is provably type-safe before shipping, I don't really care how many undecidable programs could also exist because I no longer have to ship one of those.

Re: Static Typing is not enough

#22

Post by carsongross »

jshen wrote: post #18
carsongross wrote: post #14

Earlier quoted context omitted.

Reliable dot completion without some batshit insane state-dependent VM-as-a-dev-env-or-constantly-running-tests system is... well, let's just say made much easier with static typing. I really could give a shit about what people think is "enough" (IMO, keeping stuff simple, as in simplicity of implementation, as in worse-is-better, is the only answer) I just want to hit dot and have a pretty good idea what I'm allowed…

Pry for ruby gives me great dot completion and isn't batshit insane. Most diehard dynamic typists live in their repl. When I use java with IntelliJ I miss my repl. I do gain some things from the IDE, but I feel hamstrung compared to my repl.

I'll give pry a try, but I've tried a lot of dynamic IDE environments and none have come close to IJ w/ statically typed langs.

Re: Static Typing is not enough

#23

Post by carsongross »

jshen wrote: post #18
carsongross wrote: post #14

Earlier quoted context omitted.

Reliable dot completion without some batshit insane state-dependent VM-as-a-dev-env-or-constantly-running-tests system is... well, let's just say made much easier with static typing. I really could give a shit about what people think is "enough" (IMO, keeping stuff simple, as in simplicity of implementation, as in worse-is-better, is the only answer) I just want to hit dot and have a pretty good idea what I'm allowed…

Pry for ruby gives me great dot completion and isn't batshit insane. Most diehard dynamic typists live in their repl. When I use java with IntelliJ I miss my repl. I do gain some things from the IDE, but I feel hamstrung compared to my repl.

Ah, fk man, another REPL?

I don't want a repl for editing. I want to write code in a friggen editor and have dot completion work.

I also want a repl for trying stuff out and debugging/light weight testing, but that's a different use case for me.

Re: Static Typing is not enough

#24

Post by prodigal_erik »

derefr wrote: post #13
roryokane wrote: post #8

Earlier quoted context omitted.

> The post says that. I think the grandparent knew that, and was just repeating what you said to contrast it with his following statement about what static typing is good for. And dot-completion is not completely unique to static languages, but I would say it is “particularly unique” – it is more common for static languages. And that’s not just coincidence – it is generally easier to write a tool like dot-completion…

> dot-completion involves static analysis of the code. Dot-completion involves having a living model of the program loaded in memory . You can do this with any language--static languages just partition the program model such that you get a certain phase of interpretation (compilation) past which you have a completed model of all of the code , without yet having seen any of the data . On the other hand, you can easily…

When you create a method which takes an argument in a dynamic language, there's no declaration of the type of that argument or which methods it will be known to support. So how does dot-completion work for any target other than "this"? The REPL isn't doing whole-program dataflow analysis to infer the only type(s) which could possibly be passed, is it?

Re: Static Typing is not enough

#25

Post by spacemanaki »

carsongross wrote: post #23
jshen wrote: post #18

Earlier quoted context omitted.

Pry for ruby gives me great dot completion and isn't batshit insane. Most diehard dynamic typists live in their repl. When I use java with IntelliJ I miss my repl. I do gain some things from the IDE, but I feel hamstrung compared to my repl.

Ah, f k man, another REPL? I don't want a repl for editing. I want to write code in a friggen editor and have dot completion work. I also want a repl for trying stuff out and debugging/light weight testing, but that's a different use case for me.

> I don't want a repl for editing. I want to write code in a friggen editor and have dot completion work.

I don't either, which is why I use Emacs with something like SLIME or at least inferior-lisp. But I'm sure you've tried this already, and it's not for everyone of course.

I find autocompletion and Intellisense-like features useful, but not really useful enough to make me pick a language based on them. I don't type terribly quickly either, but that doesn't worry me as most of my time is spent debugging and not typing.

Of course static typing does help catch some bugs before you get to debug them, but I think talking about autocomplete and dot-completion is kind of a distraction.

Re: Static Typing is not enough

#26

Post by Dn_Ab »

tikhonj wrote: post #12

Yes, static typing is not enough. Which is why a good statically typed language like Haskell also has great testing facilities. So you don't just write well typed code, but you also write unit tests (HUnit) and property-based tests (QuickCheck). The really neat bit is that static typing actually makes writing tests easier--QuickCheck is much easier to use in Haskell than it would be in some dynamically typed language…

QuickCheck is great and can be found in many languages - dynamic and static alike - nowadays. Another tool that is currently unique to Haskell and is easier to write tests for is Lazy/SmallCheck. SmallCheck shines in the left long tail of failure. Its core idea is based on a powerful principle: "If a program does not fail in any simple case, it hardly ever fails in any case."[]

So SmallCheck works exhaustively to find a minimal counterexample within some depth bound. This makes sense - when trying to characterize a structure for failure (or anything) you can rarely do better than the simplest explanation. However, when the problem lies in larger examples SmallCheck fails where QuickCheck catches a result so something like Type Check -> SmallCheck -> QuickCheck -> probably ok.

[] http://www.cs.york.ac.uk/fp/smallcheck/ documentation

Re: Static Typing is not enough

#27

Post by jerf »

prodigal_erik wrote: post #21
jerf wrote: post #9

Earlier quoted context omitted.

With appropriate compiler flags, you can make up any sort of contracts you like in Haskell. But there's no guarantee that the compilation process will terminate if you do, even putting aside the impenetrability of the resulting code. Haskell is not a general purpose proof assistant, and the typing definitely has limits both practical and theoretical. Abstractly, static types can represent anything, however we (by whi…

Why do people worry about compilers hanging or giving up? If I know how to kill the failed compile and fix my program so that it is provably type-safe before shipping, I don't really care how many undecidable programs could also exist because I no longer have to ship one of those.

Because if the compiler hangs, you don't get any executable code. And in the specific case of Haskell, we are talking about type constraints that are perfectly cromulent, are perfectly correctly expressed and mean something in some abstract mathematical world in which your have infinite compiler time, but in the real world will simply never finish compiling. It's not because you've failed and you can fix it by twiddling something, it's because Haskell is not actually that sort of language, and if you try to actually use the type system as a Turing-complete constraints satisfaction language, you'll get exponential performance... or doubly-exponential performance, or worse, though it stops mattering pretty quickly.

In both theory and practice, this means you can't really use Haskell that way. It's a typed language with the ability to occasionally skirt the limits, ride the line, and dip into a bit of undecidability when useful (and with a real, in-practice risk of it blowing up in your face even so), not a language in which one routinely uses the type system in a "Turing complete manner", if I may be allowed to gloss over precisely what that means. Richer type systems is a topic of ongoing research, but is not a solved problem.

Re: Static Typing is not enough

#28

Post by jshen »

carsongross wrote: post #23
jshen wrote: post #18

Earlier quoted context omitted.

Pry for ruby gives me great dot completion and isn't batshit insane. Most diehard dynamic typists live in their repl. When I use java with IntelliJ I miss my repl. I do gain some things from the IDE, but I feel hamstrung compared to my repl.

Ah, f k man, another REPL? I don't want a repl for editing. I want to write code in a friggen editor and have dot completion work. I also want a repl for trying stuff out and debugging/light weight testing, but that's a different use case for me.

https://github.com/pry/pry/wiki/Editor-integration

Re: Static Typing is not enough

#29

Post by fogus »

modarts wrote: post #10

Yet another attempt to diminish the value of statically typed languages and the benefits that go along with them.

I'm question if you read the post because I didn't diminish anything. I did say that it is a tool in the fight of software validation however.

Re: Static Typing is not enough

#30

Post by prodigal_erik »

jerf wrote: post #27
prodigal_erik wrote: post #21

Earlier quoted context omitted.

Why do people worry about compilers hanging or giving up? If I know how to kill the failed compile and fix my program so that it is provably type-safe before shipping, I don't really care how many undecidable programs could also exist because I no longer have to ship one of those.

Because if the compiler hangs, you don't get any executable code. And in the specific case of Haskell, we are talking about type constraints that are perfectly cromulent, are perfectly correctly expressed and mean something in some abstract mathematical world in which your have infinite compiler time, but in the real world will simply never finish compiling. It's not because you've failed and you can fix it by twiddl…

So the problem is that there are too many useful programs which can't be expressed in a practically decidable form, or there's no clear way to get from a form that isn't to a similar-enough form that would be, like knowing what strategies ghc uses to narrow the search space or something?
Post reply on HN