4 ms·

> I'd point out though that ML & Haskell's type systems might be simpler from a theoretic stand point, the ugly Java model appears to be easier for humans to re

> I'd point out though that ML & Haskell's type systems might be simpler from a theoretic stand point, the ugly Java model appears to be easier for humans to reason about. It's easy to reason sloppily about anything. It isn't too hard to write ML programs where types are just as uninformative as in Java, but I don't do this because it isn't helpful. > You make it sound like it is trivial to validate those static guarantees in Python. Have you built some trace framework for Python that validates all the types that can be passed to a particular function? That'd be super handy. When I write Python programs, I only care which operations can be used on an object, hopefully without raising an exception. I'm perfectly aware that it's unreasonable to expect more than this. The situation isn't much better in Java. > I wasn't talking about code generation. Me either. > There's a whole bunch of code analysis/interpretation logic that is much harder to achieve in Python. For the most part, the IDE's that support both just provide a watered down Python feature set. I don't care about the questions a language or IDE can answer. I care about the questions I need to ask, which are driven by the problem domain, rather than the capabilities of the language. If they happen to coincide, good for the language and good for the IDE. > You don't have to model that fact as a distinct type in the type system... and people often don't. Often, people implement business logic in code, rather than in the type system... else you couldn't get anything done with JavaScript (which I'm told is not actually the case, despite appearances ;-). You're right, I don't need to model it with types. But if I'm using types, they better be useful for modeling purposes! And if they aren't useful for modeling purposes, they better stay out of the way. > Yup. No composition. Then again, you can handle that logically in other ways. In the case of a TreeMap, the right to handle it would be to have a way to access the Map.Entry associated with a key. Yep, this sounds like the Right Way (tm) to do it, given the constraints. Unfortunately, it's not the path of least resistance. It's the language designer's job to make these two align. > You sort of have that, but it is all around floor/ceiling/range type queries, rather than the get because... well, you rarely need the feature and you can get by with using the containsKey() test. Which is an admission that types aren't helping. > The nice thing is that if I can't remember if get() returns the Map.Entry or just the value, the type system can catch me on it, because the return types are indeed different. In Python, I'd actually have to test it or look at the documentation. Yep, types catch quite a few things in Java. But they don't catch enough things for it to be worth the annotation burden. Crucially, they don't catch `UnsupportedOperationException`. > That's semantics for the same thing as saying the variable can point to any type. That "single static type" can be tied to any Python type, making all variables intrinsically maybes... just like all of Java's reference types. Python variables aren't maybes. Maybe has only two constructors: Just and Nothing. Python expressions are classified by a gigantic sum type that can even be extended with new constructors at runtime. > You can totally know whether you've properly handled all the null cases. Most interesting case analysis aren't of the form null vs. not null. > There's lots of tools that do exactly that, even taking advantage of the @NotNull attribute to help winnow down the possibilities. These tools are cumbersome, workflow-disrupting, and even then, sometimes they still fall short. For example... > For more complex case analyses, you can use Enum's & EnumMap's to know if you have complete coverage. It can be done through static analysis... just not purely from the type system. ... how would I say “list of lists of animals, where each sublist only contains animals of the same species”? (Assuming each species is a separate class.) In Haskell (plus existential quantification, a fairly uncontroversial extension) or OCaml (with GADTs, which subsume existential quantification), this is a breeze. > You're ignoring all the other cases where types do help, because the type system doesn't help with your pet case. Given the ubiquity of case analysis in programming, supporting it in a disciplined way isn't a “pet case”, but rather an everyday necessity. Even dynamic languages offer good facilities for it (Racket, Erlang). > In short, when it comes to static typing, you throw out the baby with the bath water. Nah. I know how to settle for less than what I want. For example, safety leaves a lot to be desired in C++, but it has other nice things to make up for it, like the previously mentioned compile-time dimensional analysis example. > I get it, you don't like it, and it is incredibly annoying looking at that narrow uncanny valley to the thing you do like, but let's not rationalize it by asserting it doesn't help. I love static type systems. That's why I feel insulted when they try to sell me a glorified linter as if it were a type system.

