Finding the most general unifier in Haskell using Data.Comp.Unification (beginner question)

user_5760615 0
Viewed 533

I have the following structure in haskell, which implements some machinery for printing and calls the unifier. I get the following error from main:

0 =/= int

It seems to think that 0 is a number rather than a variable. Below is the full implementation.

 data CType 
      = CVar Int 
      | CArr CType CType
      | CInt
      | CBool
      deriving (Eq, Data)

data Constraint 
  = Equality CType CType
    deriving (Eq, Data)

I have some base types (int and bool), an arrow type, and type variables. Then I am running some algorithms that generate equality constraints which are represented in the way above.

My goal is that given a list of constraints, I want to find the most general unifier.

I came across this library: http://hackage.haskell.org/package/compdata-0.1/docs/Data-Comp-Unification.html

Since I am new to Haskell, I can't immediately figure out if I can directly apply it. Could I use this library or am I recommended to write the unifier from scratch?

UPDATE

I am currently making the following changes to the code, but am getting a unification error for the equation

f=g

module SolveEq where
import Data.Data
import Data.Void
import Data.List as List
import Data.Map as Map
import Data.Set as Set
import Data.Maybe (fromJust)
import Data.Maybe (isJust)
import Control.Monad
import TypeCheck
import Data.Comp.Variables
import Data.Comp.Unification
import Data.Comp.Term
import Data.Comp.Derive
import Constraint
import Lang

data CTypeF a 
    = CVarF Int 
    | CArrF a a
    | CIntF
    | CBoolF
    deriving (Data, Functor, Foldable, Traversable, Show, Eq)

$(makeShowF ''CTypeF)


example :: String
example = showF (CIntF :: CTypeF String)

instance HasVars CTypeF Int where
isVar (CVarF x) = Just x
isVar (CArrF x y) = Nothing
isVar CIntF = Nothing
isVar CBoolF = Nothing

type CType_ = Term CTypeF

f :: CType_
f = Term (CVarF 0)

g :: CType_
g = Term CIntF


unravel :: CType_ -> CType
unravel a = 
    case unTerm a of 
        CVarF i -> CVar i
        CArrF a b -> CArr (unravel a) (unravel b)
        CIntF -> CInt
        CBoolF -> CBool

getUnify :: Either (UnifError CTypeF Int) (Subst CTypeF Int)
getUnify = unify [(f,g)]

main = case getUnify of
  Left (FailedOccursCheck v term)     -> putStrLn ("failed occurs check " ++ show v ++ ": " ++ (show $ unravel term))
  Left (HeadSymbolMismatch t1 t2)     -> putStrLn ("head symbol mismatch " ++ show (unravel t1)  ++ " =/= " ++ (show $ unravel t2))
  Left (UnifError str)     -> putStrLn str
  Right (subst :: Subst CTypeF Int) -> print (fmap unravel subst)

The issue is in unify [(f,g)] which I would have expected to map 0 to Int. But it seems to not see that 0 is a variable. Is there something wrong with my isVar possibly?

Note: I am running with compdata-0.12

type-theory unification lambda-calculus type-inference haskell
1 Answers

I believe you can use that library, but you'll have to make a minor change to your data structure. Specifically, you'll have to rewrite it as a signature functor instead of a recursive data type.

Here's what that means: your CType type is recursive because it contains other instances of CType within one of its constructors (CArr). Rewriting a recursive data type as a signature means making a data type that takes a type parameter, and using that type parameter everywhere you'd use recursion instead. Like this:

 data CTypeF a 
      = CVar Int 
      | CArr a a
      | CInt
      | CBool
      deriving (Eq, Data)

Now, in your program, where you previously passed around CTypes, you'll need to work with something a little more complicated than just CTypeF. Your new CType-equivalent needs to apply CTypeF circularly, to itself. Fortunately, Term does this for you, so import Data.Comp.Term and replace all your CTypes with Term CTypeFs. (You can, of course, always alias type CType = Term CTypeF to save some typing; just be aware that Term CTypeF is not literally the same as your original CType; you'll need to add some Term constructors to places that produce and consume CTypes.)

Finally, in order to use the unification machinery in compdata, you'll need an instance of HasVars for CTypeF that identifies your CVar constructor as a variable. You'll also need to make CTypeF both a Functor and Foldable, but if you enable the DeriveFunctor and DeriveFoldable language features, GHC can do this for you—it's a strictly mechanical process.

When running unify, you need to make sure you're doing it in a context where the error monad m and the variable type v are unambiguous. There are many ways to do this, but for the sake of example, let's say that we're using the simplest error monad Either e as our m, and of course you'll want v to be Int. So you might write:

f = Term (CVar 2)
g = Term CInt

-- By matching against Left and Right, we're letting GHC know that unify
-- should return an Either; this disambiguates `m`
main = case unify [(f, g)] of
  Left _      -> print "did not unify"
  Right subst -> doMoreWork subst

-- The Int here disambiguates `v`
doMoreWork :: Subst CTypeF Int -> IO ()
doMoreWork subst = undefined -- fill in the blank!
user_112286280
Related