Fermeture À Glissière Comonads, De Manière Générique

Question

Compte tenu de tout type de conteneur on peut former la (l'élément qui a le focus) fermeture à Glissière et de savoir que cette structure est un Comonad. Cela a été récemment exploré en détail merveilleux dans un autre Débordement de Pile question pour le type suivant:

data Bin a = Branch (Bin a) a (Bin a) | Leaf a deriving Functor

à la suite de fermeture à glissière

data Dir = L | R
data Step a = Step a Dir (Bin a)   deriving Functor
data Zip  a = Zip [Step a] (Bin a) deriving Functor
instance Comonad Zip where ...

C'est le cas qu' Zip est Comonad si la construction de son instance est un peu poilue. Cela dit, Zip peut être complètement mécanique dérivée de l' Tree et (je crois) tout autre type dérivé de cette façon est automatiquement Comonad, donc je pense que cela devrait être le cas, que nous pouvons construire ces types et leur comonads de façon générique et automatiquement.

Une méthode pour atteindre la généralité pour fermeture à glissière de la construction est l'utilisation de la classe suivante et le type de famille

data Zipper t a = Zipper { diff :: D t a, here :: a }

deriving instance Diff t => Functor (Zipper t)

class (Functor t, Functor (D t)) => Diff t where
  data D t :: * -> *
  inTo  :: t a -> t (Zipper t a)
  outOf :: Zipper t a -> t a

qui a (plus ou moins) représentée en Haskell Café threads et sur Conal Elliott blog. Cette classe peut être instancié pour les différentes base algébrique de types et fournit ainsi un cadre général pour parler des produits dérivés de ADTs.

Donc, en fin de compte, ma question est de savoir si ou non nous pouvons écrire

instance Diff t => Comonad (Zipper t) where ...

qui pourrait être utilisé pour subsumer spécifiques Comonad exemple décrit ci-dessus:

instance Diff Bin where
  data D Bin a = DBin { context :: [Step a], descend :: Maybe (Bin a, Bin a) }
  ...

Malheureusement, je n'ai pas eu la chance de l'écriture d'une telle instance. Est l' inTo/outOf signature est-elle suffisante? Est-il quelque chose de nécessaire pour contraindre les types? Est-ce de l'instance même possible?

Answer 1

L' Comonad exemple pour fermetures à glissière est pas

instance (Diff t, Diff (D t)) => Comonad (Zipper t) where
    extract = here
    duplicate = fmap outOf . inTo

où outOf et inTo viennent de l' Diff exemple pour Zipper t lui-même. L'exemple ci-dessus viole l' Comonad droit fmap extract . duplicate == id. Au lieu de cela, il se comporte comme:

fmap extract . duplicate == \z -> fmap (const (here z)) z

Diff (fermeture à Glissière t)

L' Diff exemple pour Zipper est fourni par les identifiant comme des produits et de réutiliser le code pour les produits (ci-dessous).

-- Zippers are themselves products
toZipper :: (D t :*: Identity) a -> Zipper t a
toZipper (d :*: (Identity h)) = Zipper d h

fromZipper :: Zipper t a -> (D t :*: Identity) a
fromZipper (Zipper d h) = (d :*: (Identity h))

Étant donné un isomorphisme entre les types de données, et un isomorphisme entre leurs dérivés, on peut réutiliser un type de l' inTo et outOf pour les autres.

inToFor' :: (Diff r) =>
            (forall a.   r a ->   t a) ->
            (forall a.   t a ->   r a) ->
            (forall a. D r a -> D t a) ->
            (forall a. D t a -> D r a) ->
            t a -> t (Zipper t a)
inToFor' to from toD fromD = to . fmap (onDiff toD) . inTo . from

outOfFor' :: (Diff r) =>
            (forall a.   r a ->   t a) ->
            (forall a.   t a ->   r a) ->
            (forall a. D r a -> D t a) ->
            (forall a. D t a -> D r a) ->
            Zipper t a -> t a
outOfFor' to from toD fromD = to . outOf . onDiff fromD

Pour les types qui sont juste newTypes pour un Diff de l'instance, de leurs dérivés sont du même type. Si nous dire le type de correcteur sujet de l'égalité de traitement D r ~ D t, nous pouvons en profiter au lieu de fournir un isomorphisme pour les dérivés.

inToFor :: (Diff r, D r ~ D t) =>
           (forall a. r a -> t a) ->
           (forall a. t a -> r a) ->
           t a -> t (Zipper t a)
inToFor to from = inToFor' to from id id

outOfFor :: (Diff r, D r ~ D t) =>
            (forall a. r a -> t a) ->
            (forall a. t a -> r a) ->
            Zipper t a -> t a
outOfFor to from = outOfFor' to from id id

Grâce à ces outils, on peut réutiliser l' Diff exemple pour les produits à mettre en oeuvre Diff (Zipper t)

-- This requires undecidable instances, due to the need to take D (D t)
instance (Diff t, Diff (D t)) => Diff (Zipper t) where
    type D (Zipper t) = D ((D t) :*: Identity)
    -- inTo :: t        a -> t        (Zipper  t         a)
    -- inTo :: Zipper t a -> Zipper t (Zipper (Zipper t) a)
    inTo = inToFor toZipper fromZipper
    -- outOf :: Zipper  t         a -> t        a
    -- outOf :: Zipper (Zipper t) a -> Zipper t a
    outOf = outOfFor toZipper fromZipper

Réutilisable

Pour utiliser le code présenté ici, nous avons besoin de quelques extensions de langage, les importations, et une reformulation de la proposition de problème.

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}

