[isabelle-dev] Fwd: Bug in Isabelle 2019/2020

[Manuel Eberl]

Oops, sorry about that!

Due to a combination of circumstances, somebody wrote a message to me
personally to the isabelle-dev mailing list and I clicked "reply" and
then this happened. Please ignore this.

Manuel


On 20/11/2020 10:37, Manuel Eberl wrote:
> Ich weiß nicht, wie die Policy auf der isabelle-users-Mailingliste ist.
> Mir war zumindest nicht klar, dass man da subscribed sein muss, um
> posten zu können.
> 
> So oder so ist das aber kein Bug, sondern völlig erwartetes Verhalten,
> und wie ich mir schon dachte liegt es an Polymorphismus:
> 
>   "to_bl (word_cat (y::4 word) (x::8 word)) =
>    to_bl (of_bl (to_bl y @ to_bl x))"
> 
> Wenn man hier [[show_sorts]] anmacht (z.B. mit "declare [[show_sorts]]"
> im theory toplevel oder mit "note [[show_sorts]]" im Isar-Beweis oder
> mit "using [[show_sorts]]" im apply-Beweis) sieht man da folgendes:
> 
> variables:
>   x :: 8 word
>   y :: 4 word
> type variables:
>   'a, 'b :: len0
> 
> Dass da zwei Typvariablen 'a und 'b sind (die für die Längen
> irgendwelcher Wörter stehen) klingt schon einmal ungut. Man kann
> Isabelle auch direkt fragen, warum die linke und rechte Seite nicht
> gleich sind, indem man "rule refl" anwendet und unification tracing
> anschaltet:
> 
>     using [[unify_trace_failure]]
>     apply (rule refl)
> 
> Da bekommt man dann die Fehlermeldung
> 
>   The following types do not unify:
>   'a::len0 word ⇒ bool list
>   'b::len0 word ⇒ bool list
> 
> Ich hab mir den Term dann etwas genauer angesehen und das Problem ist
> die Funktion word_cat:
> 
>   word_cat :: "'a::len0 word ⇒ 'b::len0 word ⇒ 'c::len0 word"
> 
> Diese Funktion macht aus zwei Wörtern beliebiger Länge ein Wort
> beliebiger Länge. Gleichzeitig macht das "to_bl", das darauf dann
> angewandt wird, aus einem Wort beliebiger Länge eine Liste von booleans.
> Dadurch kann dann die Typinferenz von Isabelle nicht mehr herleiten,
> dass die Wörter links und rechts von dem "=" gleiche Länge haben sollen.
> 
> Also am besten das Ergebnis von "word_cat" immer mit einer Typannotation
> versehen. (das gleiche gilt für of_bl, eigentlich alle Funktionen, deren
> Rückgabetyp eine zusätzliche Typvariable enthält).
> 
> Übermäßiger Polymorphismus ist manchmal etwas haarig, und da das
> Typsystem von Isabelle relativ simpel ist sind manche Operationen leider
> deutlich polymorpher als man sie gerne hätte…
> 
> Viele Grüße
> 
> Manuel
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>