Haskell correct types for class and instance

Question

I am struggling to describe what it means for terms and literals (first order logic) to be re-written. Ie I would like a function applySubstitution that can be called on both terms and literals. I thought that the substitution could be expressed as a function. However I am getting rigid type variable errors with the following code.

{-# 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

This gives be the following error:

• 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)

In my head, the type variable b in the Substitutable class should be able to take on (bad terminology I'm sure) the the value of Term a.

Any hints would be greatly welcome.

To give a more concrete example, the following works, but one needs to be explicit about which function applyTermSub or applyLitSub to call and secondly the implementation of the substitution map leaks into the implementation of the more general procedure.

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])

Ideally I would like to have an interface for substitutions (i.e one could use Data.Map etc) and secondly I would like a single substitute function that captures both term and literals.

user11228628 user11228628 · Accepted Answer · 2019-04-30T18:35:14

The error you're getting is a complaint that Term a, as specified in instance Substitutable (Term a), is not the same type as the Term a that σ accepts. This is because Haskell quantifies a over the substitute function, but not over the rest of the instance definition. So an implementation of substitute must accept a σ that handles Term a1 for some value of a1, which is not guaranteed to be the specific a that your instance is defined on. (Yes, your instance is defined over all a... but from inside the scope of the instance definition, it's as if a specific a has been chosen.)

You can avoid this by parameterizing your Substitutable class by a type constructor instead of just a type, and passing the same a to that type constructor as is used in the σ type.

{-# 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]

Haskell correct types for class and instance

1 Answers