인스턴스가 재귀 데이터 유형 인 유형 클래스에 대해 패턴 일치를 패턴 화하는 방법은 무엇입니까?

이 질문은 typeclass 값에 대한 패턴 일치 방법 에 대한 후속 조치입니다 . .

저는 1 차 논리로 애완 동물 프로젝트를 시작하고 있으며이를 위해 Haskell을 사용하기로 결정했습니다. 내 첫 번째 장애물은 '1 차 논리 공식'을 정의하는 것이므로 데이터 유형은 다음과 같습니다.

data Formula v  = Belong v v                      -- x in y
                | Bot                             -- False
                | Imply (Formula v) (Formula v)   -- p -> q
                | Forall v (Formula v)            -- forall x, p

그러나 구현 세부 사항을 기반으로 코드를 작성하는 것을 꺼리고 마음이 바뀌거나 대체 구현으로 기능을 재사용하려는 경우 유형 클래스를 사용하여 세부 정보를 추상화하고 싶습니다.

class FirstOrder m where
  belong    :: v -> v -> m v
  bot       :: m v
  imply     :: m v -> m v -> m v
  forall    :: v -> m v -> m v
  asFormula :: m v -> Formula v

(위 링크에서 제안한 asFormula대로)을 ViewPatterns( 를) 사용하기 위해 마지막 함수 를 추가 하여이 유형 클래스의 값에 대한 패턴 일치를 수행 할 수 있습니다.

이제 간단한 함수를 정의하고 싶다고 가정합니다.

subst :: (FirstOrder m) => (v -> w) -> m v -> m w

소정의 맵핑에 따라 식의 변수되는 대체품 f::v -> w(Feel로 좋아 fmap) 화학식 그래서 belong x y에 매핑 belong (f x) (f y)등을 사용하여 다음 ViewPatterns:

subst f (asFormula -> Belong x y) = belong (f x) (f y)

여태까지는 그런대로 잘됐다...

그러나 쓰려고 할 때 subst f p->q = (subst f p) -> (subst f q):

subst f (asFormula -> Imply p q)  = imply (subst f p) (subst f q)

패턴 매칭 바인딩 : 나는 그것을 생각 오는 유형의 오류가 완벽한 의미가 얻을 수 p및 q유형의 요소에 Formula v원하는 형식에 반대 m v.

이제 문제를 볼 수 fromFormula있으며 유형 클래스에 함수를 추가 하여 유형으로 다시 변환 하여 문제를 해결하는 방법을 생각할 수도 m v있지만 성능 관점에서 보면 이것이 미쳤다고 asFormula생각합니다. ), 코드를 일반화하기 위해 지불해야하는 엄청난 대가입니다.

그래서 지금은 자유 대수 (재귀 적 데이터 유형)에 대한 구조적 재귀에 의해 간단한 함수를 정의하려고하지만, 구현 세부 사항을 추상화하고 (데이터 유형이 아닌 유형 클래스에서 코드를 작성하려는) 욕구는 불가능한 입장 인 것 같습니다.

탈출구가 있습니까, 아니면 추상화를 잊고 재귀 데이터 유형으로 작업해야합니까?