Recherche…


Utilisation de règles de réécriture sur les fonctions surchargées

Dans cette question , @Viclib a demandé comment utiliser les règles de réécriture pour exploiter les lois de la classe de polices afin d'éliminer certains appels de fonctions surchargés:

Attention à la classe suivante:

class ListIsomorphic l where
    toList    :: l a -> [a]
    fromList  :: [a] -> l a

Je demande aussi cette toList . fromList == id . Comment écrire des règles de réécriture pour dire à GHC de faire cette substitution?

Ceci est un cas d'utilisation quelque peu délicat pour le mécanisme de règles de réécriture de GHC, car les fonctions surchargées sont réécrites dans leurs méthodes d'instance spécifiques par des règles implicitement créées en arrière-plan par GHC (quelque chose comme fromList :: Seq a -> [a] serait réécrit en Seq$fromList etc.).

Cependant, en réécrivant d'abord toList et fromList dans des méthodes non-typées non incorporées, nous pouvons les protéger contre une réécriture prématurée et les conserver jusqu'à ce que la règle de la composition puisse s'exécuter:

{-# RULES
  "protect toList"   toList = toList';
  "protect fromList" fromList = fromList';
  "fromList/toList"  forall x . fromList' (toList' x) = x; #-}

{-# NOINLINE [0] fromList' #-}
fromList' :: (ListIsomorphic l) => [a] -> l a
fromList' = fromList

{-# NOINLINE [0] toList' #-}
toList' :: (ListIsomorphic l) => l a -> [a]
toList' = toList


Modified text is an extract of the original Stack Overflow Documentation
Sous licence CC BY-SA 3.0
Non affilié à Stack Overflow