Rekursywne przejście w dół algebraicznych typów danych

Question

W przypadku zajmowania się sporymi algebraicznymi typami danych w Haskell, istnieje szczególne przechodzenie rekursywne nie przechwycone przez zagięcie na typ danych. Na przykład załóżmy, że mam prosty typ danych reprezentujący formuł rachunku zdań i krotnie zdefiniowaną nad nim:

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' ψ) 

Ten schemat rekursji zapewnia zwięzłą odpowiedź rekursji jak ewaluacyjnych lub znalezienie literałów:

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) 

Jednak nie jest tak dobrze, gdy chcę "zamiatać" typ danych. W dalszej SIMP jest funkcją pomocniczy określa odpowiedni wzorzec dopasowywania:

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 φ   = φ 

Stosując krotnie zdefiniować uproszczenia oczywiście powoduje nieprawidłowe wyniki. Na przykład, następujący nie jest równoważne:

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

Co jest najlepszym rozwiązaniem do rekursji jak uprościć? Czy należy zdefiniować ogólne przejście podobne do złożenia dla typu danych, czy też istnieje standardowy wzorzec rekursji do definiowania takich funkcji?

Answer 1

Czy próbowałeś Uniplate? W przypadku operacji, które działają tylko na jednym typie, może wykonywać od nowa zapisywanie i przepisywanie do określonego punktu.

Na przykład:

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" 

Odpowiednie funkcje dla jesteś transform i rewrite.

Aby uzyskać bardziej szczegółową dokumentację na temat Uniplate, istnieje również a paper (PDF).