unbound-generics-unify (empty) → 0.1.0.0

raw patch · 4 files changed

+268/−0 lines, 4 filesdep +basedep +containersdep +transformers

Dependencies added: base, containers, transformers, unbound-generics

Files

• LICENSE +29/−0
• README.md +52/−0
• src/Unbound/Generics/Unify.hs +164/−0
• unbound-generics-unify.cabal +23/−0

@@ -0,0 +1,29 @@+Copyright (c) 2024, Alejandro Serrano+++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of the copyright holder nor the names of its+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,52 @@+# Unification for `unbound-generics`++This package implements (first-order) unification by reusing the framework of [`unbound-generics`](https://hackage.haskell.org/package/unbound-generics).++To use it, declare your data types as usual, including the generically-derived instances for alpha-equivalence (`Alpha`) and substitution (`Subst`) from `unbound-generics`.+In addition to those, ask for a new instance of `Unify` with the same arguments as `Subst`, that is, the type from which we build variables, and the type we want to unify.++The packages provides a function `unify` which works on a `Unification` monad. This monad is parametrized by the type we draw variables from. That means you can have as many types as you want, but there should be a single type of variables. In many cases the compiler fails to infer that argument to the `Unification` monad, so we recommend enabling `TypeApplications` for that matter.++The result of `unify` is either a single value which is an instance of both arguments, or a `UnificationError`. That error explains where the process has failed by a `Path` consisting of constructor, fields, and indices; and a cause.++---++This is an example in which `Type` is the one we draw variables from. Since we also use `TypeConstructor` inside the `TyCon` constructor, we also need to "request" to derive `Unify Type TypeConstructor`.++```haskell+type TypeVar = Name Type++data Type = TyVar { var :: TypeVar }+          | TyFun { args :: [Type], ret :: Type }+          | TyCon { con :: TypeConstructor, args :: [Type] }+          deriving (Eq, Show, Generic, Typeable)++data TypeConstructor = TyConInt | TyConBool deriving (Eq, Show, Generic)++pattern TyInt, TyBool :: Type+pattern TyInt  = TyCon TyConInt []+pattern TyBool = TyCon TyConBool []++instance Alpha Type+instance Alpha TypeConstructor++instance Subst Type Type where+  isvar (TyVar v) = Just $ SubstName v+  isvar _ = Nothing+instance Subst Type TypeConstructor++instance Unify Type Type+instance Unify Type TypeConstructor+```++Here are some example runs, using the explicitly-typed version of `runUnification` to declare that we are using `Type`-variables. To create new variables we use the usual `s2n` function from `unbound-generics`.++```haskell+>>> runUnification @Type $ let x = s2n "x" in unify' (TyFun [TyVar x] TyInt) (TyFun [TyVar x] (TyVar x))+( Right (TyFun {args = [TyCon {con = TyConInt, args = []}], ret = TyCon {con = TyConInt, args = []}})+, fromList [(x,TyCon {con = TyConInt, args = []})] )++>>> runUnification @Type $ let x = s2n "x" in unify' (TyFun [TyVar x] TyInt) (TyFun [TyBool] (TyVar x))+( Left ([PathConstructor "TyFun", PathSelector "ret", PathConstructor "TyCon", PathSelector "con"], DifferentConstructor)+, fromList [(x,TyCon {con = TyConBool, args = []})] )+```

