Kann ich in Haskell den Typ einer polymorphen Funktion drucken, wie er werden würde, wenn ich ihm eine Entität eines konkreten Typs übergeben würde?

Dec 12 2020

Hier ist eine polymorphe Funktion in 3 Typen:

:t (.)
(.) :: (b -> c) -> (a -> b) -> a -> c

und hier eine nicht polymorphe Funktion:

:t Data.Char.digitToInt
Data.Char.digitToInt :: Char -> Int

Wenn wir das erstere auf das letztere anwenden, erhalten wir eine polymorphe Funktion in 1 Typ:

:t (.) Data.Char.digitToInt
(.) Data.Char.digitToInt :: (a -> Char) -> a -> Int

was bedeutet, dass dies (.)mit und "instanziiert" wurde (ich bin nicht sicher, ob dies der richtige Begriff ist; als C ++ - Programmierer würde ich es so nennen) mit b === Charund c === Int, daher lautet die Signatur des (.), auf das angewendet digitToIntwird, die folgende

(Char -> Int) -> (a -> Char) -> a -> Int

Meine Frage ist: Gibt es eine Möglichkeit , diese Unterschrift auf dem Bildschirm gedruckt zu haben, gegeben (.), digitToIntund die „Informationen“ , dass ich die ersteren zum letzteren bewerben?

Denn wer interessiert ist, wurde diese Frage früher als Duplikat geschlossen diese .

Antworten

7 MikeSpivey Dec 13 2020 at 06:32

Andere Antworten erfordern die Hilfe von Funktionen, die mit künstlich eingeschränkten Typen definiert wurden, wie z. B. die asTypeOfFunktion in der Antwort von HTNW. Dies ist nicht erforderlich, wie die folgende Interaktion zeigt:

Prelude> let asAppliedTo f x = const f (f x)

Prelude> :t head `asAppliedTo` "x"
head `asAppliedTo` "x" :: [Char] -> Char

Prelude> :t (.) `asAppliedTo` Data.Char.digitToInt
(.) `asAppliedTo` Data.Char.digitToInt
  :: (Char -> Int) -> (a -> Char) -> a -> Int

Dies nutzt den Mangel an Polymorphismus in der Lambda-Bindung aus, der in der Definition von impliziert ist asAppliedTo. Beide Vorkommen fin seinem Körper müssen vom gleichen Typ sein, und das ist der Typ seines Ergebnisses. Die consthier verwendete Funktion hat auch ihren natürlichen Typ a -> b -> a:

const x y = x
12 HTNW Dec 12 2020 at 09:09

Es gibt diese nette kleine Funktion, die in einer Ecke des versteckt ist Prelude:

Prelude.asTypeOf :: a -> a -> a
asTypeOf x _ = x

Es wird dokumentiert als "Erzwingen, dass sein erstes Argument den gleichen Typ wie das zweite hat". Wir können dies verwenden, um das (.)erste Argument des Typs zu erzwingen :

-- (.) = \x -> (.) x = \x -> (.) $ x `asTypeOf` Data.Char.digitToInt -- eta expansion followed by definition of asTypeOf -- the RHS is just (.), but restricted to arguments with the same type as digitToInt -- "what is the type of (.) when the first argument is (of the same type as) digitToInt?" ghci> :t \x -> (.) $ x `asTypeOf` Data.Char.digitToInt
\x -> (.) $ x `asTypeOf` Data.Char.digitToInt
  :: (Char -> Int) -> (a -> Char) -> a -> Int

Dies funktioniert natürlich für so viele Argumente, wie Sie benötigen.

ghci> :t \x y -> (x `asTypeOf` Data.Char.digitToInt) . (y `asTypeOf` head)
\x y -> (x `asTypeOf` Data.Char.digitToInt) . (y `asTypeOf` head)
  :: (Char -> Int) -> ([Char] -> Char) -> [Char] -> Int

Sie können dies als eine Variation der Idee von @ KABuhr in den Kommentaren betrachten - indem Sie eine Funktion mit einer Signatur verwenden, die restriktiver ist als ihre Implementierung, um die Typinferenz zu steuern -, außer dass wir nichts selbst definieren müssen, auf Kosten der Tatsache, dass wir nicht in der Lage sind, dies zu tun Kopieren Sie den betreffenden Ausdruck unter ein Lambda.

8 K.A.Buhr Dec 12 2020 at 09:57

Ich denke, die Antwort von @ HTNW deckt dies wahrscheinlich ab, aber der Vollständigkeit halber ist hier, wie die inContextLösung im Detail funktioniert.

Die Typensignatur der Funktion:

inContext :: a -> (a -> b) -> a

bedeutet, wenn Sie etwas haben, das Sie eingeben möchten, und einen "Kontext", in dem es verwendet wird (ausgedrückt als Lambda, das es als Argument verwendet), sagen Sie mit Typen:

thing :: a1
context :: a2 -> b

