5 ms·

With languages like Haskell you can lift many types of logic errors into the realm of type errors.

by mej10 11y ago

cle 11y ago
At what cost? What are the tradeoffs? (this is a question I'm genuinely curious about)
- 15155 11y ago
  > At what cost? Directly related to the typechecker? Non-incremental (cold) compile times.
- nickbauman 11y ago
  Defining those types and the rules of their interaction with a greater type system is also cognitive load you must do up front. In most cases, we must develop systems with incomplete knowledge and must show some progress before all the rules are defined. So you will be changing a lot more code as you learn more than you would in a dynamically typed system.
  - dllthomas 11y ago
    In my experience, this is not the case. In my current project, I am parsing and analyzing a dialect of SQL. As you say, "we must develop systems with incomplete knowledge". Had it been necessary that I get my rules right up front, there would be tremendous pain - the documentation is inconsistent, incomplete, and incorrect. Tremendous agreement there. This is no case for foregoing types. In order to write code we must be defining expectations of how our system works. Even ideally loosely coupled, code depends on the behavior of other code. When we learn that a given interface is no longer going to work, we need to find and change everywhere that relied on that interface. Working in Haskell I was able to sketch out a preliminary and incomplete set of rules; as I found them not to work I could change them - with tremendous assistance in finding exactly the points that needed to change in tandem. Working in Python earlier this year, much smaller changes to much simpler code has been substantially more painful.
    - tome 11y ago
      > In my experience, this is not the case. Not my experience either. We commonly hear the refrain "Haskell does not allow you to do exploratory programming". Personally I prefer exploratory programming in Haskell to any other language.
- phamilton 11y ago
  There's usually a cost to runtime inspection and metaprogramming. In order to guarantee things at compile time they must not be possible at runtime. Languages are getting better at type inference, but things like JSON parsing are more rigid and explicit. It just feels jobbish at times.
- ridiculous_fish 11y ago
  I have a Python script runs as both Python 2 and Python 3, using runtime checks to determine which methods to call. This sort of thing is much harder in Haskell. A more ambitious example: imagine the web with JavaScript replaced by Haskell. Your code compiles and typechecks in your browser, but that doesn't guarantee that it will do the same in mine, or a different version of yours, or tomorrow's new browser. So these static type guarantees are very weak because they only apply to a single runtime environment. The less control you have over the runtime environment, the more important dynamic typechecks become. You can also have static type checking, but you have to be prepared for the fact that your static types will be different at runtime. This property confounds most languages with static type systems, including Haskell.
  - guiraldelli 11y ago
    > A more ambitious example: imagine the web with JavaScript replaced by Haskell. Your code compiles and typechecks in your browser, but that doesn't guarantee that it will do the same in mine, or a different version of yours, or tomorrow's new browser. So these static type guarantees are very weak because they only apply to a single runtime environment. Wait... What? Are you saying that natural numbers in South America in 1990 century is different from natural numbers in Europe 2010? So how can types be different depending on browsers? Of course, if the browser implements a "compiler" that doesn't follow the basic principles reported in the standard of the language, it'll happen. If some joker wants to call `Int` a `String`, problems will happen. Otherwise, it is not true.
    - nickbauman 11y ago
      Ah, that's right. Everyone implements the compiler spec the same way every time, because we live in a perfect world.
pron 11y ago
Basically yes. The question is what exactly it buys you. In general, the proving power of Haskell's type system is that of a finite-state-machine/regular expression (i.e. you can verify behavior of an FSM), and the proving power of Idris is that of a full Turing Machine, but in general we know that verifying a program property has a lower complexity bound of Ω(# of program states), i.e. exponential in the size of the source code, regardless of the language used (actually, the more expressive the language, the harder the problem becomes, but just by a bit). The question is, then, given that all approaches are bound by the same complexity bounds for complete proof, which approach is cheaper in practice based on property type, program type and required confidence? Sadly, we don't have the answer to that question, but answering it would require some expensive empirical studies.

With languages like Haskell you can lift many types of logic errors into the realm of type errors.

by mej10 11y ago

With languages like Haskell you can lift many types of logic errors into the realm of type errors.

cle 11y ago

At what cost? What are the tradeoffs? (this is a question I'm genuinely curious about)

15155 11y ago
> At what cost? Directly related to the typechecker? Non-incremental (cold) compile times.
nickbauman 11y ago
Defining those types and the rules of their interaction with a greater type system is also cognitive load you must do up front. In most cases, we must develop systems with incomplete knowledge and must show some progress before all the rules are defined. So you will be changing a lot more code as you learn more than you would in a dynamically typed system.
- dllthomas 11y ago
  In my experience, this is not the case. In my current project, I am parsing and analyzing a dialect of SQL. As you say, "we must develop systems with incomplete knowledge". Had it been necessary that I get my rules right up front, there would be tremendous pain - the documentation is inconsistent, incomplete, and incorrect. Tremendous agreement there. This is no case for foregoing types. In order to write code we must be defining expectations of how our system works. Even ideally loosely coupled, code depends on the behavior of other code. When we learn that a given interface is no longer going to work, we need to find and change everywhere that relied on that interface. Working in Haskell I was able to sketch out a preliminary and incomplete set of rules; as I found them not to work I could change them - with tremendous assistance in finding exactly the points that needed to change in tandem. Working in Python earlier this year, much smaller changes to much simpler code has been substantially more painful.
  - tome 11y ago
    > In my experience, this is not the case. Not my experience either. We commonly hear the refrain "Haskell does not allow you to do exploratory programming". Personally I prefer exploratory programming in Haskell to any other language.
phamilton 11y ago
There's usually a cost to runtime inspection and metaprogramming. In order to guarantee things at compile time they must not be possible at runtime. Languages are getting better at type inference, but things like JSON parsing are more rigid and explicit. It just feels jobbish at times.
ridiculous_fish 11y ago
I have a Python script runs as both Python 2 and Python 3, using runtime checks to determine which methods to call. This sort of thing is much harder in Haskell. A more ambitious example: imagine the web with JavaScript replaced by Haskell. Your code compiles and typechecks in your browser, but that doesn't guarantee that it will do the same in mine, or a different version of yours, or tomorrow's new browser. So these static type guarantees are very weak because they only apply to a single runtime environment. The less control you have over the runtime environment, the more important dynamic typechecks become. You can also have static type checking, but you have to be prepared for the fact that your static types will be different at runtime. This property confounds most languages with static type systems, including Haskell.
- guiraldelli 11y ago
  > A more ambitious example: imagine the web with JavaScript replaced by Haskell. Your code compiles and typechecks in your browser, but that doesn't guarantee that it will do the same in mine, or a different version of yours, or tomorrow's new browser. So these static type guarantees are very weak because they only apply to a single runtime environment. Wait... What? Are you saying that natural numbers in South America in 1990 century is different from natural numbers in Europe 2010? So how can types be different depending on browsers? Of course, if the browser implements a "compiler" that doesn't follow the basic principles reported in the standard of the language, it'll happen. If some joker wants to call `Int` a `String`, problems will happen. Otherwise, it is not true.
  - nickbauman 11y ago
    Ah, that's right. Everyone implements the compiler spec the same way every time, because we live in a perfect world.

pron 11y ago

Basically yes. The question is what exactly it buys you. In general, the proving power of Haskell's type system is that of a finite-state-machine/regular expression (i.e. you can verify behavior of an FSM), and the proving power of Idris is that of a full Turing Machine, but in general we know that verifying a program property has a lower complexity bound of Ω(# of program states), i.e. exponential in the size of the source code, regardless of the language used (actually, the more expressive the language, the harder the problem becomes, but just by a bit). The question is, then, given that all approaches are bound by the same complexity bounds for complete proof, which approach is cheaper in practice based on property type, program type and required confidence? Sadly, we don't have the answer to that question, but answering it would require some expensive empirical studies.