Jak działa Haskell printf?

104

Bezpieczeństwo typów Haskella nie ma sobie równych tylko w przypadku języków z typami zależnymi. Ale w Text.Printf zachodzi pewna głęboka magia, która wydaje się raczej dziwna .

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

Jaka kryje się za tym głęboka magia? W jaki sposób Text.Printf.printffunkcja może przyjmować różne argumenty, takie jak ta?

Jaka jest ogólna technika umożliwiająca stosowanie argumentów wariadycznych w Haskell i jak to działa?

(Uwaga dodatkowa: przy stosowaniu tej techniki najwyraźniej tracimy pewne bezpieczeństwo typów).

> :t printf "%d\n" "foo"
printf "%d\n" "foo" :: (PrintfType ([Char] -> t)) => t
Dan Burton
źródło
15
Bezpieczny typ printf można uzyskać tylko przy użyciu typów zależnych.
sierpień
9
Lennart ma rację. Bezpieczeństwo typów Haskella ustępuje językom z jeszcze bardziej zależnymi typami niż Haskell. Oczywiście, możesz uczynić typ rzeczy podobny do printf bezpiecznym, jeśli wybierzesz bardziej informacyjny typ niż String dla formatu.
pigworker
3
zobacz oleg dla wielu wariantów printf: okmij.org/ftp/typed-formatting/FPrintScan.html#DSL-In
sclv
1
@augustss Możesz uzyskać tylko bezpieczny typ printf używając zależnych typów LUB SZABLONU HASKELL! ;-)
MathematicalOrchid
3
@MathematicalOrchid Template Haskell się nie liczy. :)
sierpień

Odpowiedzi:

131

Sztuczka polega na użyciu klas typów. W przypadku printfklucza jest to PrintfTypeklasa typu. Nie ujawnia żadnych metod, ale ważna część i tak jest w typach.

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

Więc printfma przeciążony typ powrotu. W trywialnym przypadku nie mamy żadnych dodatkowych argumentów, więc musimy mieć możliwość wystąpienia rdo IO (). W tym celu mamy instancję

instance PrintfType (IO ())

Następnie, aby obsłużyć zmienną liczbę argumentów, musimy użyć rekursji na poziomie instancji. W szczególności potrzebujemy instancji, więc jeśli rjest a PrintfType, typ funkcji x -> rrównież jest PrintfType.

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

Oczywiście chcemy obsługiwać tylko argumenty, które faktycznie można sformatować. W tym miejscu PrintfArgpojawia się klasa drugiego typu . A więc rzeczywista instancja jest

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

Oto uproszczona wersja, która pobiera dowolną liczbę argumentów z Showklasy i po prostu je drukuje:

{-# 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)

Tutaj barwykonuje akcję IO, która jest budowana rekurencyjnie, dopóki nie ma więcej argumentów, w którym to momencie po prostu ją wykonujemy.

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

QuickCheck używa również tej samej techniki, w której Testableklasa ma instancję dla przypadku podstawowego Booli rekursywną dla funkcji, które pobierają argumenty w Arbitraryklasie.

class Testable a
instance Testable Bool
instance (Arbitrary x, Testable r) => Testable (x -> r) 
hammar
źródło
Świetna odpowiedź. Chciałem tylko zaznaczyć, że haskell analizuje typ Foo na podstawie zastosowanych argumentów. Aby to zrozumieć, możesz określić typ jawności Foo w następujący sposób: λ> (foo :: (Show x, Show y) => x -> y -> IO ()) 3 "hello"
redfish64
1
Chociaż rozumiem, w jaki sposób implementowana jest część argumentu o zmiennej długości, nadal nie rozumiem, w jaki sposób kompilator odrzuca printf "%d" True. Jest to dla mnie bardzo mistyczne, ponieważ wydaje się, że wartość czasu wykonania (?) Jest "%d"odczytywana w czasie kompilacji, aby wymagać pliku Int. To jest dla mnie absolutnie zaskakujące. . . zwłaszcza, że ​​kod źródłowy nie używa takich rzeczy jak DataKindslub TemplateHaskell(sprawdziłem kod źródłowy, ale go nie zrozumiałem).
Thomas Eding
2
@ThomasEding Powodem, dla którego kompilator odrzuca, printf "%d" Truejest brak Boolwystąpienia PrintfArg. Jeśli przekażesz argument niewłaściwego typu, który ma wystąpienie PrintfArg, kompiluje się i zgłasza wyjątek w czasie wykonywania. Np .:printf "%d" "hi"
Travis Sunderland