No notion of scope · Elpi users & devs

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.

Kazuhiko Sakaguchi (Jun 29 2021 at 16:16):

You can use pi and sigma to quantify variables. Does this answer your question?

Kazuhiko Sakaguchi (Jun 29 2021 at 16:20):

https://github.com/LPCIC/coq-elpi/blob/23345e95657b71f98dd6e4cd1941764018937490/examples/tutorial_elpi_lang.v#L857-L874

Enzo Crance (Jun 29 2021 at 16:23):

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).

Kazuhiko Sakaguchi (Jun 29 2021 at 16:24):

I mean, does this work?:

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

Kazuhiko Sakaguchi (Jun 29 2021 at 16:26):

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

Enzo Crance (Jun 29 2021 at 16:26):

Your snippet does work. So sigma makes it explicit that the variable is free from any previous context.

Kazuhiko Sakaguchi (Jun 29 2021 at 16:34):

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.)

Kazuhiko Sakaguchi (Jun 29 2021 at 16:40):

Also, IIUC, all the free variables in a top-level declaration pred Args :- ... are implicitly quantified by pi.

Enrico Tassi (Jun 29 2021 at 17:02):

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: Apr 20 2024 at 08:02 UTC

Stream: Elpi users & devs

Topic: No notion of scope

Enzo Crance (Jun 29 2021 at 16:14):