Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Using generics to enforce valid structure at compile time

Tags:

c#

types

generics

By abusing the type system in c#, I can create code, where the compiler will enforce a rule, to ensure an impossible operation is not performed. In the below code, its specific to matrix multiplication.

Obviously the below is totally impractical/wrong, but are there reasons we cant have something like this in c# in the future, where I could define a type like Matrix<2,2> and have the compiler ensure safety?

Also, does anything like this exist in any mainstream languages? I'd suspect something like this might be possible with metaprogramming in C++??

public abstract class MatrixDimension { }

public class One : MatrixDimension { }
public class Two : MatrixDimension { }
public class Three : MatrixDimension { }

public class Matrix<TRow, TCol>
    where TRow : MatrixDimension
    where TCol : MatrixDimension
{

// matrix mult. rule. N×M * M×P  = N×P 
    public Matrix<TRow, T_RHSCol> Mult<T_RHSCol>(Matrix<TCol, T_RHSCol> rhs)
        where T_RHSCol : MatrixDimension
    { return null;}
}

public class TwoByTwo : Matrix<Two, Two> { }

public void Main()
{
    var twoByTwo = new Matrix<Two, Two>();
    var oneByTwo = new Matrix<One, Two>();
    var twoByThree = new Matrix<Two, Three>();
    var threeByTwo = new Matrix<Three, Two>();
    var _twoByTwo = new TwoByTwo();

    var _2x2 = twoByTwo.Mult(twoByTwo);
    var _1x2 = oneByTwo.Mult(twoByTwo);
    var _3x3 = twoByThree.Mult(threeByTwo);

    var _2x2_ = _twoByTwo.Mult(twoByTwo);

    var invalid = twoByThree.Mult(twoByThree); // compile fails, as expected
}
like image 438
jasper Avatar asked Jun 23 '12 00:06

jasper


1 Answers

F# has support for units of measure built into the language - basically creating a richer type system on top of the CLR types, like what you've started doing with generics.

A different, and I would argue complementary, approach to building a richer type system (which I'm using in my own software to ensure high reliability and correctness in the core modules) is to use the compiler in conjunction with a theorem prover to guarantee that pre- and post-conditions on methods and properties (as well as class invariants) are met.

This is well-known in mainstream languages like SPARKAda and Java (via JML extensions) - and it's available for C# as well, thanks to Microsoft Research's work on the Code Contracts feature. (Which I'm making heavy use of. I highly recommend watching the videos linked on the MSR page, they're the best way to get started with these tools.)

The cccheck static checker from MSR can run in the background of Visual Studio, and will give you error and informational messages along with (I think purple) squigglies in your code editor.

If you want to go down that route, check out the Code Contracts MSDN forum for support - that's where most users seem to hang out.

like image 77
Lars Kemmann Avatar answered Oct 13 '22 22:10

Lars Kemmann