Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
On Sat, 1 Feb 2014, Christian Sternagel wrote: Reviving this old thread once more ;) I've lost track of this thread. Are there still any open questions? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
Hi Christian,
Basically, nothing wrong. When abbreviations are declared, terms are
checked such that no abbreviations themselves are expanded. So in the
examples, the do-syntax produces an abbreviation bind_do which in this
case is not unfolded and so does not trigger the adhoc-overloading
disambiguation of bind. So, there is nothing wrong here.
Does that also mean that the resulting unit itself is as you would
expect in the following?
abbreviation
abbr2 == do {
Some ();
Some False
} -- additional type variable
I would say so.
By expanding adhoc overloading do you mean replacing concrete
constants by overloaded generic ones?
Yes.
When is Proof_Context.abbrev_mode actually true?
When parsing abbreviation declarations.
What I first thought was that I should avoid to insert overloaded (i.e.,
generic constants; cf. Adhoc_overloading.insert_overloaded) constants
whenever Proof_Context.abbrev_mode is true. But just trying this on some
examples did not change anything (as far as I can tell).
Did your examples interleave abbreviations and syntactic ad-hoc
overloading? Only then effects are about to be expected.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
Reviving this old thread once more ;)
I think I need some clarifications first:
On 12/05/2013 05:05 PM, Florian Haftmann wrote:
Reviving this old thread, Peter and me found out what is actually going
on here.
Basically, nothing wrong. When abbreviations are declared, terms are
checked such that no abbreviations themselves are expanded. So in the
examples, the do-syntax produces an abbreviation bind_do which in this
case is not unfolded and so does not trigger the adhoc-overloading
disambiguation of bind. So, there is nothing wrong here.
Does that also mean that the resulting unit itself is as you would
expect in the following?
abbreviation
abbr2 == do {
Some ();
Some False
} -- additional type variable
Even more, given the analogy that ad-hoc overloading represents some
kind of overloaded abbreviations, adhoc-overloading should never be
expanded while abbreviations are checked (query
Proof_Context.abbrev_mode). @Christian. You might consider to adjust
your code accordingly after a second round of thinking about.
By expanding adhoc overloading do you mean replacing concrete
constants by overloaded generic ones?
When is Proof_Context.abbrev_mode actually true?
What I first thought was that I should avoid to insert overloaded (i.e.,
generic constants; cf. Adhoc_overloading.insert_overloaded) constants
whenever Proof_Context.abbrev_mode is true. But just trying this on some
examples did not change anything (as far as I can tell).
What's the concrete suggestion?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
On Sun, 13 Oct 2013, Florian Haftmann wrote: Here a bisect would be helpful when this came to happen actually (or is it already present in Isabelle2013). This one already goes wrong in Isabelle2013. OK. I guess it is some variant of the ever recurring problem of »hidden polymorphism«. Will take some time to figure out actually. I've lost track of this thread. For me the question right now: Is there anything left to do for Isabelle2013-1? Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
Here a bisect would be helpful when this came to happen actually (or is it already present in Isabelle2013). This one already goes wrong in Isabelle2013. OK. I guess it is some variant of the ever recurring problem of »hidden polymorphism«. Will take some time to figure out actually. I've lost track of this thread. For me the question right now: Is there anything left to do for Isabelle2013-1? The conservative answer is: since it has been the same thing already in the last release, there is no urgent pressure to do someting about it now. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
Here a bisect would be helpful when this came to happen actually (or is it already present in Isabelle2013). This one already goes wrong in Isabelle2013. OK. I guess it is some variant of the ever recurring problem of »hidden polymorphism«. Will take some time to figure out actually. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
Here a bisect would be helpful when this came to happen actually (or is it already present in Isabelle2013). This one already goes wrong in Isabelle2013. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
Referring to Isabelle_2013 AND Isabelle_12_Sep_2013:
In the following example, using an abbreviation that contains
monad-syntax introduces a superfluous additional itself-parameter, that,
however, is immediately instantiated to unit itself. Note that, when
replacing abbreviation by definition, everything works as expected.
It looks like (see also my previous post) that monad-syntax has some
severe issues with abbreviations, that I would really like to see fixed
in the next release, as they render unusable many of my tools.
--
Peter
theory Scratch
imports
~~/src/HOL/Library/Monad_Syntax
begin
abbreviation abbr1 == Some () = (%_. Some False)
abbreviation abbr2 == do {
Some ();
Some False
}
(* ### Additional type variable(s) in specification of abbr2: 'a *)
term (abbr1, abbr2)
(*
(Some () = (%_::unit. Some False),
%TYPE::unit itself. Some () = (%_::unit. Some False))
:: bool option * (unit itself = bool option)
*)
definition abbr3 == do {
Some ();
Some False
}
(* No additional type parameter *)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
