Der Typ einer Funktion hängt von der Eingabe ab

Question

So bemerkte ich, dass nach n = 20 die in LearnYouAHaskell (unten) angegebene faktorielle Funktion aufgrund des endlichen Arbeitsbereichs des Int-Typs ausfällt.

factorial :: Int -> Int 
factorial 0 = 1 
factorial n * factorial (n-1) 

Mit factorial :: Integer -> Integer behebt das Problem schön, aber es brachte die Frage in den Sinn. Angeblich ist Integer etwas langsamer als Int, also idealerweise (und ich weiß, dass ich hier ein paar Pfennige kneife). Ich möchte, dass meine Fakultät nur auf Integer zurückgreift, wenn die Eingabe größer als 20 ist und den Typ Int->Int für die kleineren Zahlen behält. Scheint, dass es eine elegante Lösung dafür geben sollte, wenn-then-else oder Wächter, aber weiter in syntaktischen Pfeffer (Fehlermeldungen)

Answer 1

Sie können entweder durch Verwendung einer Summe Art und Züchten einer hackish Lösung ohne abhängige Typen machen, wenn in einigen Fällen die Besetzung zu Integer bis zum Ende benötigt oder zu verzögern. Ich erwarte nicht, dass eine der beiden Lösungen besser funktioniert als die Verwendung von Integer - keine Angst vor Integer, gmp und mpir sind ziemlich gut.

Die Gießlösung ist so etwas wie:

selectiveFactorial :: Integer -> Integer 
selectiveFactorial i 
    | i < 20 = fromIntegral $ factorial (fromIntegral i :: Int) 
    | otherwise = factorial i 

factorial :: Integral a => a -> a 
factorial 0 = 1 
factorial n = n * factorial (n - 1) 

Answer 2

Der Typ einer Funktion hängt von ihren Werten ab ist genau das, was dependent types sind. Leider hat Haskell keine abhängigen Typen, daher ist dies nicht möglich.

Answer 3

Es ist nicht möglich. Es gibt Dinge, die Sie tun können, aber:

1. Machen Sie den Typ allgemeineres: factorial :: Num a => a -> a; Dies ermöglicht dem Benutzer Ihrer Funktion zu entscheiden, welche Runtime Penalties im Vergleich zu dem Bereich der Nummern zulässig sind.

2. eine Summe Typ wie data PossiblyBig = Small Int | Big Integer, verwenden und dann eine Implementierung haben instance Num PossiblyBig die Dinge kodiert, das in Int als Small passen, und die Dinge, die als Big nicht passen; AFAIK Integer funktioniert schon so (schauen Sie sich die GMP-Implementierung an, wenn Sie sicher wissen wollen), also ist dies eher ein allgemeines Beispiel als Ratschläge, was Sie in dieser speziellen Situation tun sollten.

Answer 4

Wie Rein Henrichs said Sie diese Dinge in einer Sprache mit abhängigen Arten tun könnte, was Haskell nicht (noch ganz) haben. In Idris, sagen wir, es wäre so etwas wie

factorial : (n : Int) -> if n <= 20 then Int else Integer 
factorial n with (n <= 20) 
    factorial n | True = thisfactorial n 
    factorial n | False = thatfactorial n 

aussehen Aber wie wird Sie dieses Ergebnis benutzen? Nun, Sie müssen den Vergleich durchführen, um herauszufinden, welcher Typ zu erwarten ist, und wenn alles gesagt und getan ist, sehe ich nicht, wie Sie etwas gewonnen haben. Der Vollständigkeit halber könnte die Verwendung Website wie folgt aussehen:

use : Int -> Integer 
use n with (factorial n) 
    use n | fn with (n <= 20) 
    use n | fn | False = fn 
    use n | fn | True = cast fn 

Beachten Sie, dass die Reihenfolge der with Klauseln von Bedeutung ist! Die fn Bindung erhält Typ if n <= 20 then Int else Integer; Aus Gründen, die ich nicht vollständig verstehe, muss der Test n <= 20 rechts davon sein, damit die Musterübereinstimmung ihren Typ beeinflusst.