> 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 ther

> 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. Your alternative is very much an object-oriented, I'd even say English-noun-oriented, answer. From a value-oriented perspective, which I reckon is more useful, returning the key alongside with the value is useful when the user doesn't know the key in the first place (e.g., if your query is of the form “get the greatest entry whose key is less than the supplied argument”), but not otherwise. > 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. Querying a specific key and getting (Maybe) the associated value is concise and to the point. Anything that introduces additional ceremony is a little annoyance that will compound with others found along the way. > 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". If ruling out errors when fetching entries from maps is “hard”, we're all screwed. > 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. Well, I find that ML and related languages have succeeded. They force me to answer the important questions early enough: What's the logical structure of the data? To what extent can this structure be mechanically enforced? Can this concept be split into smaller, simpler ones? Do these concepts have enough in common to treat them as instances of a single, more general concept? Which implementation details of this abstraction should I hide from users? > ...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, I'm not talking about the keystroke count. More important for me is how densely packed information is. Communicating with less symbols saves time (for the reader!) and space (for the reader!). > 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. Unit tests are also a pretty dumb technology, invented by the abstraction-challenged for the abstraction-challenged. Why should I manually craft two test cases in thirty minutes, when a computer can generate thousands in less than a minute? > 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. I'm not talking about surface syntax. `Maybe` is an inductive type, and thus it's characterized by an induction principle. > However, I'd agree that for the most part Python doesn't have polymorphic type. How can it have polymorphic types when it only has one! > Maybe types are polymorphic types that represent a value or a non-value. `Nothing` is very much a value. It can be put inside `Just`, for example. > 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. The induction principle for `Maybe` can't be soundly applied to Python variables, ergo, Python variables aren't “maybes”. > That said, with a few assumptions, there are multiple ways to make what you are describing work. One is with a runtime check: (...) This could destroy the asymptotic time complexity of the original program, so it's not good. > 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, At this point, you're taking the Lisper's route of compiling custom DSLs into your language of choice. However, Lisp implementations (or, even better, Racket!) have the necessary tools to make this a pleasant process, like the ability to test macro expansions in a REPL (or, even better, syntax-parse!). > and can even survive the dreaded type erasure), FWIW, I don't see anything wrong with 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. I don't care much for runtime enforcement. What's a program supposed to do if it runs into a situation that can only be explained by programmer error? Fix itself? > 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. My solution lets me make one list where dogs come before cats, and another where cats come before dogs. Or even a list with two sublists of cats, one of which comes before dogs, the other after. Yours does not. See? Java isn't a very good language for accurate modeling! > 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. Databases are good for storing large collections of mostly unordered facts. (Although they may be queried in a specific order.) OTOH, lists are intrinsically ordered. You'd have fared much better if you had asked me “What do you need this list 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. I never explicitly asked for a DSL for defining species - why should I use a DSL when plain classes are good enough? What I asked for is a data structure with a more sophisticated invariant than Java can normally enforce. > 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. It was just a toy example. I have more realistic examples of typeful programming, e.g., to statically enforce invariants of data structures. (Type-aligned sequences, heaps, search trees, etc.) > 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). GADTs basically give you two things: existential quantification and intensional type equality constraints in constructors. Only the latter, which my example doesn't use, causes problems for type inference. > 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). I'm perfectly aware that not everything can be modeled typefully in Haskell, let alone ML. But, again, have you tried asking me what I need this data structure for? > Mathematical category theory models don't even accurately represent one of humanity's most significant taxonomic efforts! Such is life. Who said anything about category theory? I'm talking about accurately modeling whatever situation one's confronted with. Logical precision is far from exclusive to category theory, even if category theory has an impressive track record at accurately classifying all sorts of abstract structures. > 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. An unpopular but correct solution is better than no solution at all. Branching on `boolean`s and hopefully remembering the correct meaning of `true` and `false` on a per case basis doesn't scale. And inheritance is too open-ended to help with exhaustiveness checks. > 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. In Java itself, or with external tools? And where are the exhaustiveness checks?