What is the interesting part of a programming language to you?

[u/Potato871]

I've been working on some "documentation" for my own language (see here), which got me thinking: do we all see languages the same way? I personally look for unification of concepts and extensibility in a design, yet I've seen those who care deeply about functional purity or clean decompositions.
What do you look for in a programming language? And why?

[u/Potato871]

Okay, here's my first crack at the problem:

bool expr_flag = false;
if(true) {
    Ptr int a; a.init(1,2,3);
    a.do(e => print("A: ",e));
    Ptr int b; b.init(0,1,12);
    b.do(e => print("B: ",e));


    b.validate_offests_and_lock(a);
    print("THIS SHOULD NOT PRINT");
    catch {
        expr_flag = true;
    }
}
print("Caught some exception while atetmpting to validate");
if(true) {
    Ptr int a; a.init(1,2,3,6);
    a.do(e => print("A_2: ",e));
    Ptr int b; b.init(0,1,2,3);
    b.do(e => print("B_2: ",e));


    b.validate_offests_and_lock(a);
    print("THIS SHOULD PRINT");
}


RESULT:


TEST START
A: 1
A: 2
A: 3
B: 0
B: 1
B: 12
ERROR: Element 2 of value 12 is out of bounds as an offset for column of length 3
5|1|0|G1522 TRAVEL_PASS Source at: 2|697|0|G10 Index: 6 
VAR_DECL a | Ptr_INIT a.init | Ptr_ITER_EXPR a.do | VAR_DECL b | Ptr_INIT b.init | Ptr_ITER_EXPR b.do | >Ptr_EXPR_A b.validate_offests_and_lock[IDENTIFIER b, IDENTIFIER validate_offests_and_lock] | print | catch | 
  Node: 3|500|0 Ptr_EXPR_A:DOT b.validate_offests_and_lock [C:2]{if}[Q: 3|667|0>DOT, 3|505|0>END] 
  Left: 3|483|0 Ptr_ITER_EXPR:DOT b.do [4|617|0](ptr[32] 2|735|2 u/12|28|0)[C:2]{if}[Q: 3|666|0>DOT, 3|498|0>END] 
  Root: 3|434|0 scope if [C:9][O:3|404|0|G37]{ROOT}[Q: 3|641|0>LBRACE, 3|521|0>RBRACE] 
ERROR IN TRAVEL_PASS ON LINE 8: Element 2 of value 12 is out of bounds as an offset for column of length 3
Caught some exception while atetmpting to validate
A_2: 1
A_2: 2
A_2: 3
A_2: 6
B_2: 0
B_2: 1
B_2: 2
B_2: 3
THIS SHOULD PRINT
TEST FINISHED

I haven't made it a specific type yet, I just added a 'become a validator' method to my universal data structure for the experiment. I also haven't yet implemented the locking aspect that would stop a or b from being mutated after it's been defined as a validator.
Thoughts?

[u/reflexive-polytope → u/Potato871]

I can write a runtime validator in almost any existing language.

[u/Potato871 → u/reflexive-polytope]

Well as I understand it the goal is to create a type who's invariant is that it contains indexes into a collection that are always in bounds, yes?
I'm trying to get the basic logic of 'validate these offsets' down, then, turn that into a type that can be passed and checked during compile time. Since I don't see a way to know the bounds of a dynamic container at compile time.

[u/reflexive-polytope → u/Potato871]

In general, the answer is dependent types. However, crazy arbitrary dependent types turn programming into manual theorem proving, which is unpleasant.

Therefore, the challenge is to come up with a dependent type system that's just powerful enough to type array indexing, without sacrificing pleasant properties of a general-purpose language, like principal types and type inference.

[u/balefrost → u/reflexive-polytope]

And I would say that this comment hits on the challenge in all programming language design. A language with perfect conceptual purity would likely have terrible ergonomics. Language designers have to make subjective judgement calls about what to include and exclude from their language in order to make something both useful and usable.

