Coût d'exécution de la programmation de type dépendante avec GHC

Question

Je suis en train de programmer une bibliothèque de type dépendante dans Haskell. En utilisant le profilage sur mon exécutable test que je vois quelque chose comme:

commutativity' Math 1189 4022787186 29.1 27.2 29.1 27.2 

commutativity' est essentiellement (récursive) la preuve de l'addition entière propriété de commutativité pour les entiers de niveau de type. Il est défini ceci:

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 

Et puis utilisé dans ma bibliothèque gcastWith pour prouver l'équivalence des différents types. Donc ... 29% de mon temps d'exécution est dépensé pour quelque chose de complètement inutile, puisque la vérification de type se produit au moment de la compilation.

J'avais naïvement supposé que cela n'arriverait pas.

Y at-il quelque chose que je peux faire pour optimiser ces appels inutiles?

Answer 1

Si vous êtes très que le terme de preuve, vous pouvez utiliser quelque chose se termine comme

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

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

Ce doit être utilisé que sur les types ayant un seul pas de constructeur de paramètres, par exemple Refl pour a :~: b. Sinon, votre programme va probablement se bloquer ou se comporter bizarrement. Caveat emptor!

Une variante plus sûre (mais toujours dangereux!) Pourrait être

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

Notez que vous pouvez toujours planter le programme avec cela, si vous passez en bas à elle.

J'espère qu'un jour, GHC effectuera cette optimisation de manière sûre et automatique, assurant une terminaison par analyse statique.