Yes, I intended both to be integers - but in general they could be anything and the overall idea applies.

The overall idea is to be able to tell the language that an Apple_Count type represents an integer value and some extra meaning that is unique to the Apple_Count type. Additionally we specify that Apple_Counts interact with other Apple_Counts in the same way integers interact with integers, and that the 'unique meaning' of the type always passes through the operation unchanged (I'm sure there's some cool math term for this?).

Meanwhile we don't say how to mix together the 'extra unique meanings' that come with the _Count types, so any attempts to do so lets the compiler know to yell at us, because that's just nonsense according to the rules we provided.

This kind of perspective applies to every single variable in our programs - they all mean something* beyond their basest value to us, even if it's a string for a joke you haven't cleaned up yet. So my desire is to specify all the general kinds of meanings in my programs, and then be able to describe how all of those types of things can and cannot meaningfully interact when transforming the input into the output.

I've been awake and writing this for far too long and am just going off on wild and grandiose tangents, so I'll try to actually be brief. I've been totally convinced by this sort of approach. The problems uncovered are all very 'real' problems. All of them result from some basic incompatibility between the fundamental 'what' and 'how' of your program.

If you want more detail at how this all can (not must by any means, but can) work, I encourage you to look at how Ada handles type derivations (aka derived types). Do be aware Ada also uses the term 'subtype' but in a very different way. An Ada subtype, more or less, specifies a subset of values from a base type.

---

As far as Julia goes, it's been awhile since I looked into it all that much aside from a bit of a refresher this evening. The I believe the overall point is roughly correct, but I don't stand by the details, and neither should you.

Julia has at least a few issues that mean the kind of type safety I really desire is not trivially easy as the language currently exists - at least as far as I know. Unfortunately the ease-of-use of this kind of thing seems to be rather binary - it's either easy or it's hard. Partly I think that's because of how pervasive the concept is. Even a small amount of boiler plate balloons quite severely even for very simple programs.

However some of the problematic aspects of Julia seem like they might have existing solutions. For example the multiple dispatch mechanism is happy to mix and match any and all types, but type parameters provide a high degree of control over what methods are available to match in the first place. These features seem - to me anyway - to be powerful enough to have some serious potential* for making Julia one of the nicest languages to try to bolt all this typing onto after the fact. (Or maybe there's a little too much complexity to allow very nice solutions, and then the sheer number of type interactions drags Julia down to be one of the worst. Who knows!)

But subtypes of concrete types - or rather their lack - seems different. However I'm increasingly reluctant to say much more about this in any kind of useful detail. (Yes, the irony burns.) What was supposed to be a short look to confirm a few things has led me down a massive hole. The size of this hole seems to be increasing the deeper I go, and I think the expansion is accelerating. I've also passed by a few other, possibly equally sized holes along the way... I don't think I'm even that deep, and it's already pretty scary. Although I'm well past the point of firing on all cylinders, I don't think it matters down here, in the dark.

But anyway. My basic thoughts, some or all of which are probably irrelevant to varying degrees depending on how far down the hole/s you've gone.

The very general issue with the lack of concrete subtyping - at least assuming you can get at least something out of it - is that the main alternative appears to probably largely be struct wrapping. That's the closest thing to a concrete statement I have for this section. It's a big, big hole.

Struct wrapping sucks. It really, really sucks. Julia seems to do thing that both make it better and worse than it could be. In terms of making it worse - the lack of abstract composite types (though they seem to have gotten some recent attention!). This seems like it could rule out at least _simple_ methods of making the wrapping process that much nicer. Even if you did make an abstract type to grab all the behavior from the composite type of interest, you'll still need to copy the whole damn struct every single time you want to make a subtype. It might save you from all the forwarding for them all though? Maybe? Maybe not?

Even for non-composite types, any time behavior isn't implemented on an abstract type you may be looking at doing more struct wrapping. A brief glance around the standard library does not show a tendency to restrict the implementation of behavior to abstract types. I don't know if that's a common trend, but I didn't see anything in the main documentation even suggesting you might want to adopt such a practice either. So, probably means quite a fair bit of struct wrapping maybe, I think, unless you want to venture down one of the bigger holes.

Open questions. What the heck does a Union over one type actually do, and is it useful for wrapping things like this? Seems like maybe? But I can't find any mention of anything about it, and after venturing this deep I'm no longer willing to hope I can even begin to actually judge it just by poking at it. Can you shoehorn in parametric types somehow? At some point it feels like you're just going to have to write your own type system though. Primitive parametric types seems promising in principle, but I have a feeling going that route means you might just end up giving up on any code you didn't write yourself. Does "solve" the wrapping problem though...

And then macros. I.. yeah. Macros. Good, evil, both, I don't know anymore. It seems like some aspects of struct wrapping have been made easier to by them to various degrees. In some cases it appears to be better but still probably a bit of work, in others... I don't even know. And how wise is it to even dive this particular hole? I don't know. It's a thing. It might help, some. But something makes me feel only wizards are going to end up saving time this way.

I dunno. I give.

[The below was written earlier, before I had first glimpsed the Holes. Now, well. The pure naivety may be worth a laugh.]
*Wild and rampant speculation warning. I can imagine it may be possible to create a stricter version of the existing type hierarchy that adds subtype equality checks to their methods. Maybe it would even be trivial to convert existing code simply by defining those methods without the subtype checks. Nothing that sounds so good is ever so easy, but hey. This does sound similar to how convert (which itself might be a whole other thing you'd need to tame...) is handled though, so maybe?