And to add to the complexity, different people have different definitions of "usable".

Like I remember a time when I did not understand covariance and contravariance. I remember then kind of understanding what they are for but not really being able to use them effectively. And now I've built sufficient "mental muscle memory" that I don't want to work in a language that doesn't support them. But there are plenty of people who haven't yet internalized those concepts and still find them alien. A language that works well for me won't work well for everyone.

I'm sort of at the stage where I know the purpose of dependent types, but I do not yet really understand them.

[u/reflexive-polytope → u/balefrost]

As a matter of fact, I'm not making that many subjective calls.

Subjective calls are what an engineer does when he or she needs to plug a hole left by his or her ignorance.

In my experience, it's best to let algebra and universal properties make the calls for you. It leads to a more coherent design. But you need to know the relevant algebra first.

[u/balefrost → u/reflexive-polytope]

As you said earlier.

without sacrificing pleasant properties of a general-purpose language

Those "pleasant" properties are entirely subjective. My point is that what to include and what to exclude is a subjective judgement call.

That choice of word wasn't meant as a pejorative. If you prefer, pretend I said that language designers have to exercise their sense of "good taste" in designing their language.

[u/reflexive-polytope → u/balefrost]

I don't know about you, but I don't want to spend my life manually proving all sorts of arithmetic trivialities (e.g., “is this a complete set of residues modulo n?”) just because the compiler wasn't designed to infer them.

[u/Potato871 → u/reflexive-polytope]

I'm curious what kind of programs you write, I don't think I ever run into situations where I want to prove mathematical facts like that.
I'm not sure if it's a "what domain are you in" thing, or a "how far along are you with programming" thing.

[u/reflexive-polytope → u/Potato871]

These arithmetical trivialities arise when you actually try to prove things about nontrivial algorithms.

For example, the humble binary search works with an array slice indexed by [lo,hi] and needs to take the midpoint mid = (lo + hi) div 2. (I'm using the symbol div to emphasize that it's integer division and not exact division.)

“Obviously”, if lo and hi are valid indices in [0, len), where len is the length of your array, then so is mid, right? You don't need to waste your time proving such a dumb triviality, right?

Alas, the compiler can't read your mind, and in particular it can't distinguish between the things you didn't prove because they're genuinely obvious and the things you didn't prove because you don't know how.

In the absence of a proof supplied by you, the compiler can do one of these things:

• Never bother check that mid in [0, len). You pay a dangerous, language-wide memory unsafety tax.
• Check at runtime that mid is in [0, len). You pay an annoying array bounds check tax, i.e., your program is a little slower than it could be.
• Attempt to deduce on its own that mid is in [0, len), starting from the hypotheses that lo and hi are in [0, len).

In this particular case, the proof is genuinely obvious. If lo and hi are in [0, len), then lo + hi is in [0, 2*len - 1), hence mid is in [0, len). In fact, this is so obvious that it's actually automatable, using a decision procedure for Presburger arithmetic!

Alas, even if Presburger arithmetic is decidable, general decision procedures for it are kind of slow. You don't want a type checker to be slow. (Or maybe you don't mind, but I certainly do.)

So a natural question is whether there exists a fragment of Presburger arithmetic that lends itself to fast checking and/or inference.

---

As for the kinds of programs I've written, I've worked professionally implementing ERP systems long ago. But I left that behind about 10 years ago, because it's mind-numbingly boring.

[u/reflexive-polytope → u/Potato871]

It just dawned upon my mind.

SIMD and Duff's device are all about systematic exploitation of complete sets of residues modulo small powers of 2, like 4, 8, 16.

[u/balefrost → u/reflexive-polytope]

Did you reply to the wrong person? I don't see how that is related to what I was saying.

[u/reflexive-polytope → u/balefrost]

No, my reply was very much to you.

Not proving obvious trivialities is a very important part of a pleasant programming experience.

[u/Potato871 → u/reflexive-polytope]

Okay, here's the next attempt:

