Comment rendre cet algorithme plus paresseux sans me répéter?

9

(Inspiré par ma réponse à cette question .)

Considérez ce code (il est censé trouver le plus grand élément inférieur ou égal à une entrée donnée):

data TreeMap v = Leaf | Node Integer v (TreeMap v) (TreeMap v) deriving (Show, Read, Eq, Ord)

closestLess :: Integer -> TreeMap v -> Maybe (Integer, v)
closestLess i = precise Nothing where
  precise :: Maybe (Integer, v) -> TreeMap v -> Maybe (Integer, v)
  precise closestSoFar Leaf = closestSoFar
  precise closestSoFar (Node k v l r) = case i `compare` k of
    LT -> precise closestSoFar l
    EQ -> Just (k, v)
    GT -> precise (Just (k, v)) r

Ce n'est pas très paresseux. Une fois le GTcas entré, nous savons avec certitude que la valeur de retour finale sera Justquelque chose plutôt que Nothing, mais le Justreste n'est pas disponible avant la fin. Je voudrais rendre ce paresseux afin que le Justsoit disponible dès que le GTcas est entré. Mon cas de test pour cela est que je veux Data.Maybe.isJust $ closestLess 5 (Node 3 () Leaf undefined)évaluer Trueplutôt que d'enfoncer. Voici une façon dont je peux penser à faire ceci:

data TreeMap v = Leaf | Node Integer v (TreeMap v) (TreeMap v) deriving (Show, Read, Eq, Ord)

closestLess :: Integer -> TreeMap v -> Maybe (Integer, v)
closestLess _ Leaf = Nothing
closestLess i (Node k v l r) = case i `compare` k of
  LT -> closestLess i l
  EQ -> Just (k, v)
  GT -> Just (precise (k, v) r)
  where
    precise :: (Integer, v) -> TreeMap v -> (Integer, v)
    precise closestSoFar Leaf = closestSoFar
    precise closestSoFar (Node k v l r) = case i `compare` k of
      LT -> precise closestSoFar l
      EQ -> (k, v)
      GT -> precise (k, v) r

Cependant, je me répète maintenant: la logique de base est maintenant à la fois closestLessdans et dans precise. Comment puis-je écrire ceci pour qu'il soit paresseux mais sans me répéter?

Joseph Sible-Reinstate Monica
la source

Réponses:

4

Plutôt que d'utiliser des wrappers explicites, vous pouvez tirer parti du système de types. Notez que la version de precisecelle-ci utilise Maybevotre premier extrait de code:

precise :: Maybe (Integer, v) -> TreeMap v -> Maybe (Integer, v)
precise closestSoFar Leaf = closestSoFar
precise closestSoFar (Node k v l r) = case i `compare` k of
  LT -> precise closestSoFar l
  EQ -> Just (k, v)
  GT -> precise (Just (k, v)) r

est presque exactement le même algorithme que la version de precisewithout Maybede votre deuxième extrait de code, qui pourrait être écrit dans le Identityfoncteur comme:

precise :: Identity (Integer, v) -> TreeMap v -> Identity (Integer, v)
precise closestSoFar Leaf = closestSoFar
precise closestSoFar (Node k v l r) = case i `compare` k of
  LT -> precise closestSoFar l
  EQ -> Identity (k, v)
  GT -> precise (Identity (k, v)) r

Ceux-ci peuvent être unifiés en une version polymorphe dans Applicative:

precise :: (Applicative f) => f (Integer, v) -> TreeMap v -> f (Integer, v)
precise closestSoFar Leaf = closestSoFar
precise closestSoFar (Node k v l r) = case i `compare` k of
  LT -> precise closestSoFar l
  EQ -> pure (k, v)
  GT -> precise (pure (k, v)) r

En soi, cela n'accomplit pas grand-chose, mais si nous savons que la GTbranche retournera toujours une valeur, nous pouvons la forcer à s'exécuter dans le Identityfoncteur, quel que soit le foncteur de départ. Autrement dit, nous pouvons commencer dans le Maybefoncteur mais rentrer dans le Identityfoncteur dans la GTbranche:

closestLess :: Integer -> TreeMap v -> Maybe (Integer, v)
closestLess i = precise Nothing
  where
    precise :: (Applicative t) => t (Integer, v) -> TreeMap v -> t (Integer, v)
    precise closestSoFar Leaf = closestSoFar
    precise closestSoFar (Node k v l r) = case i `compare` k of
      LT -> precise closestSoFar l
      EQ -> pure (k, v)
      GT -> pure . runIdentity $ precise (Identity (k, v)) r

