wrengr / unification-fd Goto Github PK

Trying out this library I noticed that unify succeeded where occurs checking should have rejected the equation. Trying out unifyOccurs I got the correct behavior.

Is this always a bug? Or are there things I can do wrong that would cause this behavior?

src/Control/Monad/EitherK.hs:117:7:
    `<$' is not a (visible) method of class `Functor'

src/Control/Monad/EitherK.hs:241:7:
    `<$' is not a (visible) method of class `Functor'

I'll make a revision to 0.11.2

EDIT: I'd suggest dropping support for older GHCs, e.g. GHC-7, by bumping lower bound of base to base >=4.9 or even higher, as these GHCs are not used much if at all nowadays,

It seems that the Left case in zipMatch can never be used? Looking at the generic implementation, it is only used in V1 and U1, which both don't contain the parameter. It seems to make sense that Left isn't needed: either I have a pair of as which I know nothing about, so I have to use Right, or I don't have any a, in which case t a and t (a, a) are the same. So maybe it can be simplified to zipMatch :: t a -> t a -> Maybe (t (a, a))?

(If that's the case I'd suggest zipMatchWith :: (a -> a -> Maybe b) -> t a -> t a -> Maybe (t b) which helps with implementing Unifiable (f :.: g))

There's a peculiar comment about the Applicative (UTerm t) instance maybe not making sense because the first argument to (<*>) will be a UTerm with a function in it. That weirdness largely goes away with liftA2; for GHC 8.2, you can add

    liftA2 f (UVar a) (UVar b) = UVar (f a b)
    liftA2 f (UVar a) (UTerm mb) = UTerm (fmap (f a) <$> mb)
    liftA2 f (UTerm ma) b = UTerm ((\q -> liftA2 f q b) <$> ma)

I can't say if it's useful or not, but it seems pretty harmless. I'm not sure the Alternative instance is even harmless; the free package documents that one as not obeying the Alternative laws, though I don't know of any standard set thereof.

There are currently a few forks to consider merging in:

• https://github.com/ajrouvoet/unification.hs (2 ahead)
• https://github.com/lortabac/unification-fd (7 ahead)
• https://github.com/UnkindPartition/unification-fd (2 ahead); but cf the PR first

Is it possible to implement the Hindley Milner type inference algorithm using this package's API? The reason I ask is that I made an initial attempt to do so, but ran into difficult making polymorphic types Unifiable.

To illustrate this, usually the way the types are encoded in the HM algorithm is something like:

data Polytype = Polytype [TypeVariable] Monotype

data Monotype = Variable TypeVariable | FunctionType Monotype Monotype

Now, I can make Monotype implement Unifiable by doing this:

data MonotypeF x = Variable TypeVariable | FunctionType x x
    deriving (Foldable, Functor, Generic1, Traversable, Unifiable)

type Monotype = Fix MonotypeF

… but I can't make Polytype implement Unifiable (at least, not in a useful way, as far as I can tell). Is this a limitation of the unification-fd API or am I missing something?

Hi wren,

I am starting to use unification-fd in a new project, and I find writing a Unifiable instance by hand is quite tedious. I am surprised that there aren't any generic implementations of it that I could find.

I think it should be doable with GHC Generics.

So I have a few questions:

1. Do you happen to know any generic implementations? Did I miss something?
2. Is it a bad idea? :)
3. If I manage to write one, would you be open to including it in the package?

Version 0.7.1 of logict breaks the build. For more info see: Bodigrim/logict#20 (comment)

The GHC inliner on the current LTS Stackage release doesn't like the Eq and Ord instances on Fix.

The following code, compiled with GHC 8.0.1 with -v blows from ~50 "terms" to 500,000 "terms".

