Est-ce que chaque type a un catamorphisme unique?

Question

Récemment j'ai finalement commencé à sentir que je comprenais les catamorphismes. J'en ai écrit quelques-unes dans a recent answer, mais brièvement je dirais un catamorphisme pour un type abstrait sur le processus de traverser récursivement une valeur de ce type, avec les correspondances de modèle sur ce type réifiées en une fonction pour chaque constructeur que le type a. Bien que j'accueillerais volontiers des corrections sur ce point ou sur la version plus longue dans la réponse de la mienne, je pense que je l'ai plus ou moins vers le bas et ce n'est pas le sujet de cette question, juste un peu de contexte. Une fois que j'ai réalisé que les fonctions que vous transmettez à un catamorphisme correspondent exactement aux constructeurs du type, et que les arguments de ces fonctions correspondent également aux types de champs de ces constructeurs, tout se sent soudain tout à fait mécanique et je ne le sais pas. voir où il y a une marge de manœuvre pour des implémentations alternatives. Par exemple, j'ai juste inventé ce type stupide, sans vraiment le concept de ce que sa structure signifie ", et en a dérivé un catamorphisme. Je ne vois pas d'autre façon que je pourrais définir un objectif général pli sur ce type:

data X a b f = A Int b 
      | B 
      | C (f a) (X a b f) 
      | D a 

xCata :: (Int -> b -> r) 
     -> r 
     -> (f a -> r -> r) 
     -> (a -> r) 
     -> X a b f 
     -> r 
xCata a b c d v = case v of 
    A i x -> a i x 
    B -> b 
    C f x -> c f (xCata a b c d x) 
    D x -> d x 

Ma question est, est-tous les types ont une catamorphisme unique (à réordonner argument)? Ou y a-t-il des contre-exemples: types pour lesquels aucun catamorphisme ne peut être défini, ou types pour lesquels existent deux catamorphismes distincts mais également raisonnables? S'il n'y a pas de contre-exemples (c.-à-d., Le catamorphisme pour un type est unique et trivialement dérivable), est-il possible de faire en sorte que GHC dérive pour moi une sorte de classe de type automatiquement?

Answer 1

Le catamorphisme associé à un type récursif peut être dérivé mécaniquement. Supposons que vous ayez un type récursif défini, ayant plusieurs constructeurs, chacun avec sa propre arité. Je vais emprunter l'exemple d'OP. Ensuite, nous pouvons réécrire le même type en forçant chaque arité à être un, sans le tout. L'arité zéro (B) devient un si nous ajoutons un type d'unité ().

data X a b f = A (Int, b) 
      | B() 
      | C (f a, X a b f) 
      | D a 

Ensuite, nous pouvons réduire le nombre de constructeurs à l'un, l'exploitation Either au lieu de plusieurs constructeurs. Ci-dessous, nous écrivons simplement l'infixe + au lieu de Either par souci de concision.

data X a b f = X ((Int, b) +() + (f a, X a b f) + a) 

Au terme de niveau, nous savons que nous pouvons réécrire toute définition récursive comme la forme x = f x where f w = ..., écrire une équation de point fixe explicite x = f x. Au niveau du type, nous pouvons utiliser la même méthode pour réécrire les types récursifs.

data X a b f = X (F (X a b f)) -- fixed point equation 
data F a b f w = F ((Int, b) +() + (f a, w) + a) 

Maintenant, nous remarquons que nous pouvons autodériver une instance de foncteur.

deriving instance Functor (F a b f) 

Ceci est possible parce que dans le type d'origine que chaque référence récursive a eu lieu dans la position positif. Si cela ne tient pas, en faisant F a b f pas un foncteur, alors nous ne pouvons pas avoir un catamorphisme.

Enfin, nous pouvons écrire le type de cata comme suit:

cata :: (F a b f w -> w) -> X a b f -> w 

est ce type xCata de l'OP? C'est. Il suffit d'appliquer quelques isomorphismes de type. Nous utilisons les lois algébriques suivantes:

1) (a,b) -> c ~= a -> b -> c   (currying) 
2) (a+b) -> c ~= (a -> c, b -> c) 
3)() -> c ~= c 

Soit dit en passant, il est facile de se rappeler ces isomorphismes si nous écrivons (a,b) comme un produit a*b, unité () comme 1 et a->b comme une puissance b^a. En effet, ils deviennent 1) c^(a*b) = (c^a)^b , 2) c^(a+b) = c^a*c^b, 3) c^1 = c.

Quoi qu'il en soit, nous allons commencer à réécrire la partie F a b f w -> w, ne

F a b f w -> w 
=~ (def F) 
    ((Int, b) +() + (f a, w) + a) -> w 
=~ (2) 
    ((Int, b) -> w,() -> w, (f a, w) -> w, a -> w) 
=~ (3) 
    ((Int, b) -> w, w, (f a, w) -> w, a -> w) 
=~ (1) 
    (Int -> b -> w, w, f a -> w -> w, a -> w) 

Considérons le type complet maintenant:

cata :: (F a b f w -> w) -> X a b f -> w 
    ~= (above) 
     (Int -> b -> w, w, f a -> w -> w, a -> w) -> X a b f -> w 
    ~= (1) 
      (Int -> b -> w) 
     -> w 
     -> (f a -> w -> w) 
     -> (a -> w) 
     -> X a b f 
     -> w 

Ce qui est en effet (renommer w=r) le genre

xCata :: (Int -> b -> r) 
     -> r 
     -> (f a -> r -> r) 
     -> (a -> r) 
     -> X a b f 
     -> r 

L'implémentation "standard" de cata est

cata g = wrap . fmap (cata g) . unwrap 
    where unwrap (X y) = y 
     wrap y = X y 

Il faut un certain effort pour comprendre en raison de sa généralité, mais il en est bien celle prévue.

---

A propos de l'automatisation: oui, cela peut être automatisé, au moins en partie. Il y a le paquet recursion-schemes sur hackage qui permet d'écrire un quelque chose comme

type X a b f = Fix (F a f b) 
data F a b f w = ... -- you can use the actual constructors here 
     deriving Functor 

-- use cata here 

Exemple:

import Data.Functor.Foldable hiding (Nil, Cons) 

data ListF a k = NilF | ConsF a k deriving Functor 
type List a = Fix (ListF a) 

-- helper patterns, so that we can avoid to match the Fix 
-- newtype constructor explicitly  
pattern Nil = Fix NilF 
pattern Cons a as = Fix (ConsF a as) 

-- normal recursion 
sumList1 :: Num a => List a -> a 
sumList1 Nil   = 0 
sumList1 (Cons a as) = a + sumList1 as 

-- with cata 
sumList2 :: forall a. Num a => List a -> a 
sumList2 = cata h 
    where 
    h :: ListF a a -> a 
    h NilF  = 0 
    h (ConsF a s) = a + s 

-- with LambdaCase 
sumList3 :: Num a => List a -> a 
sumList3 = cata $ \case 
    NilF  -> 0 
    ConsF a s -> a + s