Cela fonctionne bien avec votre cas de test:

> isJust $ closestLess 5 (Node 3 () Leaf undefined)
True

et est un bel exemple de récursion polymorphe.

Une autre bonne chose à propos de cette approche du point de vue des performances est que cela -ddump-simplmontre qu'il n'y a pas de wrappers ou de dictionnaires. Tout a été effacé au niveau du type avec des fonctions spécialisées pour les deux foncteurs:

closestLess
  = \ @ v i eta ->
      letrec {
        $sprecise
        $sprecise
          = \ @ v1 closestSoFar ds ->
              case ds of {
                Leaf -> closestSoFar;
                Node k v2 l r ->
                  case compareInteger i k of {
                    LT -> $sprecise closestSoFar l;
                    EQ -> (k, v2) `cast` <Co:5>;
                    GT -> $sprecise ((k, v2) `cast` <Co:5>) r
                  }
              }; } in
      letrec {
        $sprecise1
        $sprecise1
          = \ @ v1 closestSoFar ds ->
              case ds of {
                Leaf -> closestSoFar;
                Node k v2 l r ->
                  case compareInteger i k of {
                    LT -> $sprecise1 closestSoFar l;
                    EQ -> Just (k, v2);
                    GT -> Just (($sprecise ((k, v2) `cast` <Co:5>) r) `cast` <Co:4>)
                  }
              }; } in
      $sprecise1 Nothing eta
KA Buhr
la source
2
Ceci est une solution assez cool
luqui
3

À partir de mon implémentation non paresseuse, j'ai d'abord refactorisé precisepour recevoir Justcomme argument, et généralisé son type en conséquence:

data TreeMap v = Leaf | Node Integer v (TreeMap v) (TreeMap v) deriving (Show, Read, Eq, Ord)

closestLess :: Integer -> TreeMap v -> Maybe (Integer, v)
closestLess i = precise Just Nothing where
  precise :: ((Integer, v) -> t) -> t -> TreeMap v -> t
  precise _ closestSoFar Leaf = closestSoFar
  precise wrap closestSoFar (Node k v l r) = case i `compare` k of
    LT -> precise wrap closestSoFar l
    EQ -> wrap (k, v)
    GT -> precise wrap (wrap (k, v)) r

Ensuite, je l'ai changé pour le faire wraptôt et je m'appelle avec iddans le GTcas:

data TreeMap v = Leaf | Node Integer v (TreeMap v) (TreeMap v) deriving (Show, Read, Eq, Ord)

closestLess :: Integer -> TreeMap v -> Maybe (Integer, v)
closestLess i = precise Just Nothing where
  precise :: ((Integer, v) -> t) -> t -> TreeMap v -> t
  precise _ closestSoFar Leaf = closestSoFar
  precise wrap closestSoFar (Node k v l r) = case i `compare` k of
    LT -> precise wrap closestSoFar l
    EQ -> wrap (k, v)
    GT -> wrap (precise id (k, v) r)

Cela fonctionne toujours comme avant, sauf au profit de la paresse supplémentaire.

Joseph Sible-Reinstate Monica
la source
1
Tous ces ids au milieu entre Justet la finale sont-ils (k,v)éliminés par le compilateur? probablement pas, les fonctions sont censées être opaques, et vous auriez pu (de manière faisable) utiliser à la first (1+)place de idtout ce que le compilateur sait. mais cela fait un code compact ... bien sûr, mon code est le démêlage et la spécification du vôtre ici, avec la simplification supplémentaire (l'élimination des ids). aussi très intéressant de voir comment le type plus général sert de contrainte, une relation entre les valeurs impliquées (pas assez serrées cependant, avec l' first (1+)autorisation de wrap).
Will Ness
1
(suite) votre polymorphe preciseest utilisé à deux types, correspondant directement aux deux fonctions spécialisées utilisées dans la variante la plus verbeuse. belle interaction là-bas. De plus, je n'appellerais pas ce CPS, wrapn'est pas utilisé comme une continuation, il n'est pas construit "à l'intérieur", il est empilé - par récursivité - à l'extérieur. Peut-être que s'il était utilisé comme continuation, vous pourriez vous débarrasser de ces ids superflus ... btw nous pouvons voir ici encore une fois cet ancien modèle d'argument fonctionnel utilisé comme indicateur de ce qu'il faut faire, en basculant entre les deux modes d'action ( Justou id).
Will Ness
3

Je pense que la version CPS à laquelle vous avez répondu vous-même est la meilleure, mais pour être complet, voici quelques idées supplémentaires. (EDIT: la réponse de Buhr est maintenant la plus performante.)

