Wie funktioniert Haskell printf?

104

Die Typensicherheit von Haskell ist unübertroffen, nur bei Sprachen mit abhängiger Eingabe. Aber mit Text.Printf ist eine tiefe Magie im Gange , die ziemlich typisch wirkt.

> printf "%d\n" 3
3
> printf "%s %f %d" "foo" 3.3 3
foo 3.3 3

Was ist die tiefe Magie dahinter? Wie kann die Text.Printf.printfFunktion solche variadischen Argumente annehmen?

Welche allgemeine Technik wird verwendet, um in Haskell verschiedene Argumente zu berücksichtigen, und wie funktioniert sie?

(Randnotiz: Bei Verwendung dieser Technik geht anscheinend die Sicherheit einiger Typen verloren.)

> :t printf "%d\n" "foo"
printf "%d\n" "foo" :: (PrintfType ([Char] -> t)) => t
Dan Burton
quelle
15
Sie können einen typsicheren Ausdruck nur mit abhängigen Typen erhalten.
August
9
Lennart hat ganz recht. Die Typensicherheit von Haskell ist nach Sprachen mit noch abhängigeren Typen an zweiter Stelle als Haskell. Natürlich können Sie einen printf-ähnlichen Objekttyp sicher machen, wenn Sie für das Format einen informativeren Typ als String auswählen.
Schweinearbeiter
3
Siehe oleg für mehrere Varianten von printf: okmij.org/ftp/typed-formatting/FPrintScan.html#DSL-In
sclv
1
@augustss Sie können einen typsicheren Ausdruck nur mit abhängigen Typen ODER TEMPLATE HASKELL erhalten! ;-)
MathematicalOrchid
3
@MathematicalOrchid Template Haskell zählt nicht. :)
August

Antworten:

131

Der Trick besteht darin, Typklassen zu verwenden. Im Fall von printfist der Schlüssel die PrintfTypeTypklasse. Es werden keine Methoden verfügbar gemacht, aber der wichtige Teil liegt trotzdem in den Typen.

class PrintfType r
printf :: PrintfType r => String -> r

Hat printfalso einen überladenen Rückgabetyp. Im trivialen Fall haben wir keine zusätzlichen Argumente, so dass wir zu instanziiert müssen in die Lage rzu IO (). Dafür haben wir die Instanz

instance PrintfType (IO ())

Um eine variable Anzahl von Argumenten zu unterstützen, müssen wir als nächstes die Rekursion auf Instanzebene verwenden. Insbesondere benötigen wir eine Instanz, damit, wenn a rist PrintfType, ein Funktionstyp x -> rauch a ist PrintfType.

-- instance PrintfType r => PrintfType (x -> r)

Natürlich wollen wir nur Argumente unterstützen, die tatsächlich formatiert werden können. Hier kommt die zweite Typklasse ins PrintfArgSpiel. Die eigentliche Instanz ist also

instance (PrintfArg x, PrintfType r) => PrintfType (x -> r)

Hier ist eine vereinfachte Version, die eine beliebige Anzahl von Argumenten in der ShowKlasse verwendet und diese nur druckt:

{-# LANGUAGE FlexibleInstances #-}

foo :: FooType a => a
foo = bar (return ())

class FooType a where
    bar :: IO () -> a

instance FooType (IO ()) where
    bar = id

instance (Show x, FooType r) => FooType (x -> r) where
    bar s x = bar (s >> print x)

Hier wird bareine E / A-Aktion ausgeführt, die rekursiv aufgebaut wird, bis keine Argumente mehr vorhanden sind. An diesem Punkt führen wir sie einfach aus.

*Main> foo 3 :: IO ()
3
*Main> foo 3 "hello" :: IO ()
3
"hello"
*Main> foo 3 "hello" True :: IO ()
3
"hello"
True

QuickCheck verwendet dieselbe Technik, bei der die TestableKlasse eine Instanz für den Basisfall Boolund eine rekursive Instanz für Funktionen hat, die Argumente in der ArbitraryKlasse annehmen .

class Testable a
instance Testable Bool
instance (Arbitrary x, Testable r) => Testable (x -> r) 
Hammar
quelle
Gute Antwort. Ich wollte nur darauf hinweisen, dass haskell den Typ von Foo anhand der angewandten Argumente herausfindet. Um dies zu verstehen, möchten Sie möglicherweise den Typ der Foo-Explizität wie folgt angeben: λ> (foo :: (Show x, Show y) => x -> y -> IO ()) 3 "Hallo"
redfish64
1
Obwohl ich verstehe, wie der Argumentteil mit variabler Länge implementiert wird, verstehe ich immer noch nicht, wie der Compiler ablehnt printf "%d" True. Dies ist für mich sehr mystisch, da es den Anschein hat, dass der Laufzeitwert (?) "%d"Zur Kompilierungszeit entschlüsselt wird, um eine zu erfordern Int. Das ist absolut verwirrend für mich. . . zumal der Quellcode keine Dinge wie DataKindsoder verwendet TemplateHaskell(ich habe den Quellcode überprüft, ihn aber nicht verstanden.)
Thomas Eding
2
@ThomasEding Der Grund, warum der Compiler ablehnt, printf "%d" Trueist, dass es keine BoolInstanz von gibt PrintfArg. Wenn Sie ein Argument des falschen Typs übergeben, für das eine Instanz vorhanden ist PrintfArg, wird es kompiliert und zur Laufzeit eine Ausnahme ausgelöst. Beispiel:printf "%d" "hi"
Travis Sunderland