Поиск наиболее общего унификатора в Haskell с использованием Data.Comp.Unification (вопрос для начинающих) - PullRequest
Новая
       55

Поиск наиболее общего унификатора в Haskell с использованием Data.Comp.Unification (вопрос для начинающих)

4 голосов
/ 17 июня 2019

У меня есть следующая структура в haskell, которая реализует некоторые механизмы для печати и вызывает унификатор. Я получаю следующую ошибку от main: 

0 =/= int

Кажется, что 0 - это число, а не переменная. Ниже приведена полная реализация. 

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

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

У меня есть несколько базовых типов (int и bool), тип стрелки и переменные типа. Затем я запускаю некоторые алгоритмы, которые генерируют ограничения равенства, которые представлены выше.

Моя цель состоит в том, чтобы, учитывая список ограничений, я хочу найти наиболее общий объединитель.

Я наткнулся на эту библиотеку: http://hackage.haskell.org/package/compdata-0.1/docs/Data-Comp-Unification.html

Поскольку я новичок в Haskell, я не могу сразу понять, могу ли я применить его напрямую. Могу ли я использовать эту библиотеку или я рекомендую написать унификатор с нуля?

UPDATE

В настоящее время я делаю следующие изменения в коде, но получаю ошибку унификации для уравнения

* * 1 022 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)

Проблема в unify [(f,g)], которую я ожидал от 0 до Int. Но, похоже, не видит, что 0 является переменной. Возможно, что-то не так с моим isVar?

Примечание: я работаю с compdata-0.12

1 Ответ

4 голосов
/ 17 июня 2019

Я полагаю, что вы можете использовать эту библиотеку, но вам придется внести незначительные изменения в вашу структуру данных.В частности, вам придется переписать его как функтор подписи вместо рекурсивного типа данных.

Вот что это значит: ваш тип CType является рекурсивным, поскольку содержит другие экземпляры CType в одном изего конструкторы (CArr).Переписать рекурсивный тип данных в качестве сигнатуры означает создание типа данных, который принимает параметр типа, и использовать этот параметр типа везде, где вместо этого вы будете использовать рекурсию.Например: 

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

Теперь в вашей программе, где вы ранее проходили около CType с, вам нужно будет работать с чем-то более сложным, чем просто CTypeF.Ваш новый CType -эквивалент должен применить CTypeF по кругу к себе.К счастью, Term сделает это за вас, поэтому импортируйте Data.Comp.Term и замените все ваши CType с Term CTypeF с.(Конечно, вы всегда можете использовать псевдоним type CType = Term CTypeF, чтобы сохранить некоторую типизацию; просто учтите, что Term CTypeF буквально не совпадает с вашим исходным CType; вам нужно добавить несколько конструкторов Term в места, которыепроизводить и потреблять CType с.)

Наконец, чтобы использовать механизм объединения в compdata, вам понадобится экземпляр HasVars для CTypeF, которыйидентифицирует ваш CVar конструктор как переменную.Вам также нужно будет сделать CTypeF и Functor и Foldable, но если вы включите языковые функции DeriveFunctor и DeriveFoldable, GHC может сделатьэто для вас - это чисто механический процесс.

Когда вы запускаете unify, вам нужно убедиться, что вы делаете это в контексте, где ошибка монады m и тип переменной v однозначно.Есть много способов сделать это, но для примера, скажем, что мы используем простейшую монаду ошибок Either e в качестве m, и, конечно, вы захотите, чтобы v было Int,Так что вы можете написать: 

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!
...