Sie können die Vereinigung a1(des allgemeinen Typs von thing) mit a2(den Einschränkungen des Kontexts) erzwingen, indem Sie einfach den Ausdruck konstruieren:

thing `inContext` context

Normalerweise thing :: awürde der einheitliche Typ verloren gehen, aber die Typensignatur von inContextimpliziert, dass der Typ dieses gesamten resultierenden Ausdrucks auch mit dem gewünschten Typ avereinheitlicht wird, und GHCi teilt Ihnen gerne den Typ dieses Ausdrucks mit.

Also der Ausdruck:

(.) `inContext` \hole -> hole digitToInt

Am Ende wird der Typ zugewiesen, der (.)im angegebenen Kontext vorhanden wäre. Sie können dies etwas irreführend schreiben als:

(.) `inContext` \(.) -> (.) digitToInt

da (.)ist so gut ein argumentname für ein anonymes lambda wie es holeist. Dies ist möglicherweise verwirrend, da wir eine lokale Bindung erstellen, die die Definition der obersten Ebene von überschattet (.), aber immer noch dasselbe benennt (mit einem verfeinerten Typ), und dieser Missbrauch von Lambdas es uns ermöglichte, den ursprünglichen Ausdruck (.) digitToIntwörtlich zu schreiben . mit der entsprechenden Kesselplatte.

Es ist eigentlich irrelevant, wie inContextdefiniert wird, wenn Sie nur GHCi nach seinem Typ fragen, also inContext = undefinedhätte es funktioniert. Wenn man sich nur die Typensignatur ansieht, ist es einfach genug, inContexteine funktionierende Definition zu geben :

inContext :: a -> (a -> b) -> a
inContext a _ = a

Es stellt sich heraus, dass dies nur die Definition von ist constund auch inContext = constfunktioniert.

Sie können inContextmehrere Dinge gleichzeitig eingeben, und sie können Ausdrücke anstelle von Namen sein. Um die ersteren unterzubringen, können Sie Tupel verwenden; Damit letzteres funktioniert, haben Sie in Ihren Lambas sinnvollere Argumentnamen verwendet.

Also zum Beispiel:

λ> :t (fromJust, fmap length) `inContext` \(a,b) -> a . b
(fromJust, fmap length) `inContext` \(a,b) -> a . b
  :: Foldable t => (Maybe Int -> Int, Maybe (t a) -> Maybe Int)

sagt Ihnen, dass fromJust . fmap lengthdie Typen im Ausdruck auf Folgendes spezialisiert wurden:

fromJust :: Maybe Int -> Int
fmap length :: Foldable t => Maybe (t a) -> Maybe Int
6 FyodorSoikin Dec 12 2020 at 03:35

Sie können dies mit der TypeApplicationsErweiterung tun, mit der Sie explizit angeben können, welche Typen Sie zum Instanziieren von Typparametern verwenden möchten:

λ :set -XTypeApplications                                 
λ :t (.) @Char @Int
(.) @Char @Int :: (Char -> Int) -> (a -> Char) -> a -> Int

Beachten Sie, dass die Argumente in der genauen Reihenfolge sein müssen.

Bei Funktionen mit einer "regulären" Typensignatur wie foo :: a -> bwird die Reihenfolge durch die Reihenfolge definiert, in der die Typparameter zuerst in der Signatur erscheinen.

Für Funktionen, die ExplicitForalllike verwenden foo :: forall b a. a -> b, wird die Reihenfolge durch das definiert, in dem sie sich befindet forall.


Wenn Sie die Art speziell bezogen auf die Anwendung , um herauszufinden , wollen (.)auf digitToChar(im Gegensatz zu nur zu wissen , welche Arten zu füllen), bin ich ziemlich sicher , dass Sie nicht in GHCi, aber ich kann Haskell IDE - Unterstützung sehr empfehlen.

Zum Beispiel sieht es für mich in VSCode so aus (hier ist die Erweiterung ):

5 chi Dec 12 2020 at 16:39

Dies ist eine geringfügige Abweichung von der Antwort von HTNW.

Angenommen, wir haben einen potenziell großen Ausdruck, der einen polymorphen Bezeichner enthält poly

 .... poly ....

und wir fragen uns, wie der polymorphe Typ zu diesem Zeitpunkt instanziiert wurde.

Dies kann unter Ausnutzung von zwei Funktionen von GHC erfolgen: asTypeOf(wie von HTNW erwähnt) und typisierten Löchern wie folgt:

 .... (poly `asTypeOf` _) ....

Beim Lesen des _Lochs generiert GHC einen Fehler, der den Typ des Begriffs angibt, der anstelle dieses Lochs eingegeben werden soll. Da wir verwendet haben asTypeOf, muss dies derselbe sein wie der Typ der bestimmten Instanz, die polywir in diesem Kontext benötigen.

Hier ist ein Beispiel in GHCi:

> ((.) `asTypeOf` _) Data.Char.digitToInt
<interactive>:11:17: error:
    * Found hole: _ :: (Char -> Int) -> (a -> Char) -> a -> Int