Email Gateway (Aug 19 2022 at 08:13): Email Gateway (Aug 19 2022 at 08:13):From: Tobias Nipkow <nipkow@in.tum.de>
type_synonym 'a t = "'a :: field"
yields
Ignoring sort constraints in type variables(s): "'a"
in type abbreviation "t"
Why that? It would be very nice not to lose them.
Tobias
Email Gateway (Aug 19 2022 at 08:13):From: Makarius <makarius@sketis.net>
Can you explain what you are trying to achieve? Do you want the system to
reject type expressions if the argument types of synonyms do not observe
the sort constraint?
Type classes never restrict the domain of type constructors, they are
always defined. Type synonyms are not even type constructors, just some
abstract syntax for existing types.
Makarius
Email Gateway (Aug 19 2022 at 08:13):From: Tobias Nipkow <nipkow@in.tum.de>
I figured it out myself: because in an application to some type T, "T t = T ::
field", but the rhs is only legal if T is a type variable, not a compound type.
Hence my type synonym would only make sense if we allowed types of the form "T
:: C" (just like we allow terms of the form "e :: T"). I had not thought this
through, but by analogy with the term level, I guess "T::C" should be rejected
if T is not of class C.
Although I had not originally thought of this generalization, I must say that I
have occasionally wished I could write "T :: C" to check if some type is in some
class. But maybe there is alternative way to check this?
Tobias
Email Gateway (Aug 19 2022 at 08:15):From: Makarius <makarius@sketis.net>
On Fri, 10 Aug 2012, Tobias Nipkow wrote:
I figured it out myself: because in an application to some type T, "T t
= T :: field", but the rhs is only legal if T is a type variable, not a
compound type. Hence my type synonym would only make sense if we allowed
types of the form "T :: C" (just like we allow terms of the form "e ::
T"). I had not thought this through, but by analogy with the term level,
I guess "T::C" should be rejected if T is not of class C.
Correct. The term language as full type constraint solving, but the type
language not. Sort constraints are limited to type variables, and there
is no "sort inference".
In the past 2 decades I have occasionally observed the difference as a
matter of fact. I don't think it would be feasible to change this.
Although I had not originally thought of this generalization, I must say
that I have occasionally wished I could write "T :: C" to check if some
type is in some class. But maybe there is alternative way to check this?
Once you write down T as expression, its type variables have already some
sort assignment, so it is all settled.
What exactly means "to check"? What is the application context?
Makarius
Email Gateway (Aug 19 2022 at 08:15):From: Tobias Nipkow <nipkow@in.tum.de>
Am 10/08/2012 16:37, schrieb Makarius:
On Fri, 10 Aug 2012, Tobias Nipkow wrote:
I figured it out myself: because in an application to some type T, "T t = T ::
field", but the rhs is only legal if T is a type variable, not a compound
type. Hence my type synonym would only make sense if we allowed types of the
form "T :: C" (just like we allow terms of the form "e :: T"). I had not
thought this through, but by analogy with the term level, I guess "T::C"
should be rejected if T is not of class C.Correct. The term language as full type constraint solving, but the type
language not. Sort constraints are limited to type variables, and there is no
"sort inference".In the past 2 decades I have occasionally observed the difference as a matter of
fact. I don't think it would be feasible to change this.
And it would not buy us very much, except:
Although I had not originally thought of this generalization, I must say that
I have occasionally wished I could write "T :: C" to check if some type is in
some class. But maybe there is alternative way to check this?Once you write down T as expression, its type variables have already some sort
assignment, so it is all settled.What exactly means "to check"? What is the application context?
Check in the sense of ascertain, test, verify. Writing T down and having it
parsed settles only that it (T) is a legal type, but not if it is, for example,
a field.
Tobias
Email Gateway (Aug 19 2022 at 08:16):From: Makarius <makarius@sketis.net>
Of course, one can do this in ML. So far I was under the implicit
assumption that we talk about type inference for the surface syntax that
is usually exposed to end-users.
Here is an example:
ML {*
val T = @{typ "'a::finite * 'b::finite * bool"};
val S = @{sort finite};
@{assert} (Sign.of_sort @{theory} (T, S))
*}
So T is first produced by going through the whole syntax + check layers of
Isabelle. Later we test if it belongs to a certain sort.
Once could wrap something like this into a document antiquotation for
example. Note that it can not be done inside an ML syntax translation
-- that is too early in the many syntax layers and the information is not
there yet.
Makarius
Email Gateway (Aug 19 2022 at 08:16):From: Tobias Nipkow <nipkow@in.tum.de>
I meant on the Isabelle top level. Like command "typ". But with class.
Tobias
Email Gateway (Aug 19 2022 at 08:16):From: Makarius <makarius@sketis.net>
Here are some variants with terms, using the regular type-inference to
ensure a certain sort membership in the end:
term "TYPE('a::finite * 'b::finite * bool) :: _::finite itself"
notepad
begin
let "_ :: _::finite itself" = "TYPE('a::finite * 'b::finite * bool)"
end
This works because "_::finite" is a type-inference parameter that can be
instantiated.
In principle, one could cook up something like SORT_CONSTRAINT for the
above, although that is not that elegant.
This is just type-inference, not sort-inference. And without the term
context, there would not even be type-inference.
Makarius
Email Gateway (Aug 19 2022 at 08:16):From: Tobias Nipkow <nipkow@in.tum.de>
There would probably not be that many uses of such a document antiquotation but
surely one could also wrap that code up into a top level command?
Tobias
Email Gateway (Aug 19 2022 at 08:17):From: Makarius <makarius@sketis.net>
I would rather make it a variant of the existing 'typ' command like this:
typ T -- "as before"
typ T :: S -- "with sort check"
I'll study the situation of the sources soon ...
Makarius
Email Gateway (Aug 19 2022 at 08:17):From: Tobias Nipkow <nipkow@in.tum.de>
Am 12/08/2012 22:03, schrieb Makarius:
On Sat, 11 Aug 2012, Tobias Nipkow wrote:
surely one could also wrap that code up into a top level command?
I would rather make it a variant of the existing 'typ' command like this:
typ T -- "as before"
typ T :: S -- "with sort check"
Great minds think alike ;-)
I hadn't suggested it myself because I thought you might object that this gives
the impression that "T :: S" is legal syntax for types in general.
But I am all for it!
Tobias
I'll study the situation of the sources soon ...
Makarius
Last updated: Apr 26 2024 at 12:28 UTC