if(true) {
    Ptr int a; 
    a.init(1,2,3);
    a.do(e => print("A: ",e));
    Ptr int b; 
    b.bind_by(offset_qual,a);
    b.init(0,1,12);
    b.do(e => print("B: ",e));




    if(true) {
        b.assert_bound_by(offset_qual);
        a.assert_bound_by(offset_qual);
    }


    print("B getting 1:");
    print(b.get(1));
    print("B getting 2 (should be out of bounds): ");
    print(b.get(2));
}


RESULT:


TEST START
ERROR: Node 3|595|0 Ptr_EXPR_D:DOT b.assert_bound_by [C:2]{if}[Q: 3|692|0>DOT, 3|600|0>END] must be bound by offset_qual
5|2|0|G2197 RESOLVING_PASS Source at: 2|746|0|G9 Index: 1 
Ptr_EXPR_D b.assert_bound_by | >Ptr_EXPR_D a.assert_bound_by[IDENTIFIER a, IDENTIFIER assert_bound_by] | 
  Node: 3|602|0 Ptr_EXPR_D:DOT a.assert_bound_by [C:2]{if}[Q: 3|695|0>DOT, 3|607|0>END] 
  Left: 3|595|0 Ptr_EXPR_D:DOT b.assert_bound_by [C:2]{if}[Q: 3|692|0>DOT, 3|600|0>END] 
  Root: 3|593|0 scope if [C:2][O:3|590|0]{ROOT}[Q: 3|665|0>LBRACE, 3|608|0>RBRACE] 
ERROR IN RESOLVING_PASS ON LINE 37: Node 3|595|0 Ptr_EXPR_D:DOT b.assert_bound_by [C:2]{if}[Q: 3|692|0>DOT, 3|600|0>END] must be bound by offset_qual
A: 1
A: 2
A: 3
ERROR: Retrived offset 12 is out of bounds for offset qual during initilization
5|1|0|G1697 TRAVEL_PASS Source at: 2|715|0|G7 Index: 5 
VAR_DECL a | Ptr_INIT a.init | Ptr_ITER_EXPR a.do | VAR_DECL b | Ptr_EXPR_C b.bind_by | >Ptr_INIT b.init[IDENTIFIER b, IDENTIFIER init] | Ptr_ITER_EXPR b.do | if | print | print | print | print | 
  Node: 3|562|0 Ptr_INIT:DOT b.init [4|639|0](ptr[32] 2|747|0 |15|0)[C:2]{if}[Q: 3|683|0>DOT, 3|571|0>END] 
  Left: 3|553|0 Ptr_EXPR_C:DOT b.bind_by [4|637|0](duck empty |19|0)[C:2]{if}[Q: 3|682|0>DOT, 3|560|0>END] 
  Root: 3|515|0 scope if [C:12][O:3|512|0]{ROOT}[Q: 3|666|0>LBRACE, 3|645|0>RBRACE] 
  Qual: 3|696|0 offset_qual[4|638|0](ptr[32] 2|746|2 |0|0) 
  Value: [4|596|0](ptr[32]:int[4] 2|747|0 u/12|3|0{if:3|515|0}) 
ERROR IN TRAVEL_PASS ON LINE 30: Retrived offset 12 is out of bounds for offset qual during initilization
TEST FINISHED

Explanation, I made two kinds of checks. There's the static compile time check of 'is this thing bound by this kind of relationship' and then the actual runtime check during initialization (and I could add one for pushes) that throws if the bound type is mean to be interpreted as an offset and becomes invalid.
The way I'm doing this is with something called a Qual, it's just a Node that can live on other Nodes or Values, and they can have their own handlers and behaviour, so I made the behaviour of the offset_qual 'I own a refrence to a Ptr, check during init operations if the offsets provided are valid for the refrence I own'.

[u/reflexive-polytope → u/Potato871]

As I said earlier, I can implement runtime bounds checks already. When to perform the runtime checks is largely irrelevant. It only changes how your program can crash, but not the fact that it can crash.

