Stream: Elpi users & devs

Topic: Unification variables as name in type

Luko van der Maas (Oct 06 2023 at 10:03):

I noticed while writing Elpi code that it is possible to write code like this

kind foo type.
type X int -> foo.
type Y Z -> foo.

without Elpi Typecheck. giving any errors. Is there a reason for this, or is it a bug? If there is a use case I would be very interested to see how it would work, as I can't find any that do anything.

Luko van der Maas (Oct 06 2023 at 10:04):

Or is it simply a capital letter name that you then can't use anywhere anymore?

Enzo Crance (Oct 06 2023 at 12:31):

Hello. IIUC the value Z here is an Elpi variable in the type. You are in fact creating a polymorphic constructor Y for foo that takes any value and returns a foo.

Enzo Crance (Oct 06 2023 at 12:32):

kind list type -> type.
type nil A -> list A.
type cons A -> list A -> list A.

Does that help?

Luko van der Maas (Oct 06 2023 at 13:40):

When I try to use either X or Y in a later piece of code it doesn't work as they are interpreted as unification variables, not constructors of foo. It happens because they are capital letters I think. That was what my question was mostly about, sorry for formulating it badly. But I do see now how the Z would work.

Luko van der Maas (Oct 06 2023 at 13:42):

Also the vscode syntax highlighting doesn't work anymore at that point, so it feels like a weird edge case.

Luko van der Maas (Oct 06 2023 at 13:42):

image.png

Paolo Giarrusso (Oct 06 2023 at 17:01):

@Enzo Crance I'm surprised, I'd also expect a unification variable rather than polymorphism — can you build a list int and a list string with those constructors?

Paolo Giarrusso (Oct 06 2023 at 17:03):

@Luko van der Maas yeah everything uppercase is a unification variable, I'm surprised that's accepted for the "thing to type"... Maybe it could force the variable and its solutions to have that type?

Enrico Tassi (Oct 06 2023 at 17:46):

It is a bug

Enrico Tassi (Oct 06 2023 at 17:47):

The type checker is a really simple piece of code, and here the parser is too permissive

Last updated: Oct 13 2024 at 01:02 UTC