import Control.Monad.Identity
import Data.Proxy
import Control.Comonad

data Zipper t a = Zipper { diff :: D t a, here :: a }

onDiff :: (D t a -> D u a) -> Zipper t a -> Zipper u a
onDiff f (Zipper d a) = Zipper (f d) a

deriving instance Diff t => Functor (Zipper t)
deriving instance (Eq (D t a), Eq a) => Eq (Zipper t a)
deriving instance (Show (D t a), Show a) => Show (Zipper t a)

class (Functor t, Functor (D t)) => Diff t where
  type D t :: * -> *
  inTo  :: t a -> t (Zipper t a)
  outOf :: Zipper t a -> t a

Produits, Sommes et Constantes

L' Diff (Zipper t) instance s'appuie sur des implémentations de Diff pour les produits :*:, les sommes :+:, les constantes Identity, et zéro Proxy.

data (:+:) a b x = InL (a x) | InR (b x)
    deriving (Eq, Show)
data (:*:) a b x = a x :*: b x
    deriving (Eq, Show)

infixl 7 :*:
infixl 6 :+:

deriving instance (Functor a, Functor b) => Functor (a :*: b)

instance (Functor a, Functor b) => Functor (a :+: b) where
    fmap f (InL a) = InL . fmap f $ a
    fmap f (InR b) = InR . fmap f $ b


instance (Diff a, Diff b) => Diff (a :*: b) where
    type D (a :*: b) = D a :*: b :+: a :*: D b
    inTo (a :*: b) = 
        (fmap (onDiff (InL . (:*: b))) . inTo) a :*:
        (fmap (onDiff (InR . (a :*:))) . inTo) b
    outOf (Zipper (InL (a :*: b)) x) = (:*: b) . outOf . Zipper a $ x
    outOf (Zipper (InR (a :*: b)) x) = (a :*:) . outOf . Zipper b $ x

instance (Diff a, Diff b) => Diff (a :+: b) where
    type D (a :+: b) = D a :+: D b
    inTo (InL a) = InL . fmap (onDiff InL) . inTo $ a
    inTo (InR b) = InR . fmap (onDiff InR) . inTo $ b
    outOf (Zipper (InL a) x) = InL . outOf . Zipper a $ x
    outOf (Zipper (InR a) x) = InR . outOf . Zipper a $ x

instance Diff (Identity) where
    type D (Identity) = Proxy
    inTo = Identity . (Zipper Proxy) . runIdentity
    outOf = Identity . here

instance Diff (Proxy) where
    type D (Proxy) = Proxy
    inTo = const Proxy
    outOf = const Proxy

Bin Exemple

J'ai posé la Bin exemple comme un isomorphisme pour une somme de produits. Nous avons besoin non seulement de ses dérivés, mais sa dérivée seconde ainsi

newtype Bin   a = Bin   {unBin   ::      (Bin :*: Identity :*: Bin :+: Identity)  a}
    deriving (Functor, Eq, Show)
newtype DBin  a = DBin  {unDBin  ::    D (Bin :*: Identity :*: Bin :+: Identity)  a}
    deriving (Functor, Eq, Show)
newtype DDBin a = DDBin {unDDBin :: D (D (Bin :*: Identity :*: Bin :+: Identity)) a}
    deriving (Functor, Eq, Show)

instance Diff Bin where
    type D Bin = DBin
    inTo  = inToFor'  Bin unBin DBin unDBin
    outOf = outOfFor' Bin unBin DBin unDBin

