Hi. I have noticed that if you define a variable in a block (say, in a branch of an `if`

construct), it will be given a type by the elpi typechecker, but if the same variable is defined elsewhere, in the same predicate but in another block that "should" be considered semantically distinct from the first one, then the variable in that second block must have the same type as the one given by the typechecker at the first encounter. It means the typing context is kept all the time while typing a predicate, and there is no notion of scope. Is that a common way to go in Prolog-based languages? Are there theoretical reasons for this? I am interested. Thanks for your answers.

You can use `pi`

and `sigma`

to quantify variables. Does this answer your question?

This does not typecheck whereas it should perfectly work IMHO.

```
mypred T :-
if (T = {{ nat }}) (
G = 2,
coq.say G
) (
G = "x",
coq.say G
).
```

That is why I was asking if there was a theoretical reason not to represent any block logic (like a builtin `if`

with that kind of separation).

I mean, does this work?:

```
mypred T :-
if (T = {{ nat }}) (sigma G\
G = 2,
coq.say G
) (sigma G\
G = "x",
coq.say G
).
```

But I often forget to put explicit quantifications and then have to debug it. This is an issue for me.

Your snippet does work. So `sigma`

makes it explicit that the variable is free from any previous context.

I think that reading `sigma G`

as a quantifier `∃ G`

is the natural way to understand it. Contrarily, `pi`

corresponds to forall. (But @Enrico Tassi may explain it better.)

Also, IIUC, all the free variables in a top-level declaration `pred Args :- ...`

are implicitly quantified by `pi`

.

Yes, you are right.

Anyway, I would not recommend using the same variable name with two types/meanings, since it may not help the reader.

Last updated: Jun 06 2023 at 23:01 UTC