Stream: Elpi users & devs

Topic: No notion of scope


view this post on Zulip Enzo Crance (Jun 29 2021 at 16:14):

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.

view this post on Zulip Kazuhiko Sakaguchi (Jun 29 2021 at 16:16):

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

view this post on Zulip Kazuhiko Sakaguchi (Jun 29 2021 at 16:20):

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

view this post on Zulip 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).

view this post on Zulip 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
  ).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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: Feb 05 2023 at 14:02 UTC