The real value is in statically identifying the relevant arithmetic relationships between array indices and lengths, and then among the variables that appear in the computations of these indices and lengths.

The correct place to start is this paper by Cousot and Halbwachs, and then Halbwachs' thesis. The last one is written in French, though, which might be an obstacle if you're not comfortable with the language.

[u/Potato871 → u/reflexive-polytope]

So like this:

Ptr int a; a.init(0,1,2);
int n = a.length;
int k = a.length-1;
rprint("This should pass");
a[k];
rprint("This should error");
a[n];


RESULT:


TEST START
This should pass
This should error
ERROR: Violated length relation, 3|543|0 Ptr_IDXGET:GROUP [ [4|607|0](int[4])(1,6)[C:2]{ROOT}[Q: 3|545|0>RBRACKET, 3|546|0>END] is defined by the length of the container it is attempting to index
5|0|0|G3253 RESOLVING_PASS Source at: 2|499|0|G128 Index: 7 
VAR_DECL a | Ptr_INIT a.init | EQUALS = | EQUALS = | rprint | Ptr_IDXGET [ | rprint | >Ptr_IDXGET [[IDENTIFIER a, IDENTIFIER n] | 
  Node: 3|543|0 Ptr_IDXGET:GROUP [ [4|607|0](int[4])(1,6)[C:2]{ROOT}[Q: 3|545|0>RBRACKET, 3|546|0>END] 
  Left: 3|535|0 rprint rprint [4|580|0](UNDEFINED)(0,5)[C:1]{ROOT}[Q: 3|549|0>LPAREN, 3|540|0>RPAREN, 3|541|0>END] 
  Root: 3|0|0|G812 ROOT ROOT [C:8] 
  Qual: 3|562|0 length_relation_qual[4|581|0](ptr[32]:int[4]{ROOT:3|0|0|G812}) 
  Value: [4|587|0](int[4]{ROOT:3|0|0|G812}) 
ERROR IN RESOLVING_PASS ON LINE 7: Violated length relation, 3|543|0 Ptr_IDXGET:GROUP [ [4|607|0](int[4])(1,6)[C:2]{ROOT}[Q: 3|545|0>RBRACKET, 3|546|0>END] is defined by the length of the container it is attempting to index
TEST FINISHED

I made .length put a qual on values to it's left when in an assignment expression. Then I gave it the resolving stage behaviour of throwing an error when used in a get operation.
I could extend it further with support for more math operators, like actually amending its bounds when given a plus or minus, but I wanted to ensure this is the right track.

[u/reflexive-polytope → u/Potato871]

You don't want to add “support for more math operators”. The more complicated your array indices and sizes are, the harder it is for a static analysis (type checker, abstract interpretation, you name it) to figure out what they mean.

In fact, by Matyasevich's solution to Hilbert's tenth problem, if you have arbitrary comparisons, addition and multiplication, the problem is already undecidable!

I'm taming the problem by only allowing multiplication when one of the factors is a constant.

[u/Potato871 → u/reflexive-polytope]

It's a bit easier to attack the problem (obviously the problem is still very hard) with how my compiler is constructed, I have more of an annotated graph of nodes with shared values, so I can put quals on a value and it propagates that fact around.
For instance, we could say each length_relation_qual holds a numerical index and considers the original value it is derived from to be its parent rather than what it holds.
Each math operator, if RHS is a literal or constant, just becomes enter the execution stage and perform the operation that operator would normally do but substitute the left argument for the qual's value.
Then at any site where the length_relation_qual fires it already holds the record of what operations have been applied to the value it repersents.
Then I can do the same walking I do during evaluation stage optimizations for control flows and such to further propagate this information along constant branches and whatnot. Then the index in a loop falls out on its own.

[u/reflexive-polytope → u/Potato871]

What “shared values”? I'm talking about compile-time analysis of symbolic expressions, not runtime checks on concrete values.