Laufzeitkosten von abhängiger Programmierung mit GHC

Ich programmiere eine abhängige Bibliothek in Haskell. Mit Profilierung auf meinem Test ausführbar sehe ich so etwas wie:Laufzeitkosten von abhängiger Programmierung mit GHC

commutativity' Math 1189 4022787186 29.1 27.2 29.1 27.2

commutativity' ist im Grunde (rekursiv) der Nachweis der Integer-Addition commutativity Eigenschaft für Typ-Level-Zahlen. Es ist dies definiert:

commutativity' :: SNat n -> SNat m -> Plus (S n) m :~: Plus n (S m) 
commutativity' SZ m = Refl 
commutativity' (SS n) m = gcastWith (commutativity' n m) Refl

Und dann in meiner Bibliothek verwendet mit gcastWith die Gleichwertigkeit der verschiedenen Arten zu beweisen.

Also ... 29% meiner Laufzeit ist für etwas völlig nutzlos ausgegeben, da Typ-Überprüfung zur Kompilierzeit passiert.

Ich hatte naiv angenommen, dass dies nicht passieren würde.

Gibt es etwas, was ich tun kann, um diese nutzlosen Anrufe zu optimieren?

Quelle

2016-12-30 denormal

Dies sind die Kosten für die Verwendung einer gesamten Sprache. Typ Sicherheit beruht auf der Bewertung von Beweisen in kanonischer Form. In vollständigen Sprachen können Proofs ohne Auswertung vertraut und somit zur Laufzeit gelöscht werden. Sie könnten den Trust-Hit nehmen und 'unsafeCoerce' verwenden, nachdem Sie überprüft haben, dass Ihr Programm hinter dem Typchecker steht. – pigworker

Siehe Abschnitt 4.4.4 "Laufende Beweise" von Richard A. Eisenbergs These https://arxiv.org/abs/1610.07978 – danidiaz

Ich träume davon, dass GHC einen (abstrakten) Checker für die Terminierung integriert und automatisch "Beweise" mit Hilfe von Null optimiert/neu schreibt Kostbare Zwänge. Das wäre _really_ nett. – chi

Wenn Sie sehr sicher, dass der Beweis Begriff endet Sie so etwas wie

unsafeProof :: proof -> proof 
unsafeProof _ = unsafeCoerce() 

someFunction :: forall n m. ... 
someFunction = case unsafeProof myProof :: Plus (S n) m :~: Plus n (S m) of 
    Refl -> ...

genutzt werden müssen, nur auf Typen mit einer einzigen keine Parameter Konstruktor verwenden können, beispielsweise Refl für a :~: b. Andernfalls wird Ihr Programm wahrscheinlich abstürzen oder sich merkwürdig verhalten. Vorwurfsvollstrecker!

Ein sicherer (aber immer noch unsicher!) Variante könnte

unsafeProof :: a :~: b -> a :~: b 
unsafeProof _ = unsafeCoerce()

Hinweis sein, dass Sie noch das Programm mit, dass abstürzen, wenn Sie unten, um es passieren.

Ich hoffe, eines Tages wird GHC diese Optimierung sicher und automatisch durchführen, um die Beendigung durch statische Analyse sicherzustellen.

Quelle

2016-12-30 22:02:08 chi

Hmmm ... Ich denke, dass die Nachfrage nach dieser Terminierungsanalyse viel größer sein wird, nachdem Richard Eisenberg abhängige Typen implementiert hat. – Alec

FWIW, das Idiom, das ich häufiger in 'base' und anderen Bibliotheken sehe ([Beispiel] (https://hackage.haskell.org/package/base-4.9.0.0/docs/src/Data.Typeable.html#eqT)) ist 'unsafeCoerce Refl', nicht' unsafeCoerce() '.Ich nehme an, es ist widerstandsfähiger gegen eine Änderung der Darstellung von ': ~:' –

@BenjaminHodgson Es verdeutlicht die Absicht besser, ja. Für den allgemeinen Fall, obwohl "unsafeProof :: proof -> proof" gibt es keinen "besten" Konstruktor, den wir verwenden können, also habe ich '()' als das kanonische Element des letzten Typs verwendet. – chi

Laufzeitkosten von abhängiger Programmierung mit GHC

Antwort

Verwandte Themen