Truy nhập ngược từ dưới lên đệ quy của các kiểu dữ liệu đại số

Question

Khi xử lý các kiểu dữ liệu đại số lớn trong Haskell, có một quá trình truyền đệ quy cụ thể không được chụp bằng cách gấp trên kiểu dữ liệu. Ví dụ, giả sử tôi có một kiểu dữ liệu đơn giản đại diện cho công thức trong logic mệnh đề, và một lần được xác định trên nó:

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

chương trình đệ quy này cung cấp một câu trả lời ngắn gọn để recursions như đánh giá hoặc tìm literals:

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) 

Tuy nhiên, nó không quá tốt khi tôi muốn "quét" loại dữ liệu. Trong phần sau, simp là một hàm phụ được xác định bởi khớp mẫu phù hợp:

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

Sử dụng một lần để xác định đơn giản, tất nhiên, tạo ra kết quả không chính xác. Ví dụ, sau đây không phải là tương đương:

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

giải pháp tốt nhất để recursions như là gì đơn giản hóa? Tôi có nên xác định một traversal chung tương tự như gấp trên các loại dữ liệu, hoặc là có một mô hình đệ quy chuẩn để xác định các chức năng như vậy?

Answer 1

Bạn đã thử Uniplate? Đối với các hoạt động chỉ hoạt động trên một kiểu duy nhất, nó có thể thực hiện viết lại từ dưới lên và viết lại cho đến một điểm cố định.

Ví dụ:

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" 

Các chức năng liên quan cho bạn là transform và rewrite.

Để biết thêm tài liệu chuyên sâu về Uniplate, cũng có a paper (PDF).