5 ms·

Just a technical point that hints at a significant philosophical idea: The asymptote cannot reach 100% of program behavior in any finitary way. That would solve

Just a technical point that hints at a significant philosophical idea: The asymptote cannot reach 100% of program behavior in any finitary way. That would solve the halting problem. The x-axis should go off to infinity. Also, it's not a smooth progression. There are huge jumps in expressivity involved here. Going from Java-style types to Hindley-Milner to full System F are all massive jumps in expressivity. There are also incompatible features of type theories. Type theories are a fractal of utility and complexity. A type system doesn't only describe the behavior of the program you write. It also informs you of how to write a program that does what you want. That's why functional programming pairs so well with static typing, and in my opinion why typed functional languages are gaining more traction than lisp. How many ways are there to do something in lisp? Pose a feature request to 10 lispers and they'll come back with 11 macros. God knows how those macros compose together. On the other hand, once you have a good abstraction in ML or Haskell it's probably adhering to some simple, composable idea which can be reused again and again. In lisp, it's not so easy. A static type system that's typing an inexpressive programming construct is kind of a pain because it just gets in the way of whatever simple thing you're trying to do. A powerful programming construct without a type system is difficult to compose because the user will have to understand its dynamics with no help from the compiler and no logical framework in which to reason about the construct. So, a static type system should be molded to fit the power of what it's typing. The fact that every Go programmer I talk to has something to say about their company's boilerplate factory for getting around the lack of generics tells me something. This is only a matter of taste to a point. In mathematics there are a vast possibility of abstract concepts that could be studied, but very few are. It's because there's some difficult to grasp idea of what is good, natural mathematics. The same is in programming: there are a panoply of programming constructs that could be devised, but only some of them are worth investigating. Furthermore, for every programming construct you can think of there's only going to be a relatively small set of natural type systems for it in the whole space of possible type systems. Generics are a natural type system for interfaces. The idea that interfaces can be abstracted over certain constituents is powerful even if your compiler doesn't support it. If it doesn't, it just means that you have to write your own automated tools for working with generics. It's not pretty.

tom_mellior 9y ago
> The asymptote cannot reach 100% of program behavior in any finitary way. That would solve the halting problem. There are languages that enforce termination. They only accept programs that can be shown to terminate through syntactic reasoning (e.g., when processing lists, you only recurse on the tail), or where you can prove termination by other means. Coq is like this, as is Isabelle, as is F* , as are others. They also provide different kinds of escape hatches if you really want non-terminating things, like processing infinite streams. This "we can never be sure of anything, because the halting problem" meme is getting boring. Yes, you cannot write the Collatz function in Coq. No, that is not a limitation in the real world.
- hwayne 9y ago
  > This "we can never be sure of anything, because the halting problem" meme is getting boring. Yes, you cannot write the Collatz function in Coq. No, that is not a limitation in the real world. How about, say, a video game? That's something where we reasonably _want_ it to not terminate, because we're primarily interested in its side effects.
  - tom_mellior 9y ago
    That's what the escape hatches are for. In Coq, for instance, you can also write functions processing infinite streams, provided that they also produce something regularly. For example, in a game, you could write a function from an infinite stream of inputs to an infinite stream of frame updates. You can not write functions that would not terminate while computing the updates for some given frame. Alternatively, you just write a function to iterate your game world update N times, where you choose N large enough to ensure that your game can run until the heat death of the universe. That's not a nonterminating function, but it's long-running enough for all practical purposes.
- danharaj 9y ago
  I'm aware of strongly normalizing systems and the escape hatch of coinductive programming. But when we're talking about the space of all programs, the fundamental limit of incompleteness is important. How else do we judge the merit of a type system except by seeing how it fits into the overall space of computable processes? There are two ways to see type systems. In the first way you construct terms along with their types, this is called Church style. In the second way, the terms exist before their types and you use types to describe their behavior, this is called Curry style. In particular take System F. In Church style the terms of System F come with their types. In Curry style we see System F types as a way to describe the behavior of untyped lambda terms. I used to think Church style was more important but lately I've been more partial to Curry style. Programs exist before you type them, type systems tell you how they behave. They also tell you how to construct programs but this is subordinate to the more fundamental descriptive capacity.

tom_mellior 9y ago

> The asymptote cannot reach 100% of program behavior in any finitary way. That would solve the halting problem. There are languages that enforce termination. They only accept programs that can be shown to terminate through syntactic reasoning (e.g., when processing lists, you only recurse on the tail), or where you can prove termination by other means. Coq is like this, as is Isabelle, as is F* , as are others. They also provide different kinds of escape hatches if you really want non-terminating things, like processing infinite streams. This "we can never be sure of anything, because the halting problem" meme is getting boring. Yes, you cannot write the Collatz function in Coq. No, that is not a limitation in the real world.

hwayne 9y ago
> This "we can never be sure of anything, because the halting problem" meme is getting boring. Yes, you cannot write the Collatz function in Coq. No, that is not a limitation in the real world. How about, say, a video game? That's something where we reasonably _want_ it to not terminate, because we're primarily interested in its side effects.
- tom_mellior 9y ago
  That's what the escape hatches are for. In Coq, for instance, you can also write functions processing infinite streams, provided that they also produce something regularly. For example, in a game, you could write a function from an infinite stream of inputs to an infinite stream of frame updates. You can not write functions that would not terminate while computing the updates for some given frame. Alternatively, you just write a function to iterate your game world update N times, where you choose N large enough to ensure that your game can run until the heat death of the universe. That's not a nonterminating function, but it's long-running enough for all practical purposes.
danharaj 9y ago
I'm aware of strongly normalizing systems and the escape hatch of coinductive programming. But when we're talking about the space of all programs, the fundamental limit of incompleteness is important. How else do we judge the merit of a type system except by seeing how it fits into the overall space of computable processes? There are two ways to see type systems. In the first way you construct terms along with their types, this is called Church style. In the second way, the terms exist before their types and you use types to describe their behavior, this is called Curry style. In particular take System F. In Church style the terms of System F come with their types. In Curry style we see System F types as a way to describe the behavior of untyped lambda terms. I used to think Church style was more important but lately I've been more partial to Curry style. Programs exist before you type them, type systems tell you how they behave. They also tell you how to construct programs but this is subordinate to the more fundamental descriptive capacity.