One Way to Represent Things

  -- ogf(c,x) = Σ n:ℕ, cₙ xⁿ
  def ogf (c : ℕ → ℕ) (α : Type) :=
  Σ n:ℕ, fin (c n) × (fin n → α)

For example list has coefficients Cn = {1,1,1,1...}

  inductive list (α : Type)
  | nil : list
  | cons (hd : α) (tl : list) : list

  inductive bin_tree (α : Type)
  | leaf : bin_tree
  | branch (x : α) (left : bin_tree) (right : bin_tree) : bin_tree

Computing those coefficients from a type definition is not always trivial though (see the symbolic method http://algo.inria.fr/flajolet/Publications/AnaCombi/book.pdf).

This can be extended to infinite data structures too by switching the natural numbers to ordinal numbers in the ogf definition.

Choosing a canonical representative is not feasible in the general case, so yes one would need to prove that every operation respects the equivalence relation.

The other alternative is to emulate sum types through run-time type information or using code generation like protobuf. I also fail to see how these approaches are simpler or more maintainable.

Sum types are not a panacea for all software development ills, but they're the simplest and most direct solution to a concrete problem: My data is either this type or that type.

Analogously, Rust or F# have type systems which allow you to build the Option type yourself easily: there is no magic behind them, and you can just write down whatever sum type you want. Similarly, we want to be able to build arbitrary quotient types (not just of numbers, but of general sets with equivalence relations) ourselves.

I'm a bit skeptical, but, xarray's demos are very impressive. They do all kinds of geospatial modeling on ocean salinity, ozone, etc, and the data model seems general enough to create beautiful plots automatically (for various reasons, but mostly because of what you were saying in your post: simplicity enforced by constraints).

I'd love your thoughts on xarray, since it was such a serendipitous discovery in relation to your post. (If you're not impressed with xarray, then that's probably a useful signal that perhaps it's a step in the wrong direction on the ladder of complexity.) But either way, thanks for reminding me that "the solution is elegance, not a battalion of special cases."

The answer is, they aren't the same concept. In English, we may look at multiple implementations and say "hey, those are all an 'image'", but in reality, each of these is a distinct concept:

A representation of the image meant for manipulation by pixel, such as for a 2d image editor.

A representation of the internal structure of the image format, such as giving access to the PNG or JPG frames.

The raw bytes of the specific serialization, such as for shipping around a network.

Representations of the image in a display context, such as the display driver might use.

Representation of the image from the point of view of metadata, such as a file explorer may need.

Representation of an image from the point of view of editing, where it may be disassembled into frames or layers for later reconstruction after applying edits, such as Photoshop may use.

You can't create an "image" class/package/library that will fit all those needs, to say nothing of the ways those needs may interact with other things (i.e. I may need metadata for that file explorer that includes non-images as well, even there are image-specific elements to it like a thumbnail).

Moreover, the lack of connectivity between this sort of object isn't even my top 25 programming problems... I'm almost always several layers composed on top of these sorts of things anyhow with my own local data concerns. Even if I've got an "image" I've also got a ton of other things with it that nothing else can be expected to understand (like which user this is a avatar for or where the image came from or any number of other things).

It's sometimes annoying to deal with too many color types or something, but that's a local concern for an ecosystem, not a universal problem a general-purpose language should be spending valuable design budget trying to dictate. (DSLs can, if appropriate, precisely because they are domain-specific languages.)

Colors:

    (r{0.0-255.0}, g{0.0-255.0}, b{0.0-255.0}, a{0.0-255.0})

    { red = r{0.0-1.0}, green = g{0.0-1.0}, blue={0.0-1.0}, opacity = o{0.0-1.0} }

Or geopoint:

    (lat, lng)

    (lng, lat)

When consensus is reached, things settle down - so most new languages give you associative arrays out of the box. On the other hand, there was a time when exceptions seemed to be the consensus on runtime error handling, but there has been some rethinking on that...

Then there is APL, which seems to exemplify what you are asking for. It is very well-regarded by those who get it, but it seems to have been just too difficult (or alien) for most of the engineers whose purpose it addresses.

Haskell may not be the best example to make a case from, as it is still, to a large extent, an experimental language. Spreadsheets are also something of an outlier, as they are a system of data manipulation already developed before it was practical to computerize them.

In certain designed 2D/3D languages you can have N parsers that start and end in different places in any direction, potentially even in a random order depending upon the language.

Unix shell is an unstructured text environment. Data loses all semantic context the moment it's pushed to stdout, and thus every program that wants to interact with it needs to have its own, half-baked, buggy parser included. This is wasteful and a source of many maintenance and security problems.

Whereas in an Object Oriented language you would access the elements by calling a method myArray.at(123). The benefit is you don't need to know how that data is stored or where.

In OOP the elements of an Array of course can be Arrays too, whose elements you can similarly only access via a method-call.

In Smalltalk even the 'nil' meaning no object at all is an Object.

The "formal side" assumes a static environment, but our OS and apps and browsers are constantly churning. When the runtime reality diverges from the compile-time model, you'll want dynamicism: can this object do that? What happens if I try to invoke an unsupported operation? etc.