Putting a {-# NOINLINE (==) #-} pragma on the instance for Eq (Fix f), or writing a manual instance for Eq (Foo' a) with a similar pragma solves my issue. For now I am doing the second as a work around.

The issue can be tested with LTS-7.2 through to LTS-7.14, and is not present on LTS-6.27.

newtype Fix f = Fix { unFix :: f (Fix f) }

instance (Eq (f (Fix f))) => Eq (Fix f) where
  x == y  = unFix x == unFix y
  x /= y  = unFix x /= unFix y

data Foo' a = A
            | B a
            | C a
            | D a a
            | E a a a
            deriving (Eq)

type Foo = Fix Foo'

bar :: Foo -> Foo -> m ()
bar t t' =
  if t == t'
  then undefined
  else undefined

Last upload was four years ago and many commits have happened since then.

I've written some code making it possible to deriving Unifiable instances using Generic1 from GHC.Generics. How maintained is this repo, i.e. if I make a PR will it see the light of day on Hackage (modulo the code being acceptable of course)?

zipMatchViaGeneric
  :: (Generic1 t, GUnifiable (Rep1 t))
  => t a
  -> t a
  -> Maybe (t (Either a (a, a)))
zipMatchViaGeneric l r = to1 <$> gZipMatch (from1 l) (from1 r)

class (Traversable t, Generic1 t) => GUnifiable t where
  gZipMatch :: t a -> t a -> Maybe (t (Either a (a,a)))

instance GUnifiable t => GUnifiable (M1 m i t) where
  gZipMatch (M1 l) (M1 r) = M1 <$> gZipMatch l r

instance GUnifiable U1 where
  gZipMatch _ _ = Just U1

instance Eq c => GUnifiable (K1 m c) where
  gZipMatch (K1 l) (K1 r) | l == r    = Just (K1 l)
                          | otherwise = Nothing

instance GUnifiable Par1 where
  gZipMatch (Par1 l) (Par1 r) = Just . Par1 . Right $ (l, r)

instance Unifiable x => GUnifiable (Rec1 x) where
  gZipMatch (Rec1 l) (Rec1 r) = Rec1 <$> zipMatch l r

instance (GUnifiable l, GUnifiable r) => GUnifiable (l :+: r) where
  gZipMatch (L1 l) (L1 r) = L1 <$> gZipMatch l r
  gZipMatch (R1 l) (R1 r) = R1 <$> gZipMatch l r
  gZipMatch _      _      = Nothing

instance (GUnifiable l, GUnifiable r) => GUnifiable (l :*: r) where
  gZipMatch (l1 :*: r1) (l2 :*: r2) =
    (:*:) <$> gZipMatch l1 l2 <*> gZipMatch r1 r2

instance (Unifiable a, GUnifiable b) => GUnifiable (a :.: b) where
  gZipMatch (Comp1 l) (Comp1 r) = do
    x <- zipMatch l r >>= traverse
      (\case
        Left  a        -> Just $ Left <$> a
        Right (a1, a2) -> gZipMatch a1 a2
      )
    pure (Comp1 x)

I'm using applyBindings pervasively in https://github.com/mlabs-haskell/lambda-buffers/blob/401f8a920a557c71440795174da199a1e128c4f9/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs#L254.

It was very difficult to understand what's happening, but without it the whole thing just doesn't work. On multiple occasions I tried to debug this, and from what I can tell the 'variable sharing' business makes some unification (as on one side there's a variable) succeed when it shouldn't. This is 'fixed' by using applyBindings throughout to resolve any term completely so it doesn't contain shared variables.

I'd appreciate some advice here as it's my impressions that applyBindings should NOT be able to affect the semantics of a unification-fd program.

Thanks!

In NLTK, they have a module for the unification of https://en.wikipedia.org/wiki/Feature_structure. The
http://www.nltk.org/howto/featstruct.html

I wonder if this package provides the necessary for doing it in Haskell.

Travis is deprecated. See ekmett/lens#954

to be up-to-date with the ecosystem and in order to get the package back to stackage (see commercialhaskell/stackage#6955).

https://hackage.haskell.org/package/logict-0.8.1.0/changelog