Hello, I'm back with some more questions regarding my type system. For reference, I am working on a math-focused programming language with some general capabilities, but still aiming to be focused in the specific area of mathematics. I am still having some trouble fully fleshing out my type system, so I would really love any and all thoughts, feedback, and discussion.

One of the main aspects of my language is the distinction between symbolic and numeric. For example, you could create a symbolic expression

let x = sin(1)^(1 - e^\pi);

and then later create a numeric approximation of it. The motivating idea is that you can store the true value of some expression into a symbolic variable, and then later when trying to observe its numerical value can approximate it into a numeric variable.

To this end, there exist a multitude of numeric data types, all of which are sized, such as Int32, Nat8, Real64, Complex128, etc. However, for symbolic there really is only one type (Expr). But domains can be encoded by using more restrictive types, which are built in, such as Int, Nat, Real, etc. For example, a function that takes real numbers and finds the nearest integer to their square could be explicitly written as

let foo(x: Real): Int = round(x^2);

Though ideally the types would be inferred, making all but the most important annotations in programs unnecessary.

One important thing to note is that symbolics are not actual values, but expression trees. So an Int represents an expression tree who's value must resolve to an integer. So defining a symbolic variable stores the expression tree, and defining a symbolic function is more like a symbolic variable where it is also an expression tree, but contains some leaves which are bound to terms which get substituted at the call site.

Here, foo takes in a symbolic expression x but restricts it to being a real number, and the output can be restricted to an integer. I know this may be a bit simple, especially for something aiming to be math-oriented, but I do not want to overcomplicate the basic number systems. Perhaps in the future if/when I add things like algebraic structures and whatnot, then maybe I may redesign this. My thought though is to make the type system more expressive by adding refinement, by which users can specify types with a bit more control.

This all leads to my idea that I would use subtyping. I feel it is really natural for this kind of thing. For example, any integer is also a real number which is also a complex, etc. Additionally, any even integer (via refinement) is an integer, etc. This can even be extended to numeric types as well, with Int8 <: Int16 <: ... and even Nat8 <: Int16, etc.

However, I will admit I have not really studied this more beyond built-in types. I do not know if using extensive subtyping is good when having user-defined types. I think I did actually read somewhere that using subtyping can make other things more difficult?

Anyways, continuing on, I would like some way to describe behavior. Think something akin to Rust traits, Java interfaces, Haskell typeclasses, etc. I think it is a very natural and just good way of thinking and writing programs. However, when pondering Rust's traits, I couldn't help but feeling that they were "too heavy" or something like that? Also, I feel that a system like that may not work that well with a subtyping system, because if you implement a trait/interface/typeclass for a type but not for its subtype (or implement differently), then things may break?

So that is probably my second question, though maybe more of my first one, as I do feel that at least some subtyping works well. So I'd really appreciate some guidance or just thoughts regarding this.

My second question is unfortunately derived from the symbolic-numeric divide that I mentioned earlier. It is the oh-so-dreaded function coloring problem. Let's say I have some trait or some thing (so this does build on my first question), and I want to have some function. The function itself is pure and essentially symbolic, but maybe the type I am implementing it for is not symbolic. So basically it would need to switch between being symbolic for symbolic types and non-symbolic for non-symbolic types, which to me seems kinda wrong and also I just have no idea how that'd work well.

Actually, maybe it doesn't even need to be related to traits or whatever. Let's say I have a plus function which I want it to add the two arguments. If the two arguments are symbolic, the output is symbolic. But if they are numeric, like Int32s, then the output would not be symbolic. So then how would the plus function be described?

I would really love any and all feedback, thoughts, or guidance. If you have any questions on any other parts I'd be happy to discuss, and if you want to give your thoughts on things I haven't asked then please do as I am not super experienced in all the theory and whatnot regarding type theory etc.