Dependent typing considered unreadable

Actually, this is a complaint I have with most functional languages too, but I figured I may as well ask for the sky. This seems to be almost entirely a function of historical path dependence, rather than any deliberate optimization.

For the record, my favorite language syntax of all time belongs to C#, with Javascript (ES6+) coming in at a close second. Python would do in a pinch, too. Obviously none of them have the type system I want, but there's no reason in principle that you couldn't have both nice syntax and a good type system.

Scala occupies an awkard halfway point on both counts: it starts out maybe 70% as readable as Java and rapidly descends as soon as you start doing anything interesting with it. It also forces you to engage in tedious hackery to get an approximation of the functionality that something like Idris would provide out of the box, and you still can't get all the way there.

I know that the trade-off with readability is brevity - C# lately has had me feeling the boilerplate blues - but the option would certainly be nice.

Something like this would be really nice:

                
    var r = new Record[] { //... };

    constraint NonZeroInt<int>(int val)
    {
        val != 0;
    }
                
            

Then, to avoid a compile-time error (because what kind of language would let you divide by something that might evaluate to 0?), you'll need to write:

                
    int numerator = r.Sum();
    int denominator = r.Length;
    decimal avgValue = denominator is 
                    | NonZeroInt => numerator/denominator;
                    | int => 0;
                
            

But, of course, the right way to do it would be to guarantee that the list's length satisfies the NonZeroInt type constraint:

                
    constraint NonEmptyList<T>(T t) where T : IEnumerable
    {
        t.Length != 0;
    }

    var r = new NonEmptyList<Record>(){ //This has to have at least one record! };
                
            

Then you can just write this instead:

                
    int numerator = r.Sum();
    NonZeroInt denominator = r.Length;
    decimal avgValue = numerator/denominator;
                
            

This way, you don't have the unexpected behavior of returning something that might be mistaken for a valid result. You'd need to write something to handle the case where you have 0 records (EmptyList, anyone?), of course.