cbsmith 10y ago
> Yep, this sounds like the Right Way (tm) to do it, given the constraints. Unfortunately, it's not the path of least resistance. It's the language designer's job to make these two align. See, I'd argue that in this particular case, it actually is the more correct model of the solution. There are two questions you are looking to answer: is there an entry, and what is the value associated with that entry. One way to solve it is to ask two questions. The other is to get the entry, and if there is one, ask the entry for its value. Using a Maybe of Maybe type creates an unnecessary anonymous type when the entry type is already the natural and correct type. So I'm not sure how it isn't the path of least resistance, but I'll accept that there are better solutions. I find it hard to accept that it is a bad one. I'll completely disagree with the notion that it is the language designer's job to make the two align. Aside from efforts like Brainfuck, programming language design is a series of trade offs, with the general guiding principle of "easy things should be easy, and hard things should be possible". There's plenty of empirical evidence that even getting that right is sufficiently challenging that nobody has really succeeded, but in some few cases they have hit somewhat close approximations. > Yep, types catch quite a few things in Java. But they don't catch enough things for it to be worth the annotation burden. Crucially, they don't catch `UnsupportedOperationException`. They don't catch it, because static types systems like Java's resolve at compile & bind time. You get a "cannot find symbol" error. UnsupportedOperationException can represent failures in circumstances that may literally be unknown/undecidable at compile or bind time. ...and let's be clear about the annotation burden here. It's not that huge of a burden. Typing in type annotations is a very small amount of work, and significantly less work (even if all you counted were keystrokes, it's an easy order of magnitude win) than writing the equivalent validation logic as unit tests. > Python variables aren't maybes. Maybe has only two constructors: Just and Nothing. Python expressions are classified by a gigantic sum type that can even be extended with new constructors at runtime. One can have a language that through inferencing will construct "Just" automagically from any expression that matches the parameterized type (e.g. C++'s optional type); whether you need an explicit constructor is a matter of syntactic sugar and doesn't change the type. Of course variable assignment needn't involve construction at all (e.g. "let a = b"). However, I'd agree that for the most part Python doesn't have polymorphic type. Maybe types are polymorphic types that represent a value or a non-value. However, what I said was that Python variables (which are not types) are intrinsically maybes, which is true. They can be bound to an object of any type, including the NoneType. > ... how would I say “list of lists of animals, where each sublist only contains animals of the same species”? (Assuming each species is a separate class.) I can't imagine a context where I'd create a separate class for each species. Maybe you'd do something like it so you could metaprogram the class system to use an eDSL for defining species. That said, with a few assumptions, there are multiple ways to make what you are describing work. One is with a runtime check: @NotNull List<List<Animal>> x; assert x.stream().allMatch((y) -> (y != null) && (y.stream().map(Animal::getClass).distinct().count() <= 1)); Another would be to create a Species annotation (you might want to check out type annotations in Java, they let you extend the reasoning in the type system quite extensively, and can even survive the dreaded type erasure), which would have the merit of being something that would be well enforced at compile time, bind time, and execution time, whilst providing that eDSL for defining new species. For small lists of species, it would be practical to use CRGP to structure lists with no more than N species, but for longer lists it'd get tedious super fast. Somewhat more realistically, I'd probably do something subtly different from what you are suggesting, using a map of lists rather than your list of lists. I'd be strongly tempted to use an enum (and therefore an enum map) for species instead of classes, but a LinkedHashMap<Class, Species> would have all the useful behaviours of your List of Lists that I would expect one would be looking for. This of course would have some issues (e.g. enforcing that species be leaf classes, allowing two separate lists of the same species), but it'd have the advantage of actually being useful. Far more realistically, you'd implement the whole thing as a database -possibly a graph database- capturing all the various taxonomies around animals & types as well as relationships between animals. Then you'd actually have something useful. > In Haskell (plus existential quantification, a fairly uncontroversial extension) or OCaml (with GADTs, which subsume existential quantification), this is a breeze. Well, I'd say that breeze is mostly hot air. ;-) I have yet to see someone do class per species (for a non-fixed list of species) with Haskell or OCaml (or really any language) in a way that was at all useful. At best you might do something like this to jerry rig an eDSL for defining new Species/Classes. Either way, the type system certain wasn't capturing the complexities of species taxonomies. I find it noteworthy that even in the cases of Haskell & OCaml, you had to go to language extensions, both of which are noted for how they make reasoning about types much more difficult (type inferencing with GADTs is pretty much something you don't do). Even with those extensions, the species logic is way more complex than any computer type system. I have yet to see a Haskell or OCaml program that would use to type system to magically reorganize the lists every time species assignments change or someone finds a new facet to the species problem (of which I believe there are well over twenty to date). Mathematical category theory models don't even accurately represent one of humanity's most significant taxonomic efforts! Such is life. > Given the ubiquity of case analysis in programming, supporting it in a disciplined way isn't a “pet case”, but rather an everyday necessity. There are a specific set of languages with type systems designed for doing case analysis. The entirety of works in those languages doesn't even come close to representing a majority of software based on lines of code, amount of use, people actually writing in them today, or any other reasonable quantification I can imagine. I think that speaks pretty thoroughly about how ubiquitous that particular solution is. There are other practical approaches to case based reasoning that work well enough (in a lot of cases, simple enums and switch statements allow for straightforward static analysis), while allowing the type system to provide all kinds of other useful assistance. > I love static type systems. That's why I feel insulted when they try to sell me a glorified linter as if it were a type system. I'm annoyed by bad type systems too, but I'd not pretend that a linter, let alone a glorified linter, doesn't save me a lot more trouble than it causes.

cbsmith 10y ago

> Yep, this sounds like the Right Way (tm) to do it, given the constraints. Unfortunately, it's not the path of least resistance. It's the language designer's job to make these two align. See, I'd argue that in this particular case, it actually is the more correct model of the solution. There are two questions you are looking to answer: is there an entry, and what is the value associated with that entry. One way to solve it is to ask two questions. The other is to get the entry, and if there is one, ask the entry for its value. Using a Maybe of Maybe type creates an unnecessary anonymous type when the entry type is already the natural and correct type. So I'm not sure how it isn't the path of least resistance, but I'll accept that there are better solutions. I find it hard to accept that it is a bad one. I'll completely disagree with the notion that it is the language designer's job to make the two align. Aside from efforts like Brainfuck, programming language design is a series of trade offs, with the general guiding principle of "easy things should be easy, and hard things should be possible". There's plenty of empirical evidence that even getting that right is sufficiently challenging that nobody has really succeeded, but in some few cases they have hit somewhat close approximations. > Yep, types catch quite a few things in Java. But they don't catch enough things for it to be worth the annotation burden. Crucially, they don't catch `UnsupportedOperationException`. They don't catch it, because static types systems like Java's resolve at compile & bind time. You get a "cannot find symbol" error. UnsupportedOperationException can represent failures in circumstances that may literally be unknown/undecidable at compile or bind time. ...and let's be clear about the annotation burden here. It's not that huge of a burden. Typing in type annotations is a very small amount of work, and significantly less work (even if all you counted were keystrokes, it's an easy order of magnitude win) than writing the equivalent validation logic as unit tests. > Python variables aren't maybes. Maybe has only two constructors: Just and Nothing. Python expressions are classified by a gigantic sum type that can even be extended with new constructors at runtime. One can have a language that through inferencing will construct "Just" automagically from any expression that matches the parameterized type (e.g. C++'s optional type); whether you need an explicit constructor is a matter of syntactic sugar and doesn't change the type. Of course variable assignment needn't involve construction at all (e.g. "let a = b"). However, I'd agree that for the most part Python doesn't have polymorphic type. Maybe types are polymorphic types that represent a value or a non-value. However, what I said was that Python variables (which are not types) are intrinsically maybes, which is true. They can be bound to an object of any type, including the NoneType. > ... how would I say “list of lists of animals, where each sublist only contains animals of the same species”? (Assuming each species is a separate class.) I can't imagine a context where I'd create a separate class for each species. Maybe you'd do something like it so you could metaprogram the class system to use an eDSL for defining species. That said, with a few assumptions, there are multiple ways to make what you are describing work. One is with a runtime check: @NotNull List<List<Animal>> x; assert x.stream().allMatch((y) -> (y != null) && (y.stream().map(Animal::getClass).distinct().count() <= 1)); Another would be to create a Species annotation (you might want to check out type annotations in Java, they let you extend the reasoning in the type system quite extensively, and can even survive the dreaded type erasure), which would have the merit of being something that would be well enforced at compile time, bind time, and execution time, whilst providing that eDSL for defining new species. For small lists of species, it would be practical to use CRGP to structure lists with no more than N species, but for longer lists it'd get tedious super fast. Somewhat more realistically, I'd probably do something subtly different from what you are suggesting, using a map of lists rather than your list of lists. I'd be strongly tempted to use an enum (and therefore an enum map) for species instead of classes, but a LinkedHashMap<Class, Species> would have all the useful behaviours of your List of Lists that I would expect one would be looking for. This of course would have some issues (e.g. enforcing that species be leaf classes, allowing two separate lists of the same species), but it'd have the advantage of actually being useful. Far more realistically, you'd implement the whole thing as a database -possibly a graph database- capturing all the various taxonomies around animals & types as well as relationships between animals. Then you'd actually have something useful. > In Haskell (plus existential quantification, a fairly uncontroversial extension) or OCaml (with GADTs, which subsume existential quantification), this is a breeze. Well, I'd say that breeze is mostly hot air. ;-) I have yet to see someone do class per species (for a non-fixed list of species) with Haskell or OCaml (or really any language) in a way that was at all useful. At best you might do something like this to jerry rig an eDSL for defining new Species/Classes. Either way, the type system certain wasn't capturing the complexities of species taxonomies. I find it noteworthy that even in the cases of Haskell & OCaml, you had to go to language extensions, both of which are noted for how they make reasoning about types much more difficult (type inferencing with GADTs is pretty much something you don't do). Even with those extensions, the species logic is way more complex than any computer type system. I have yet to see a Haskell or OCaml program that would use to type system to magically reorganize the lists every time species assignments change or someone finds a new facet to the species problem (of which I believe there are well over twenty to date). Mathematical category theory models don't even accurately represent one of humanity's most significant taxonomic efforts! Such is life. > Given the ubiquity of case analysis in programming, supporting it in a disciplined way isn't a “pet case”, but rather an everyday necessity. There are a specific set of languages with type systems designed for doing case analysis. The entirety of works in those languages doesn't even come close to representing a majority of software based on lines of code, amount of use, people actually writing in them today, or any other reasonable quantification I can imagine. I think that speaks pretty thoroughly about how ubiquitous that particular solution is. There are other practical approaches to case based reasoning that work well enough (in a lot of cases, simple enums and switch statements allow for straightforward static analysis), while allowing the type system to provide all kinds of other useful assistance. > I love static type systems. That's why I feel insulted when they try to sell me a glorified linter as if it were a type system. I'm annoyed by bad type systems too, but I'd not pretend that a linter, let alone a glorified linter, doesn't save me a lot more trouble than it causes.