StartseiteMathlog

Typentheorie bei xkcd

Von / 13. Juni 2015 / 3 Kommentare
Mehr

Typentheorie ist ein Teil der Mathematik, von dem ich überhaupt nichts verstehe, obwohl sie zur Zeit sehr angesagt zu sein scheint.

Grob gesagt geht es um die jedem Informatiker ins Blut gegangene Tatsache, dass das Ergebnis einer Verknüpfung mehrerer Objekte davon abhängt, zu welchem Typ die jeweiligen Objekte gehören: 2+2 kann 4 oder 22 sein, je nachdem ob es sich um Zahlen oder Symbole handelt (und mit “+” die Addition oder die Konkatenation gemeint ist).

Unter dem Schlagwort “univalent foundations of mathematics” hat Typentheorie als Teilgebiet der Mathematik in den letzten Jahren viel Aufmerksamkeit bekommen. Aus Topologen-Sicht bemerkenswert, dass es sinnvoll zu sein scheint, Typen nicht als Mengen, sondern als Homotopietypen aufzufassen – das führt zur Homotopietypentheorie.

Bei xkcd heute geht es aber nicht um Typentheorie in der Mathematik, sondern um Programmiersprachen mit ungewöhnlichen Konventionen. In der ersten Zeile etwa wird die Zahl 2 mit dem Symbol 2 addiert, in der 2.Zeile ergibt die Konkatenation des Symbols 2 mit [] nicht etwa “2[]”, sondern “[2]”.

Typentheorie bei xkcd

Mehr Erläterungen hier.

Stichworte: , ,
Mehr

Kommentare (3)

  1. #1 Dr. Webbaer
    13. Juni 2015

    Ohne jetzt jeden Gag verstanden zu haben:
    1.) Daten kommen oft als Zeichen (“char“) , was mit der Erfassungsweise zu tun hat, bspw. mit dem Tippen von Fingerspitzen auf dafür geeignete Geräte.
    2.) Typisierungen meinen Einschränkungen oder Constraints auf wie oben erfasste Daten.
    3.) T. dienen der sogenannten Datenkonsistenz und werden von Datenhaltungssystemen, oft von sogenannten RDBS(en) sichergestellt, als eines deren Leistungsmerkmale.
    4.) Es rechnet sich insofern “besser” mit Zahlen wie mit Zeichen, die keine numerische Bedeutung haben.
    5.) “Rechnen” meint im Sinne von Technik im Sinne der hier erörterten Informationstechnologie Operatoren und viele Operatoren sind überladen (das Fachwort), wenn sogenannte Programmiersprachen gemeint sind.
    Das Kreuz (“+”) meint insofern die Addition und die Verknüpfung von Zeichenfolgen.
    6.) Einige Programmiersprachen wie bspw. Perl arbeiten, sozusagen zynisch, dbzgl. mit dem Datentyp ‘variant‘.
    7.) Insofern versucht die zur Laufzeit bereitstehende Umgebung Typisierungen sozusagen intuitiv vorzunehmen, nicht immer im Sinne des Entwicklers.

    Wobei es bei diesen “glorreichen” sieben Punkten einmal belassen werden soll, ischt ein spannendes Thema, gerade für die Praxis sogenannter Entwickler.

    Insbesondere geht es darum Typisierungen sinnhaft und vom Entwickler gesteuert einzusetzen, der Entwickler soll einerseits nicht behindert oder genötigt werden Einschränkungen der gemeinten Art zu setzen und zu pflegen, andererseits auch auf möglicherweise anfallende Fehlerbehandlung hingewiesen werden von der Entwicklungsumgebung, oft auch erst: zur Laufzeit. [1]

    HTH
    Dr. W

    [1]
    ‘Getting Things Done’ – könnte was mit Larry Wall und seiner Philosophie zu tun haben, im webverwiesenen Text war Ihr Kommentatorenfreund nicht en dé­tail, hoffentlich ist er tauglich.

  2. #2 Karl Mistelberger
    14. Juni 2015

    Das Programmieren von Computern war schweißtreibend bis endlich Fortran kam. Die Welt war nun einigermaßen in Ordnung. Dann kam C. Da schrieb Steve Oualline das Buch “Practical C Programming: Why Does 2+2=5986?”

    Für die Begriffsstutzigen schrieb er noch ein zweites Buch: “How Not to Program in C++: 111 Broken Programs and 3 Working Ones, or Why does 2+2=5986?”

  3. #3 Dr. Webbaer
    17. Juni 2015

    Wer sich ein wenig quälen will, an Hand von Aussagen der bekannte Online-Enzyklopädie:
    -> https://en.wikipedia.org/wiki/History_of_type_theory
    -> https://en.wikipedia.org/wiki/Type_system

    ‘Meaning’ oder ‘Bedeutung’ ergibt sich auf Seiten der derart “formalwissenschaftlichen” Anwendung, des Programms, nicht selbst, sondern erst abstrakt auf die Welt bezogen. [1]

    Wittgenstein war im Erstverwiesenen recht sachnah und lustig, wie der Schreiber dieser Zeilen findet, gerne mal reinschauen.

    MFG
    Dr. W

    [1]
    Programme unterstützen Projekte und Prozesse, die gesellschaftlich stattfinden, einen Wert, idR einen sogenannten Mehrwert (wirtschaftswissenschaftlicher Fachbegriff, aber durchaus allgemein intuitiv) zu unterstützen zu generieren in der Lage sind.
    Bedeutung entsteht in dieser “Realwelt”.