Recorrido recursivo de abajo hacia arriba de tipos de datos algebraicos

Question

Al tratar con tipos de datos algebraicos considerables en Haskell, hay un recorrido recursivo particular no capturado al plegar sobre el tipo de datos. Por ejemplo, supongamos que tengo un tipo simple de datos que representa las fórmulas en la lógica de proposiciones, y un pliegue definido sobre él:

type FAlgebra α φ = 
(φ, φ,    -- False, True 
    α -> φ,    -- Atom 
    φ -> φ,    -- Negation 
    φ -> φ -> φ,   -- Conjunction 
    φ -> φ -> φ,   -- Disjunction 
    φ -> φ -> φ,   -- Implication 
    φ -> φ -> φ)   -- Bi-implication 

fold :: FAlgebra α φ -> Form α -> φ 
fold (f,t,lit,not,con,dis,imp,iff) = fold' where 
fold' (Fls)  = f 
fold' (Tru)  = t 
fold' (Lit α) = lit α 
fold' (Not φ) = not (fold' φ) 
fold' (Con φ ψ) = con (fold' φ) (fold' ψ) 
fold' (Dis φ ψ) = dis (fold' φ) (fold' ψ) 
fold' (Imp φ ψ) = imp (fold' φ) (fold' ψ) 
fold' (Iff φ ψ) = iff (fold' φ) (fold' ψ) 

Este esquema de recursión proporciona una respuesta sucinta a recursiones como de evaluación o la búsqueda de literales:

eval :: (Ord α) => Map α Bool -> Form α -> Bool 
eval v = fold (False, True, (fromJust . flip M.lookup v), 
       not, (&&), (||), ((||) . not), (==)) 

literals :: (Ord α) => Form α -> Set α 
literals = fold (S.empty, S.empty, S.singleton, id, 
       S.union, S.union, S.union, S.union) 

Sin embargo, no funciona tan bien cuando deseo "barrer" el tipo de datos. En lo siguiente, Simp es una función auxiliar definida por necesario de patrones:

simplify :: Form α -> Form α 
simplify (Not φ) = simp (Not (simplify φ)) 
simplify (Con φ ψ) = simp (Con (simplify φ) (simplify ψ)) 
simplify (Dis φ ψ) = simp (Dis (simplify φ) (simplify ψ)) 
simplify (Imp φ ψ) = simp (Imp (simplify φ) (simplify ψ)) 
simplify (Iff φ ψ) = simp (Imp (simplify φ) (simplify ψ)) 
simplify φ   = φ 

Uso de un pliegue para definir simplificar, por supuesto, genera resultados incorrectos. Por ejemplo, lo siguiente no es equivalente:

simplify = fold (Fls, Tru, Lit, (simp . Not), con Con, con Dis, con Imp, con Iff) 
where con f φ ψ = simp (f φ ψ) 

¿Cuál es la mejor solución para simplificar recursividad como ? ¿Debo definir un cruce genérico similar al doblez sobre el tipo de datos, o hay un patrón de recursión estándar para definir tales funciones?

Answer 1

¿Has probado Uniplate? Para las operaciones que solo funcionan en un solo tipo, puede realizar reescrituras y reescrituras de abajo arriba hasta un punto fijo.

Por ejemplo:

import Data.Generics.Uniplate.Direct 
import qualified Data.Map as M 

data Form a = Fls | Tru | Lit a 
      | Not (Form a) 
      | Con (Form a) (Form a) 
      | Dis (Form a) (Form a) 
      -- etc. 
    deriving (Show, Eq) 

instance Uniplate (Form a) where 
    uniplate (Not f) = plate Not |* f 
    uniplate (Con f1 f2) = plate Con |* f1 |* f2 
    uniplate (Dis f1 f2) = plate Dis |* f1 |* f2 
    -- one case for each constructor that may contain nested (Form a)s 
    uniplate x = plate x 

simplify :: Form a -> Form a 
simplify = transform simp 
where 
    simp (Not (Not f)) = f 
    simp (Not Fls) = Tru 
    simp (Not Tru) = Fls 
    simp x = x 

test = 
    simplify (Not (Not (Not (Not (Lit "a"))))) == Lit "a" 

Las funciones relevantes para usted son transform y rewrite.

Para obtener una documentación más detallada acerca de Uniplate también hay a paper (PDF).