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

[Manuel Eberl]

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