La première idée est de se débarrasser de l' closestSoFaraccumulateur " " et de laisser le GTcas gérer toute la logique de choisir la valeur la plus à droite la plus petite que l'argument. Sous cette forme, le GTboîtier peut renvoyer directement un Just:

closestLess1 :: Integer -> TreeMap v -> Maybe (Integer, v)
closestLess1 _ Leaf = Nothing
closestLess1 i (Node k v l r) =
  case i `compare` k of
    LT -> closestLess1 i l
    EQ -> Just (k, v)
    GT -> Just (fromMaybe (k, v) (closestLess1 i r))

C'est plus simple, mais prend un peu plus d'espace sur la pile lorsque vous rencontrez de nombreux GTcas. Techniquement, vous pouvez même l'utiliser fromMaybesous la forme d'un accumulateur (c'est-à-dire remplacer l' fromJustimplicite dans la réponse de luqui), mais ce serait une branche redondante et inaccessible.

L'autre idée qu'il y a vraiment deux "phases" de l'algorithme, une avant et une après avoir frappé un GT, donc vous le paramétrez par un booléen pour représenter ces deux phases, et utilisez des types dépendants pour coder l'invariant qu'il y aura toujours un aboutir à la deuxième phase.

data SBool (b :: Bool) where
  STrue :: SBool 'True
  SFalse :: SBool 'False

type family MaybeUnless (b :: Bool) a where
  MaybeUnless 'True a = a
  MaybeUnless 'False a = Maybe a

ret :: SBool b -> a -> MaybeUnless b a
ret SFalse = Just
ret STrue = id

closestLess2 :: Integer -> TreeMap v -> Maybe (Integer, v)
closestLess2 i = precise SFalse Nothing where
  precise :: SBool b -> MaybeUnless b (Integer, v) -> TreeMap v -> MaybeUnless b (Integer, v)
  precise _ closestSoFar Leaf = closestSoFar
  precise b closestSoFar (Node k v l r) = case i `compare` k of
    LT -> precise b closestSoFar l
    EQ -> ret b (k, v)
    GT -> ret b (precise STrue (k, v) r)
Li-yao Xia
la source
Je n'ai pas pensé à ma réponse en tant que CPS jusqu'à ce que vous la signaliez. Je pensais à quelque chose de plus proche d'une transformation wrapper ouvrier. Je suppose que Raymond Chen frappe à nouveau!
Joseph Sible-Reinstate Monica
2

Que diriez-vous

GT -> let Just v = precise (Just (k,v) r) in Just v

?

luqui
la source
Parce que c'est une correspondance de modèle incomplète. Même si ma fonction est un tout est total, je n'aime pas que des morceaux soient partiels.
Joseph Sible-Reinstate Monica
Vous avez donc dit "nous savons avec certitude", toujours avec un certain doute. C'est peut-être sain.
luqui
Nous le savons avec certitude, étant donné que mon deuxième bloc de code dans ma question revient toujours Justmais est total. Je sais que votre solution telle qu'elle est écrite est en fait totale, mais elle est fragile dans la mesure où une modification apparemment sûre pourrait alors entraîner un creux.
Joseph Sible-Reinstate Monica
Cela ralentira également légèrement le programme, car GHC ne peut pas prouver qu'il le sera toujours Just, il ajoutera donc un test pour s'assurer que ce n'est pas à Nothingchaque fois qu'il se répète.
Joseph Sible-Reinstate Monica
1

Non seulement nous savons toujours Just, après sa première découverte, nous savons aussi toujours Nothing jusque- là. C'est en fait deux "logiques" différentes.

Donc, nous allons d'abord à gauche, alors expliquons cela :

data TreeMap v = Leaf | Node Integer v (TreeMap v) (TreeMap v) 
                 deriving (Show, Read, Eq, Ord)

closestLess :: Integer 
            -> TreeMap v 
            -> Maybe (Integer, v)
closestLess i = goLeft 
  where
  goLeft :: TreeMap v -> Maybe (Integer, v)
  goLeft n@(Node k v l _) = case i `compare` k of
          LT -> goLeft l
          _  -> Just (precise (k, v) n)
  goLeft Leaf = Nothing

  -- no more maybe if we're here
  precise :: (Integer, v) -> TreeMap v -> (Integer, v)
  precise closestSoFar Leaf           = closestSoFar
  precise closestSoFar (Node k v l r) = case i `compare` k of
        LT -> precise closestSoFar l
        EQ -> (k, v)
        GT -> precise (k, v) r

Le prix est que nous répétons au plus une étape au plus une fois.

Will Ness
la source