Haskell правильные типы для класса и экземпляра

Question

Я пытаюсь описать, что значит переписать термины и литералы (логику первого порядка). Т.е. мне нужна функция applySubstitution, которую можно вызывать как по терминам, так и по литералам. Я думал, что замена может быть выражена как функция. Однако я получаю ошибки переменных жесткого типа со следующим кодом.

{-# LANGUAGE UnicodeSyntax #-}

module Miniexample where
import qualified Data.Maybe as M

data Term a = F a [Term a]
            | V a

data Literal a = P a [Term a]
               | E (Term a) (Term a)

class Substitutable b where
  substitute :: b -> (Term a -> Maybe (Term a)) -> b

instance Substitutable (Term a) where
  substitute x@(V _) σ    = M.fromMaybe x (σ x)
  substitute f@(F l xs) σ = M.fromMaybe f' (σ f)
    where f' = F l (map (flip substitute σ) xs)

instance Substitutable (Literal a) where
  substitute (P l xs) σ = P l (map (flip substitute σ) xs)
  substitute (E s t) σ  = E (substitute s σ) (substitute t σ)

class Substitution σ where
  asSub :: σ -> (a -> Maybe a)

applySubstitution σ t = substitute t (asSub σ)

(<|) t σ = applySubstitution σ t

Это дает следующую ошибку:

• Couldn't match type ‘a1’ with ‘a’
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      substitute :: forall a1.
                    Term a -> (Term a1 -> Maybe (Term a1)) -> Term a
    at /.../Miniexample.hs:16:3-12
  ‘a’ is a rigid type variable bound by
    the instance declaration
    at /.../Miniexample.hs:15:10-31
  Expected type: Term a1
    Actual type: Term a
• In the first argument of ‘σ’, namely ‘x’
  In the second argument of ‘M.fromMaybe’, namely ‘(σ x)’
  In the expression: M.fromMaybe x (σ x)
• Relevant bindings include
    σ :: Term a1 -> Maybe (Term a1)
      (bound at /.../Miniexample.hs:16:22)
    x :: Term a
      (bound at /.../Miniexample.hs:16:14)
    substitute :: Term a -> (Term a1 -> Maybe (Term a1)) -> Term a
      (bound at /.../Miniexample.hs:16:3)

В моей голове переменная типа b в классе Substitutable должна иметь возможность принимать (я уверен, плохая терминология) значение Term a.

Любые намеки приветствуются.

Чтобы дать более конкретный пример, работает следующее, но нужно четко указать, какую функцию applyTermSub или applyLitSub вызывать, а во-вторых, реализация карты замещения просочилась в реализацию более общей процедуры.

module Miniexample where
import qualified Data.Maybe as M
import qualified Data.List as L

data Term a = F a [Term a]
            | V a deriving (Eq)

data Literal a = P a [Term a]
               | E (Term a) (Term a) deriving (Eq)


termSubstitute :: (Term a -> Maybe (Term a)) -> Term a -> Term a
termSubstitute σ x@(V _)    = M.fromMaybe x (σ x)
termSubstitute σ f@(F l xs) = M.fromMaybe f' (σ f)
    where f' = F l (map (termSubstitute σ) xs)

litSubstitute :: (Term a -> Maybe (Term a)) -> Literal a -> Literal a
litSubstitute σ (P l xs) = P l (map (termSubstitute σ) xs)
litSubstitute σ (E s t)  = E (termSubstitute σ s) (termSubstitute σ t)

applyTermSub :: (Eq a) => Term a -> [(Term a, Term a)] -> Term a
applyTermSub t σ = termSubstitute (flip L.lookup σ) t

applyLitSub :: (Eq a) => Literal a -> [(Term a, Term a)] -> Literal a
applyLitSub l σ = litSubstitute (flip L.lookup σ) l

-- variables
x  = V "x"
y  = V "y"
-- constants
a  = F "a" []
b  = F "b" []
-- functions
fa = F "f" [a]
fx = F "f" [x]

σ = [(x,y), (fx, fa)]

test = (applyLitSub (P "p" [x, b, fx]) σ) == (P "p" [y, b, fa])

В идеале я хотел бы иметь интерфейс для подстановок (т. Е. Можно использовать Data.Map и т. Д.), А во-вторых, я хотел бы использовать одну функцию подстановки, которая захватывает и термин, и литералы.

Answer 1

Ошибка, которую вы получаете, является жалобой на то, что Term a, как указано в instance Substitutable (Term a), отличается от типа Term a, который принимает σ.Это связано с тем, что Haskell количественно определяет a по функции substitute, но не по остальной части определения экземпляра.Таким образом, реализация substitute должна принимать σ, который обрабатывает Term a1 для некоторого значения a1, которое не обязательно является конкретным a, на котором определен ваш экземпляр.(Да, ваш экземпляр определен для всех a ... но изнутри области определения экземпляра, это как если бы был выбран конкретный a.)

Вы можете избежать этого путем параметризацииваш класс Substitutable с помощью конструктора типов вместо просто типа и передачи в этот конструктор типа того же a, который используется в типе σ.

{-# LANGUAGE UnicodeSyntax #-}

import qualified Data.Maybe as M
import qualified Data.List as L

data Term a = F a [Term a]
            | V a deriving (Eq)

data Literal a = P a [Term a]
               | E (Term a) (Term a) deriving (Eq)

class Substitutable f where
  substitute :: f a -> (Term a -> Maybe (Term a)) -> f a

instance Substitutable Term where
  substitute x@(V _) σ    = M.fromMaybe x (σ x)
  substitute f@(F l xs) σ = M.fromMaybe f' (σ f)
    where f' = F l (map (flip substitute σ) xs)

instance Substitutable Literal where
  substitute (P l xs) σ = P l (map (flip substitute σ) xs)
  substitute (E s t) σ  = E (substitute s σ) (substitute t σ)

(<|) t σ = substitute t $ flip L.lookup σ


-- variables
x  = V "x"
y  = V "y"
-- constants
a  = F "a" []
b  = F "b" []
-- functions
fa = F "f" [a]
fx = F "f" [x]

σ = [(x,y), (fx, fa)]


main = print $ show $ (P "p" [x, b, fx] <| σ) == P "p" [y, b, fa]