Warum hat eine Funktion, die mit Mustererkennung erstellt wurde, die Integritätsbedingung Typ Eq, aber nicht bei Verwendung eines Datenkonstruktors?

Question

Warum GHCI eine equality type Einschränkung in der Art Signatur für diese Funktion Liste matchInt, die ich über Mustervergleich aufgebaut:

$ ghci 
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help 
Prelude> :{ 
Prelude| matchInt 1 = 3 
Prelude| matchInt _ = 4 
Prelude| :} 
Prelude> matchInt 1 
3 
Prelude> matchInt 22 
4 
Prelude> :t matchInt 
matchInt :: (Eq a, Num a, Num p) => a -> p 

Wenn dagegen einen einfachen Daten Konstruktor verwendet, gibt es keine Einschränkung Gleichheit Art.

$ ghci 
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help 
Prelude> data Z = Y Int 
Prelude> :{ 
Prelude| matchDataInt (Y 1) = 3 
Prelude| matchDataInt _ = 4 
Prelude| :} 
Prelude> matchDataInt (Y 1) 
3 
Prelude> matchDataInt (Y 22) 
4 
Prelude> :t matchDataInt 
matchDataInt :: Num p => Z -> p 

Tat Instanzen von Z kann nicht vergleichen:

Prelude> Y 22 == Y 33 
<interactive>:11:1: error: 
    • No instance for (Eq Z) arising from a use of ‘==’ 
    • In the expression: Y 22 == Y 33 
     In an equation for ‘it’: it = Y 22 == Y 33 

Also noch einmal, warum hat die matchInt Funktionsliste der Gleichheit als Einschränkungsart aber nicht die Funktion matchDataInt?

Diese question ist verwandt. Wenn jedoch ein Gleichheitstest für matchInt benötigt wird, warum wird er nicht für matchDataInt benötigt? Und hier komme ich zu meinem wichtigsten Punkt: nicht beidematchInt und matchDataInt müssen gegen 1 für die Mustererkennung zu arbeiten zu testen?

Answer 1

syntaktisch matchInt gebaut wird auf einem Muster Spiel definieren könnte, aber die patern match hier ist eine Illusion. 1 ist kein Datenkonstruktor. Numerische Literale sind überladen. 1 entspricht fromInteger #1, wobei #1 ein nicht überladenes Merkmal (nicht in Standard-Haskell ausdrückbar) vom Typ Integer ist. Sie können nicht wirklich Muster gegen solche Dinge ausrichten.

So ist der Compiler können Sie schreiben, was syntaktisch ein Muster Spiel ist, aber diese Bezeichnung bedeutet wirklich eine Wache:

matchInt 1 = ... -- what is written 
matchInt x | x == fromInteger #1 = ... -- what it really means 

Da die Art der matchInt nicht explizit angegeben ist, gefolgert wird. Es ist eine Funktion, also ist der Typ eine Verfeinerung von a->b. Der Aufruf von fromInteger führt zu der Einschränkung Num a, und der Aufruf an == führt zu der Einschränkung Eq a, und das ist alles, was wir über a sagen können.

Wenn OTOH wir die Funktion eine explizite Unterschrift geben, sagen

matchInt :: Int->Int 

dann wir den Typ nicht schließen müssen, aber nur überprüfen, ob sie die Einschränkungen erfüllt. Da Int sowohl Eq Int als auch Num Int erfüllt, ist alles in Ordnung.

Und das ist, was in Ihrem zweiten Beispiel passiert. Es ist bekannt, dass der übereinstimmende Typ Int ist, und zwar nicht aufgrund einer expliziten Typ-Signatur, sondern weil er aus der Y Int-Alternative Z abgeleitet wird. Auch hier hat Int bereits alle benötigten Instanzen.

Answer 2

Die matchDataInt Funktion keine Eq Einschränkung erforderlich, da es speziell auf eine Int Spiele und Int s bereits eine Eq Instanz haben.

Ihre matchInt Funktion nimmt nicht nur Int s als Parameter - es jede Art Zahl nehmen, solange Sie diese Zahl für die Gleichstellung vergleichen. Deshalb hat es Typ (Eq a, Num a, Num p) => a -> p. Sie könnten auch geben Sie den Typ Num p => Int -> p (spezialisiert a bis Int), weil Int bereits Eq und Num Instanzen hat.

Ihre matchDataInt Funktion, auf der anderen Seite nimmt eine Z als Argument und jede Z enthält eine Int. Ein Mustervergleich gegen , dass Int ergibt eine Eq Einschränkung, aber nur auf der Int. Sie könnten stattdessen haben

data Z' a = Y' a 

matchDataNum :: (Eq a, Num a, Num p) => Z' a -> p 
matchDataNum (Y' 1) = 3 
matchDataNum _  = 4 

Und hier könnten Sie die Eq a Einschränkung nicht entfernen.

---

Dies alles könnte etwas klarer mit Variantenfunktionen sein, die Zahlen nicht selbst zurückgeben.Wenn wir

data Z = Y Int 
data Z' a = Y' a 

is1 1 = True 
is1 _ = False 

isY1 (Y 1) = True 
isY1 _  = False 

isY'1 (Y' 1) = True 
isY'1 _  = False 

haben dann die drei Funktionen, die wir definiert haben, haben die Typen

is1 :: (Eq a, Num a) => a -> Bool 
isY1 :: Z -> Bool 
isY'1 :: (Eq a, Num a) => Z' a -> Bool 

Wir auch

is1Int :: Int -> Bool 
is1Int 1 = True 
is1Int _ = False