Inductive Constructors prevent use of certain variable names

[mariari]

inductive Foo {
  foo : Nat -> Foo;
}

bar : {A : Type} -> A -> A;
bar foo := foo;

with the error message

The constructor foo should have 1 argument, but has been given 0

Ideally the variable should win here, it's also related to

bar : {A : Type} -> Foo A -> A;
bar (foo foo) := foo;

Note that functions are punned so if I made a function foo it would not error this way. Meaning there is a difference between inductive functions and functions precedence wise

[janmasrovira]

I feel like this is in general acceptable or even desirable.
I have the following considerations:

1. We know at the scoping stage whether it's a variable or a constructor, thus making the implementation much simpler. If we want the variable name to win I guess that we would need to defer the resolution until arity checking.
2. I would be very confused to find a constructor name on the left hand side of a function and not be a constructor.

[mariari]

Thank you for quickly responding, forgive me for my long winded response!

For me, the dissonance comes in when it comes to resolution rules. Namely functions and constructors resolves differently for naming, which means code breaks upon certain kinds of refactoring and that the type digest of a file does not give the full meaning in resolution.

Let us consider optimization and refactoring of a data type.

say we have a point module

module foo;

open import Prelude;
open import Data.Nat;
open import Complex;

-- here we use a natural representation
inductive Point {
  xy-point : ℕ -> ℕ -> Point;
};

-- Alias for xy-point, for shorthand
point : ℕ -> ℕ -> Point;
point ≔ xy-point;

end;

Say after we make this Point module, we end up making a Complex Module.

module Complex;

open import Prelude;
open import Data.Nat;

inductive ℂ {
  complex : ℕ -> ℕ -> ℂ;
};

real-part : ℂ -> ℕ;
real-part (complex real imaginary) ≔ real;

imaginary-part : ℂ -> ℕ;
imaginary-part (complex real imaginary) ≔ imaginary;

imaginary : ℕ -> ℂ;
imaginary imaginary ≔ complex zero imaginary;

real : ℕ -> ℂ;
real nat ≔ complex zero nat;

to-real : ℂ -> ℕ;
to-real comp ≔ real-part comp + imaginary-part comp;

end;

Thus we also add in Point

from-complex : ℂ -> Point;
from-complex comp ≔
  point (real-part comp) (imaginary-part comp);

Great. However say for our model of points, it actually more natural to do all of our algorithms on a complex number (it isn't in this specific example, but you can see how future code may be a more natural representation of code often.).

However since other rely on us, we want to maintain API compatability.

module foo;

open import Prelude;
open import Data.Nat;
open import Complex;

-- we now decide to change the represnetation of Point, keeping the
-- API the same
inductive Point {
  from-complex : ℂ -> Point;
};

xy-point : ℕ -> ℕ -> Point;
xy-point x y ≔ from-complex (complex x y);

point : ℕ -> ℕ -> Point;
point ≔ xy-point;

end;

So, we end up with this representation, so that the digest of the module is the same

from-complex : ℂ -> Point;
xy-point : ℕ -> ℕ -> Point;
point : ℕ -> ℕ -> Point;

however, we may now break user code, as if they have open import Point, and happen to use from-complex as any variable name in the language, then the new representation breaks their code.

This example is a bit contrived, namely in that from-complex is unlikely to be a variable name. However let us consider my alias example

point : ℕ -> ℕ -> Point;
xy-point : ℕ -> ℕ -> Point;

both have the same type according to minijuvix.

Which one is the constructor? Say we came up with this order and people started to use our code like

from-point : Point -> BusinessData; 
from-point point ≔ ...;

but internally we do not know this, and we decide that "well we mostly use the point alias, let's just make it the constructor and plan to depreciate xy-point", and thus commit the following code

-- here we use a natural representation
inductive Point {
  point : ℕ -> ℕ -> Point;
};

-- DEPRECATED
xy-point : ℕ -> ℕ -> Point;
xy-point ≔ point;

Now we have broken their code, as although our type digest is the same, which one is the constructor is different, breaking code upon an innocent looking change.

What makes this rough, is constructors like nil would still break it even if 1. was implemented, since this would not be possible to fix the scoping rule for such a case, as there is overlapping intent of what things mean, meaning that bringing in constructors with no arguments into scope breaks the bijection between the consturctor syntax and how resolution works for everything else.

[mariari]

I ended up sampling the following ML's for behavior

1. Agda
2. Idris
3. F*
4. Haskell
5. OCaml

F*, Haskell, and OCaml allow only upper case constructors, and lower case pattern variables.

Idris and Agda are more interesting examples.

For Idris, Idris allows only lower case pattern variables. Thus the following is not admissible

foo : Nat -> Nat
foo BAR = BAR

What is interesting however, is that constructors can be lower case, see the following code

https://github.com/mariari/Misc-ML-Scripts/blob/master/Idris/resolution.idr

In here the compiler gives me the following warnings

- + Errors (2)
 |-- resolution.idr line 8 col 6:
 |   Resolution.z has a name which may be implicitly bound.
 |   This is likely to lead to problems!
 `-- resolution.idr line 9 col 6:
     Resolution.s has a name which may be implicitly bound.
     This is likely to lead to problems!

However the REPL boots up fine.

Idris implies that functions and constructors are very similar to the degree where they share the same namespace, and syntax in the language (gadt syntax mimics type signatures!). This makes sense from a practical perspective, as someone using your code as a library is likely does not care about implementation details to this level. Carrying with the theme, constructors with 0 arguments lose to local variables for the same reason. This implication allows us a few things:

• We can swap out the representation of the data type in the future when we find performance issues.
  • Haskell's Data.Sequence give out custom constructors so that we can assume the naive representation when thinking about behavior.
• For libraries not centered around data structures (socket libraries, etc.), we can make certain functions that are apart of the API, as constructors then later deprecate or change the internals
  • If patterns constructors and functions weren't the same, we may have some resolution issues on users who use our code here.

Looking back at the posted file we can see that foo and foo' are the same even though they happen to have variable names that overlap with constructors.

(The contriveness of my examples make it look more confusing than it is, I am sorry!)

Agda works in the same way as MiniJuvix. Since constructors are tied to patterns in the language, functions and constructors have subtle differences in resolution and can cause issues in refactoring.

Although the argument here is focused on constructors vs functions, the real issue is the resolution of pattern forms vs non pattern forms, as the issue would arise with functions that we can declare pattern forms for.

Namely that by binding some name x to a pattern form, we can not use the variable x in any module where this shows up as it would be resolved to the pattern form x and not the local variable x.

Idris and Prolog both handle this ambiguity in similar ways.

Idris states that upper case can not be pattern variables, and thus it has to be some pattern form, thus we can have patterns with zero arguments this way.

Prolog states that Upper case variables are Pattern Variables, and that lower case values are not objects to be unified.

?- a = a.
  yes
?- a = b.
  no
?- a = X.
  X = a
  yes
?- [a,b,c] = [X|Y]
x = a
Y = [b,c]

[janmasrovira]

That's a very nice insight, thanks for taking the time to explore and write all of this.
As you've highlighted, there is no perfect approach, but we have decided to handle it in a similar way to Agda since it is what we prefer. We prefere it mostly because:

1. we don't want to have lexical restrictions on constructors (i.e. first letter is a capital letter).
2. We want resolution of names to be solved during scoping. Note that this is different from Agda. In Agda you can have multiple constructors with the same name and the name gets fully resolved during type checking.
3. Constructor names should take priority over variables in patterns.