I just wrote https://lobste.rs/s/6gzmym/static_types_are_dangerously#c_9lzbuq A couple of crazy ideas on types: 1. The Right Way is for product types to be nominative and sum types to be structural. 2. Maybe we need tags for product types as well? Then unify types on the names not of types but of their constituent tags, whether sums or products. e.g.

Foo

and

Bar

can be automatically coerced in:

type Foo = A int * B boolean
type Bar = A int * B boolean

My newish take on types in PLs is that they're all at the wrong level of abstraction. ADTs don't get it right either. We don't want to model types (which containerized the information, and overspecify the proximity of values), we want to model the information in some other normal form (kinda like 6NF in relational). Then separately we may want to define memory layout types (views on the normal form) that are materialized. The 'domain model' should only affect the normal form. The practical and optimization concerns should only affect the materialized views. https://twitter.com/chatur_shalabh/status/1201989863660122112 https://twitter.com/BrandonBloom/status/1202001092248141824

Why do ADTs not satisfy your criteria? The classic example of an ADT on Wikipedia is the integers: https://en.wikipedia.org/wiki/Abstract_data_type. Are you saying that including relations between 1 and 2 in the type is over-specific? There's certainly a large state space here, and it's been done to death on LtU 😛. For example, I could generalize from my previous comment to unification between two types (or type and value, or two values) stemming from some combination of: a) the type name b) the set of members c) the set of methods For example, Java unification (just classes) requires the name to match, which indirectly requires a superset of members and methods. Go unification (interfaces) requires just superset of methods. OCaml (I think?) is the same as Go. I'm sure lots of niche languages have explored other points in this state space. But really all this gets deep into architecture astronaut territory. There's a lot of wisdom in the idea to ignore inheritance in favor of composition. The use case I use to ground my uses of types is: what is the minimum we need to add to Hindley-Milner (basically structs and tagged unions) to avoid the NASA Mars Orbiter disaster? Basically assigning units to numbers. The nice thing about this use case is that it requires balancing usability with correctness. Nobody's going to create a unique struct for every numeric use case in their program. (And the long saga of

signed

vs

unsigned

in C shows that this path has correctness problems as well.) So yeah, there are rarefied use cases where you want to distinguish between interface+relations and a materialized view. But it seems excessive to require that two-level framework all the time. @Edward de Jong / Beads Project has units, if I recall correctly. Have you written up a description anywhere of Beads's type system?

@shalabh "We don't want to model types (which containerized the information, and overspecify the proximity of values), we want to model the information in some other normal form (kinda like 6NF in relational)."

I think there are "functional" and "relational" styles of programming, which are appropriate in different contexts. In my project (Curv), there is currently no state. It is purely functional. You build up geometric shapes using function composition: applying shape operators to shape values. The functional style is focussed on values, which containerize information and force it to be hierarchical. But, this style works really well in Curv. @Kartik Agaram Integers & arithmetic are another example where functional style works well. The functional style, with its containerized, hierarchical data, seems to be bad for modelling "real world" data, with its non-hierarchical relationships, and seems to be bad for managing state in game programming. For that, you want "relational" programming, which is what I think is what Shalabh is talking about. I'm using this term loosely to describe Entity Component Systems, Datalog, etc.

My take on this: types are fine, it's type systems that are a problem. All type systems I know impose a single type structure on "everything", typically meaning "a program", which is a somewhat arbitrarily defined subsystem of a computing system. Every type system I have seen is great for some use cases and horrible for others. So either we need to find the one type system that's good for everything, or admit that we need different type systems and find a way to make them collaborate.

ADTs don't really work because record types do not satisfy my criteria. It's the

car.wheels

vs

wheel.car

problem. In the information model there is only one relationship between the car and the wheels. (This goes back to the domain types vs machine types discussion we had at some point.) In something like RDF, or any graph model there is only one (obvious) way to model the car-wheel relationship: there's a car, there's a wheel, there's a 1:many relationship between car and wheels. When using record types, you have to partition the information into two records - now you must decide where the link goes. This is what I mean by the 'relationship should be outside the entity' but it is inside in records. Sometimes I might want to lookup the car for a given wheel. Now I have a few options: Loop over all the cars and see if they contain this wheel, construct a reverse mapping using a new data structure

Dict[Wheel, Car]

. If you do that and it's somewhat long lived, you now have to keep the data consistent. The point is your code is not written to fit the domain model but it is written to fit this type model that contains various projections of the domain model. Importantly these projections are manually constructed and maintained. Other concerns (such as optimization) might lead to decisions like lets keep both

car.wheels

and

wheel.car

because we need fast lookup in both directions.

This is actually an interesting case and way easier in a dependently typed language. Why? Because if you add two measurements with different units, the return value type isn't obvious, and likely the result type is only known at runtime (aka you're likely passing types as values). The approach that keeps rows of each unit until you "flatten" it out to a single unit is a good one too, though clearly keeps more around than flattening (and disregarding rounding error you should be able to store everything as one unit). Fun times though: in this example, time affects the conversion rate between currencies, so it almost could be seen as 3-dimenensional (amount, currency, and time of conversion)