Open RandomActsOfGrammar opened 3 years ago
Sorry for the long delay with this. I think this is an interesting issue with polymorphism that I remember discussing with Andrew, Gopalan, Yuting the last time I was in Minneapolis. I believe at that point I was convinced that we would need some kind of range restriction for type arguments. However, Yuting ended up implementing a version without the restriction. Maybe this is explained in the paper Yuting and Gopalan wrote about schematic polymorphism?
Ping @yvting, @gnadathur97.
Given a definition, the type variables in its type are schematic over its entire body. Such a schematic definition represents an infinite set of definitions obtained by instantiating the type variables with ground types.
The example above can be restated as follows where the scope of type variables is made explicit:
Define hideType [A] : A -> typeHider -> prop by
hideType X (typeHider_c X).
Here, the type variable A ranges over a single clause. Note that in the current implementation we implicitly derive schematic type variables from types and do not allow this form of definitions. This can be changed if people think the explicit syntax will improve readability.
With regards to the example, I do not see any ill-typed code. Once hideType
is defined, it may be freely used in other schematic definitions as long as its occurrences are well-typed. This is the case for the occurrence of hideType
in hideHelper
which has a type instance aty -> typeHider -> prop
.
Also notice that the constant typeHider_c
has different type instances in hideType
and hiderHelper
. The former is A -> typeHider
(this A
is the schematic type variable of hideType
), while the latter is bty -> typeHider
.
Finally, because the types of A
and B
are different while the single definitional clause of hideType
only allows such occurrences of variables to have the same type, we can prove that hiderHelper
never holds:
Theorem hiderHelper_false: forall A B,
hiderHelper A B -> false.
intros.
case H1.
case H2.
We can write ill-typed code which Abella accepts by using a polymorphic type constructor.
Some definitions to provide types to demonstrate the issue:
The code showing the actual issue:
By using
hideType
to produce atypeHider_c
, we are able to use a term of typeaty
(the variableB
) as the second argument ofhiderHelper
, which is supposed to take a term of typebty
.If Abella disallowed constructors having type variables in argument types which don't appear in the type being built, I don't think it would be possible to build ill-typed code like this. We would not be able to write the
typeHider_c
constructor becauseA
does not occur intypeHider
, andtypeHider_c
is what lets us hide the true type ofB
.