Add Typing Environments

[jakzale]

Adding typing environemnts

• Add type environments to type checker,
• Update existing tests,
• Update progToString to generate ext keywords,
• Add scoping rules for for loops.
• add a Program section specifying all ext variables.
• Update API freeVars to extVars,
  these are not the free variables that you are looking for.
• Test for loops scopes
  At the moment there is no test case for for loop shadowing an ext variable.

[jakzale]

This should fix some problems with #76, but it doesnt have assignments yet.

[effectfully]

This should fix some problems with #76

I thought that problem is already fixed? The problem was that we were renaming programs with loops and we were implicitly assuming that a loop always evaluates at least once, so every variable bound in the loop body gets introduced into the scope. But that was a false assumption, so we removed loops from the typed language. No loops in the typed language = no scoping problems.

There's still ambiguity in the untyped language, but that doesn't matter, at the moment at least.

but it doesnt have assignments yet.

What do you mean by assignments?

[jakzale]

I thought that problem is already fixed? The problem was that we were renaming programs with loops and we were implicitly assuming that a loop always evaluates at least once, so every variable bound in the loop body gets introduced into the scope. But that was a false assumption, so we removed loops from the typed language. No loops in the typed language = no scoping problems.

Now we have proper scoping rules for for loops, meaning that the discussion for the value of the for loop variable is moot, as the following program is ill typed

for i = 1 to 10 do end;
assert i == 10;

There's still ambiguity in the untyped language, but that doesn't matter, at the moment at least.

What sort of ambiguity you refer to?

What do you mean by assignments?

Since we add a scope for the for loop, the following programs are ill typed

for i = 1 to 10 do
  assert j > 0;
  let j = i * 2;
end;

and

for i = 1 to 10 do
  let j = i * 2;
end;
assert j == 20;

Furthermore, the last assertion in the following program will be true

let j = 0;
for i = 1 to 1 do
  let j = i;
end;
assert j == 0;

I want to add an assignment operator to modify a variable without adding a new binding, which would make the following program's assertion true

let j = 0;
for i = 1 to 1 do
  j <- i;
end;
assert j == 1;

[effectfully]

What sort of ambiguity you refer to?

I misunderstood what you're after.

I've responded in the Loops issue.

[effectfully]

This doesn't look right. The point of MonadScope was to assign the same unique to all variables that share a name. Regardless of whether those variables are distinct or not. That logic doesn't work for mapping untyped variables to typed ones as here we need to track scopes properly.

In particular,

let x = 0;
let x = 1;
assert x == 1;

now elaborates to the wrong

let x_0 = 0;
let x_1 = 1;
assert x_0 == 1;

which is obscured by the fact that we recover the correct scoping in the renamer.

This suggests that we should have two kinds of golden tests: the program that we get right after type checking and the program that we get after renaming. Unless I'm wrong, it'll show that we now do weird things in the type checker.

[effectfully]

which is obscured by the fact that we recover the correct scoping in the renamer.

Hm, I looked into the renamer and I don't think it can recover scoping. I'm really confused now, how is this whole thing working? Golden tests suggest that we do have correct scoping, but looking at the code I don't see how that can possibly be the case. Can we have a unit test with

let x = 0;
let x = 1;
assert x == 1;

where we only type check things and don't rename them?

[effectfully]

Oh, I think I see what's going on. So taking

let x = 0;
let x = 1;
assert x == 1;

we call

checkStatement (R.ELet var m) kont =
    case uniOfVar . R.unVar $ var of
        Some uni -> do
                tM <- T.withKnownUni uni $ checkExpr m
                withVar var $ \ tVar -> kont [T.ELet (UniVar uni tVar) tM]

over the first and then the second let, so we extend the initially empty environment first, but then we don't extend it and instead use the already existing binding. So the program elaborates to

let x_0 = 0;
let x_0 = 1;
assert x_0 == 1;

which then gets renamed correctly.

I'm not entirely sure if it should be causing us any problems right now, but it certainly will in future. For example, we'll need to inline the value of a loop variable and if the loop variable has the same name than some previously referenced variable, then we can't just use the value of that variable, we have to actually update the environment instead of reusing the existing entry that just became shadowed. Or in future we may have stuff like

let x = T;
let x = 1;
assert x == 1;

and here we also need to update the environment and can't reuse the existing entry, because the type of the new binding differs from the type of the old one.

[jakzale]

Ok, this actually gave me slight headache as well, because there are two notions of environment conflated into one:

• tracking which uniques are assigned to which identifier, and
• tracking which variables are in scope.

I do not think that untangling them together should be an issue.

Explanation

1. I refactored withVar to pass the typed version of the variable to the continuation in order to encapsulate the process of changing from R.Var to T.Var.
2. To keep the old behaviour of giving the same unique to the same identifier, we use a Map R.Var T.Var to track which uniques are assigned to which identifiers.
3. We reuse the same map to track which variables are in scope.
4. As variables are intrinsically typed, we use the name of variable to infer its type/uni.

Once we switch to extrinsically-typed variables, we will probably need to:

• Use a different map for tracking which uniques have been assigned (Map (R.Var, Uni) T.Var)
• Use a proper typing environment, which similar to Map R.Var (T.Var, Uni).

[effectfully]

Previously we had this:

tracking which uniques are assigned to which identifier, and

and not this:

tracking which variables are in scope.

Now that we have the latter and given that I can always get the list of external variables of a program, I don't think we need the former anymore. So once we switch to extrinsically-typed variables I propose to only have Map R.Var (T.Var, Uni) (or Map R.Var T.UniVar for that matter).

Or do you have a use case for Map (R.Var, Uni) T.Var?

[jakzale]

Or do you have a use case for Map (R.Var, Uni) T.Var?
Not really.

Given that we relax our requirement for uniques, maybe we should parameterise the typed ast by the type of variable as well. Personally I would like to work without uniques and supply. Especially, since we will perform a renaming step in the compiler anyways.

[effectfully]

This still does not look right.

Why do we need the

    case Map.lookup var tyEnv of
        Just tVar -> kont tVar

part? We needed this kind of logic previously, but I'm currently failing to see why we need it now.

What happens if we remove that and do

            tVar <- freshVar . R.unVar $ var
            local (Map.insert var tVar) $ kont tVar

(the Nothing case) unconditionally?

[jakzale]

Is this something that we're going to have in the long run? If the plan is to inline the value of a loop variable, then we can unscope the loop variable after the loop (and only inline in the body of the loop then).

Hmm, I need to think about it. Yes, we could technically inline the loop variable and erase it completely. I am still not sure how to do it properly, as there are programs in the spec that depend on variables bound in the body of a for loop. Lemme think about it for a bit.

[effectfully]

I am still not sure how to do it properly, as there are programs in the
spec that depend on variables bound in the body of a for loop.

Why is that a problem?

for i = 0 to 1 do
  let x = i;
assert x == 1;

will elaborate to

let x = 0;
let x = 1;
assert x == 1;

[jakzale]

Hmm, maybe I am overdoing it.

[effectfully]

This still does not look right.

Why do we need the

    case Map.lookup var tyEnv of
        Just tVar -> kont tVar

part? We needed this kind of logic previously, but I'm currently failing to see why we need it now.

What happens if we remove that and do

            tVar <- freshVar . R.unVar $ var
            local (Map.insert var tVar) $ kont tVar

(the Nothing case) unconditionally?

[jakzale]

Ah yes, we can do that, then we do not need to do renaming in type checking.