instance Diff DBin where
    type D DBin = DDBin
    inTo  = inToFor'  DBin unDBin DDBin unDDBin
    outOf = outOfFor' DBin unDBin DDBin unDDBin

L'exemple des données de la réponse précédente est

aTree :: Bin Int    
aTree =
    (Bin . InL) (
        (Bin . InL) (
            (Bin . InR) (Identity 2)
            :*: (Identity 1) :*:
            (Bin . InR) (Identity 3)
        )
        :*: (Identity 0) :*:
        (Bin . InR) (Identity 4)
    )

Pas le Comonad exemple

L' Bin exemple ci-dessus fournit un contre-exemple pour fmap outOf . inTo étant la mise en œuvre correcte de l' duplicate pour Zipper t. En particulier, il fournit un contre-exemple pour l' fmap extract . duplicate = id loi:

fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree

Ce qui donne (remarquez comment il est plein d' Falses partout, tout False serait suffisant pour réfuter la loi)

Bin {unBin = InL ((Bin {unBin = InL ((Bin {unBin = InR (Identity False)} :*: Identity False) :*: Bin {unBin = InR (Identity False)})} :*: Identity False) :*: Bin {unBin = InR (Identity False)})}

inTo aTree est un arbre avec la même structure que l' aTree, mais partout il y a une valeur, il s'agit plutôt d'une fermeture à glissière avec la valeur, et le reste de l'arbre avec toutes les valeurs d'origine intact. fmap (fmap extract . duplicate) . inTo $ aTree est aussi un arbre avec la même structure que l' aTree, mais everywere il y avait une valeur, il s'agit plutôt d'une fermeture à glissière avec la valeur, et le reste de l'arbre avec toutes les valeurs remplacé avec la même valeur. En d'autres termes:

fmap extract . duplicate == \z -> fmap (const (here z)) z

La suite de tests complète pour tous les trois - Comonad lois, extract . duplicate == id, fmap extract . duplicate == id, et duplicate . duplicate == fmap duplicate . duplicate est

main = do
    putStrLn "fmap (\\z -> (extract . duplicate) z == z) . inTo $ aTree"
    print   . fmap ( \z -> (extract . duplicate) z == z) . inTo $ aTree    
    putStrLn ""
    putStrLn  "fmap (\\z -> (fmap extract . duplicate) z == z) . inTo $ aTree"
    print    . fmap ( \z -> (fmap extract . duplicate) z == z) . inTo $ aTree    
    putStrLn ""
    putStrLn "fmap (\\z -> (duplicate . duplicate) z) == (fmap duplicate . duplicate) z) . inTo $ aTree"
    print   . fmap ( \z -> (duplicate . duplicate) z == (fmap duplicate . duplicate) z) . inTo $ aTree

Answer 2

Compte tenu de l'infiniment dérivable Diff classe:

class (Functor t, Functor (D t)) => Diff t where
    type D t :: * -> *
    up :: Zipper t a -> t a
    down :: t a -> t (Zipper t a)  
    -- Require that types be infinitely differentiable
    ddiff :: p t -> Dict (Diff (D t))

around peut être écrite en termes de up et down sur le Zippers' diffs'derivitive, essentiellement

around z@(Zipper d h) = Zipper ctx z
    where
        ctx = fmap (\z' -> Zipper (up z') (here z')) (down d)

L' Zipper t a se compose d'un D t a et a. Nous allons down le D t a, l'obtention d'un D t (Zipper (D t) a) avec une fermeture à glissière dans tous les trous. Ces fermetures se compose d'un D (D t) a et de la a qui était dans le trou. Nous allons up chacun d'eux, l'obtention d'un D t a et à éplucher avec l' a qui était dans le trou. Un D t a et a faire Zipper t a, de nous donner un D t (Zipper t a), qui est le cadre nécessaire pour un Zipper t (Zipper t a).

L' Comonad exemple est alors simplement

instance Diff t => Comonad (Zipper t) where
    extract   = here
    duplicate = around

La capture de l'instrument dérivé Diff dictionnaire demande un peu plus de la plomberie, qui peut être fait avec les Données.Contrainte ou de la méthode présentée dans une réponse

around :: Diff t => Zipper t a -> Zipper t (Zipper t a)
around z = Zipper (withDict d' (fmap (\z' -> Zipper (up z') (here z')) (down (diff z)))) z
    where
        d' = ddiff . p' $ z
        p' :: Zipper t x -> Proxy t
        p' = const Proxy