wrengr / unification-fd Goto Github PK
View Code? Open in Web Editor NEWGeneric functions for single-sorted first-order structural unification
License: Other
Generic functions for single-sorted first-order structural unification
License: Other
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 a
s 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:
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:
Warning: 'modify' is out of scope. (in either 'Control.Monad.MaybeK' or 'Control.Monad.State.UnificationExtras')
Missing documentation for:
unFix (src/Data/Functor/Fixedpoint.hs:94)
runIntBindingT (src/Control/Unification/IntVar.hs:159)
execIntBindingT (src/Control/Unification/IntVar.hs:169)
runIntRBindingT (src/Control/Unification/Ranked/IntVar.hs:118)
execIntRBindingT (src/Control/Unification/Ranked/IntVar.hs:128)
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.