I'm working on a programming language. I'd like to have your feedback: So... PL Design:

We have functions and types (I'd like to define functions in terms of types but so far I have no idea how to do this because functions define the () operator and that's a operator definition in a type definition)

Types can be parameterized by other types and values:

Matrix<3,2> for example

this is also possible in c++ but the parameter values have to be compile time constants 
I want to also allow bindings to runtime constants.

readonly int a = Int.Parse(System.Console.ReadLine());
readonly int b = Int.Parse(System.Console.ReadLine());

Matrix<a,b>;


Matrix<3,2> a;
Matrix<2,4> b;
These 2 matrices can be multiplied like : a * b which results in a Matrix<3,4>;

Matrix<a,b> c;
Matrix<b,a> d;

These 2 can also be compiled which result in Matrix<a,a>;

What about this case?

readonly int a = Int.Parse(System.Console.ReadLine());
readonly int b = Int.Parse(System.Console.ReadLine());
readonly int c = Int.Parse(System.Console.ReadLine());
readonly int d = Int.Parse(System.Console.ReadLine());

Matrix<a,b> e;
Matrix<c,d> f;

I can only multiply if b and c are the same. How do I check this? Do I check this? Does the * - Func check this?

Option 1: Pattern matching and cast

I could ask if Matrix<a,b> is Matrix<a,c> like this:

if(e is Matrix<a,c> newE)
{
    ...
}


This works like the C# version of the 'is' - operator. It checks for a valid cast and copies the result into a new variable, in this case 'newE'
Now I can multiply newE by f;

Overall it seems a bit wasteful since copying Matrix<?,?> is probably lots of work.
How to fix this? Well,...
Idea 1: check if 'b' is 'c' instead. 

if(b is c)
{
    ...
}

The compiler should know that within the if-true-block b is equal to c and should simply allow e * f to happen.
This does seem to need a new compiler primitive that I have not really thought about yet (instantiating proofs like Lean and Idris).


Idea 2: 
Why even copy 'e' and make a new variable 'newE'? 
If Matrix<a,b> and Matrix<a,c> are indeed the same type (when b is equal to c) then it should be safe to retype 'e' simply as Matrix<a,c>.

if(e as Matrix<a,c>)
{
    //typeof(e) in this block here is Matrix<a,c>
    ... 
}

This here really depends on a very strict form of equality. Equality is easy when it comes to built in stuff for primitives but this is a user defined world. Does it make sense to constrain type parameterizations to primitives and special record types with built in equality?
Does the compiler just predefine equality? Is there a way to do this via conversions instead?


How would the other side look like? 

type Matrix<int a,int b>
{
    ...   
    public static Matrix<a,c> operator*<int c>(Matrix<a,b> m1, Matrix<b,c> m2)
    {
        ...
    }
}

There's an implicit constraint here with 'b' being the second parameter of 'm1' but also the first of 'm2'.

Another idea:


type Matrix<int a, int b>
{
    ...
    public static Matrix<a,c> operator*<EqualTo<b> c>(Matrix<a,b> m1, Matrix<c,d> m2)
    {
        ...
    }
}

Here EqualTo constitutes a refinement - type of int.
A refinement type is a type based on another type combined with a predicate.
A refinement type constraints the value space of the base class.


type EqualTo<int k> : constr int
{
    //Not sure how to do this tho.. should be usable in an if statement
    public static EqualTo? operator is(int p)
    {
        if(p != k) return null;
        return new this();
    }
}

We can also define interface types like this:
type IArithmetic : constr Type
{
    private Type WrappedType;
    public static IArithmetic? operator is(Type tp)
    {
        bool hasAddOperator = tp.GetMember("operator+",...) != null;
        bool hasSubOperator = tp.GetMember("operator-",...) != null;
        ....
        if(hasAddOperator && hasSubOperator && ...)
        {
            return new this(tp);
        }
    }

    //We can then even generate custom bindings
    public static WrappedType operator+(WrappedType a, WrappedType b)
    {
        var m = WrappedType.GetMember("operator+") as Func<WrappedType,WrappedType,WrappedType>
        return m(a,b);
    }
}

Then you can use IArithmetic just like a normal type

static void DoSmthStuff<IArithmetic T>(T someValue)
{
    ...
}


The type refinement concept requires compile time function execution to work of course.






var k = System.Console.WriteLine;
var d = MyNamespace.WriteLine;

var m = System<Windows>.Console;
var n = System.Console;


struct S<T>
{
    static void T GetT()
    {
        ...
    }
}


var m1 = S<int>.GetT;
typeof(m1) => Func<int>
var m2 = S<>.GetT;
typeof(m2) => Func<>
m2<int>();

nameof(k) => "WriteLine";
nameof(d) => "WriteLine";