I'm not sure what the idea even means, or if it really warrants a separate paradigm than OOP. Is it related to category theory? Frustrated that a 'new' paradigm got dropped on me with only a couple sentences of explanation.

It's bogus, they just wanted to use the word "category" to try and lure in FP enthusiasts.

It's not a bogus! We are FP enthusiasts and the word "category" has really strong connections to our type system. However, the name might be a little misleading so we've already changed it. Anyway, we treat our types as categories. For example 1 belongs to a singleton category 1 (thus you can write 1 :: 1) but it also belongs to category of positive numbers or all numbers in general, thus again you can write (1 :: 1 :: Nat :: Int :: Num :: *). I hope you see now connections to category theory. However the name itself, as I noted above, could be misleading so we need to change it.

That's just plain-old dependent typing, isn't it? What's in this and not in, say, Idris, such that you can say that it's a whole new paradigm?

1 also belongs to 'all integers from 1 through 10'. Is this also a category? (I assume yes). How is this category expressed in Luna?

Yes it is, `1 :: 1 | .. | 10`. The pipe combines categories, so you can as well write `1 :: 1|2|3|4|5|6|7|8|9|10`. Both of the forms are however not yet supported in the main branch of official compiler and will not be supported during the first release yet.

I wouldn’t say it’s bogus, and there definitely wasn’t any malicious intention behind it, it’s just that finding a name for such a property is super difficult. As I’ve written above, it’s about having fine-grained control over the data (object) constructors. It turns out most words synonymous to “type”, “kind”, “category” etc. (as understood in the wide sense) are already taken by mathematical / programming concepts. We will, however, change the name, as it causes way too much confusion :).

And you know that because?

This feature is a bit of a misnomer, as it immediately brings up discussions about category theory. That being said, the idea behind it is pretty simple, yet powerful. Our typechecker will be able to track the shape of data on a deeper level than usual types. Basically will be tracking the exact constructors used to construct data, not just types – something that is a huge pain in most existing typed languages. If you for example take Haskell, you can have a data type with multiple different constructors, and even though you may be certain that some of those are impossible to occur at some points in your program, it is difficult to express that certainty on typelevel – other than repacking to a different datatype, with less constructors, which then need to be named differently and need repacking even if you're just calling a function that expects a wider range of constructors, and thus is definitely safe. However, due to the amount of work with more foundational layers of the language, we've had to postpone implementing this feature until further down the line. It is coming at some point for sure, though :)

That sounds like a horribly leaky abstraction if you mean that you're literally going to statically track the call stack to attempt to verify invariants. Hopefully it's just a misunderstanding on my part.

This sounds a bit like Idris with its dependent types.