@@ -0,0 +1,164 @@+{-# language DefaultSignatures, UndecidableInstances, GADTs, MultiWayIf, AllowAmbiguousTypes #-}+-- | Unification for @unbound-generics@+module Unbound.Generics.Unify (+  -- * Main unification functions+  unify', Unify(..),+  -- ** Information about errors+  UnificationError, UnificationErrorCause(..),+  Path, PathElement(..),+  -- * Unification as a monad+  Unification(..),+  -- ** Base implementation+  UnificationM, runUnification,+  -- ** Including fresh creation+  UnificationFreshM, runUnificationFresh,+  -- ** As a monad transformer+  UnificationMT, runUnificationT,+  -- * Generic methods+  GUnify(..)+) where++import Data.Bifunctor+import Control.Monad (forM)+import Control.Monad.Trans.State+import Data.Functor.Identity+import Data.Map+import GHC.Generics+import Unbound.Generics.LocallyNameless++-- | Path to navigate to a unification error.+type UnificationError = (Path, UnificationErrorCause)++-- | Potential causes for unification errors.+data UnificationErrorCause where+  OccursCheck          :: (Name t) -> t -> UnificationErrorCause+  DifferentConstructor :: UnificationErrorCause+  DifferentListLength  :: UnificationErrorCause++instance Show UnificationErrorCause where+  show OccursCheck {}       = "OccursCheck"+  show DifferentConstructor = "DifferentConstructor"+  show DifferentListLength  = "DifferentListLength"++type Path = [PathElement]+-- | Ways to navigate within a value.+data PathElement+  = PathConstructor String | PathSelector String | PathIndex Int+  deriving (Eq, Show)++-- | Stateful storage of substitutions as required for unification.+--+-- The substitution operates only on terms and variables of type 't'.+class Monad m => Unification t m where+  -- | Obtain the current substitution.+  currentSubst :: m (Map (Name t) t)+  -- | Add a new substitution.+  recordSubst  :: Name t -> t -> m ()++applySubst :: forall t a m. (Unification t m, Subst t a) => a -> m a+applySubst term = do+  current <- currentSubst @t @m+  pure $ foldlWithKey (\t v u -> subst v u t) term current++type UnificationM t = UnificationMT t Identity+type UnificationFreshM t = UnificationMT t FreshM++runUnification :: forall t a. UnificationM t a -> (a, Map (Name t) t)+runUnification action = runIdentity (runUnificationT action)++runUnificationFresh :: forall t a. UnificationFreshM t a -> (a, Map (Name t) t)+runUnificationFresh action = runFreshM (runUnificationT action)++runUnificationT :: forall t m a. Monad m => UnificationMT t m a -> m (a, Map (Name t) t)+runUnificationT action = runStateT (unUnificationMT action) empty++newtype UnificationMT t m a +  = UnificationMT { unUnificationMT :: StateT (Map (Name t) t) m a }+  deriving (Functor, Applicative, Monad)++instance (Monad m) => Unification t (UnificationMT t m) where+  currentSubst = UnificationMT $ get+  recordSubst v t = UnificationMT $ modify (insert v t)++-- | Tries to unify two terms, giving back a common term, or a unification error.+--+-- This variant requires the terms to be of the same type 't' as the variables within them.+unify' :: forall t m. (Unification t m, Unify t t) => t -> t -> m (Either UnificationError t)+unify' = unify @t++-- | Declares the ability to unify values of type 'a' containing variables of type 't'.+class Subst t a => Unify t a where+  -- | Tries to unify two terms, giving back a common term, or a unification error.+  unify :: Unification t m => a -> a -> m (Either UnificationError a)++  default unify :: forall m. (Generic a, GUnify t (Rep a), Unification t m)+                 => a -> a -> m (Either UnificationError a)+  unify x y = do+    x' <- applySubst @t x+    y' <- applySubst @t y+    result <- unifyIsvar x' y'+    case result of+      Left e -> pure $ Left e+      Right r -> Right <$> applySubst @t r++    where+      unifyIsvar x y+        | Just (SubstName v1) <- isvar @t @a x+        , Just (SubstName v2) <- isvar @t @a y+        = if | v1 == v2  -> Right <$> applySubst @t x+             | v1  < v2  -> do { recordSubst v1 y ; Right <$> applySubst @t x }+             | otherwise -> do { recordSubst v2 x ; Right <$> applySubst @t y }+        -- do occurs check!!+        | Just (SubstName v) <- isvar @t @a x = do { recordSubst v y ; Right <$> applySubst @t x }+        | Just (SubstName v) <- isvar @t @a y = do { recordSubst v x ; Right <$> applySubst @t y }+        | otherwise = unify_ x y++      unify_ :: a -> a -> m (Either UnificationError a)+      unify_ x y = fmap to <$> gunify @t @(Rep a) @m (from x) (from y)++instance {-# overlaps #-} Unify t (Name t) where+  unify = error "should have never arrived here"++-- required because otherwise strings are matched as lists+instance {-# overlaps #-} Unify t String where+  unify x y+    | x == y    = pure $ Right x+    | otherwise = pure $ Left ([], DifferentConstructor)++instance {-# overlaps #-} (Unify t a) => Unify t [a] where+  unify xlst ylst+    | length xlst /= length ylst = pure $ Left ([], DifferentListLength)+    | otherwise = sequence <$> forM (zip3 [0 .. ] xlst ylst) (\(i, x,  y) -> first (first (PathIndex i :)) <$> unify @t x y)++-- | Implementation of unification using @GHC.Generics@.+class GUnify t f where+  gunify :: Unification t m => f a -> f a -> m (Either UnificationError (f a))++instance GUnify t U1 where+  gunify _ _ = pure $ Right U1++instance (Unify t a) => GUnify t (K1 i a) where+  gunify (K1 x) (K1 y) = fmap K1 <$> unify @t x y++instance GUnify t f => GUnify t (D1 d f) where+  gunify (M1 x) (M1 y) = fmap M1 <$> gunify @t x y++instance (Constructor c, GUnify t f) => GUnify t (C1 c f) where+  gunify c@(M1 x) (M1 y) = bimap (first (PathConstructor (conName c) :)) M1 <$> gunify @t x y++instance (Selector s, GUnify t f) => GUnify t (S1 s f) where+  gunify c@(M1 x) (M1 y) = +    case selName c of+      ""  -> fmap M1 <$> gunify @t x y+      con -> bimap (first (PathSelector con :)) M1 <$> gunify @t x y++instance (GUnify t f, GUnify t g) => GUnify t (f :*: g) where+  gunify (x1 :*: x2) (y1 :*: y2) = do+    r1 <- gunify @t x1 y1+    r2 <- gunify @t x2 y2+    pure $ (:*:) <$> r1 <*> r2++instance (GUnify t f, GUnify t g) => GUnify t (f :+: g) where+  gunify (R1 x) (R1 y) = fmap R1 <$> gunify @t x y+  gunify (L1 x) (L1 y) = fmap L1 <$> gunify @t x y+  gunify _ _ = pure $ Left ([], DifferentConstructor)

@@ -0,0 +1,23 @@+cabal-version:      3.0+name:               unbound-generics-unify+version:            0.1.0.0+synopsis:           Unification based on unbound-generics+-- description:+license:            BSD-3-Clause+license-file:       LICENSE+author:             Alejandro Serrano+maintainer:         trupill@gmail.com+-- copyright:+category:           Language+build-type:         Simple+extra-source-files: README.md++common warnings+    ghc-options: -Wall++library+    import:           warnings+    exposed-modules:  Unbound.Generics.Unify+    build-depends:    base >= 4.16 && < 5, unbound-generics ^>= 0.4.4, containers >= 0.7, transformers >= 0.6+    hs-source-dirs:   src+    default-language: GHC2021