@@ -0,0 +1,154 @@
1+-----------------------------------------------------------------------------
3+-- Module : Control.Monad.Unify
4+-- Copyright : (c) Phil Freeman 2013
7+-- Maintainer : Phil Freeman <paf31@cantab.net>
8+-- Stability : experimental
14+-----------------------------------------------------------------------------
16+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
17+{-# LANGUAGE FlexibleInstances #-}
18+{-# LANGUAGE FlexibleContexts #-}
19+{-# LANGUAGE DeriveDataTypeable #-}
20+{-# LANGUAGE MultiParamTypeClasses #-}
21+{-# LANGUAGE FunctionalDependencies #-}
22+{-# LANGUAGE UndecidableInstances #-}
24+module Control.Monad.Unify where
29+import Control.Applicative
30+import Control.Monad.State
31+import Control.Monad.Error.Class
33+import Data.HashMap.Strict as M
36+-- Untyped unification variables
41+-- A type which can contain unification variables
44+ unknown :: Unknown -> t
45+ isUnknown :: t -> Maybe Unknown
46+ unknowns :: t -> [Unknown]
47+ ($?) :: Substitution t -> t -> t
50+-- Identifies types which support unification
52+class (Partial t) => Unifiable m t | t -> m where
53+ (=?=) :: t -> t -> UnifyT t m ()
56+-- A substitution maintains a mapping from unification variables to their values
58+data Substitution t = Substitution { runSubstitution :: M.HashMap Int t }
60+instance (Partial t) => Monoid (Substitution t) where
61+ mempty = Substitution M.empty
62+ s1 `mappend` s2 = Substitution $
63+ M.map (s2 $?) (runSubstitution s1) `M.union`
64+ M.map (s1 $?) (runSubstitution s2)
67+-- State required for type checking
69+data UnifyState t = UnifyState {
71+ -- The next fresh unification variable
75+ -- The current substitution
77+ , unifyCurrentSubstitution :: Substitution t
81+-- An empty @UnifyState@
83+defaultUnifyState :: (Partial t) => UnifyState t
84+defaultUnifyState = UnifyState 0 mempty
87+-- The type checking monad, which provides the state of the type checker, and error reporting capabilities
89+newtype UnifyT t m a = UnifyT { unUnify :: StateT (UnifyState t) m a }
90+ deriving (Functor, Monad, Applicative, MonadPlus)
92+instance (MonadState s m) => MonadState s (UnifyT t m) where
93+ get = UnifyT . lift $ get
94+ put = UnifyT . lift . put
96+instance (MonadError e m) => MonadError e (UnifyT t m) where
97+ throwError = UnifyT . throwError
98+ catchError e f = UnifyT $ catchError (unUnify e) (unUnify . f)
101+-- Run a computation in the Unify monad, failing with an error, or succeeding with a return value and the new next unification variable
103+runUnify :: UnifyState t -> UnifyT t m a -> m (a, UnifyState t)
104+runUnify s = flip runStateT s . unUnify
107+-- Substitute a single unification variable
109+substituteOne :: (Partial t) => Unknown -> t -> Substitution t
110+substituteOne u t = Substitution $ M.singleton u t
113+-- Replace a unification variable with the specified value in the current substitution
115+(=:=) :: (Error e, Monad m, MonadError e m, Unifiable m t) => Unknown -> t -> UnifyT t m ()
118+ let sub = unifyCurrentSubstitution st
121+ let current = sub $? unknown u
122+ case isUnknown current of
123+ Just u1 | u1 == u -> return ()
125+ UnifyT $ modify $ \s -> s { unifyCurrentSubstitution = substituteOne u t <> unifyCurrentSubstitution s }
128+-- Perform the occurs check, to make sure a unification variable does not occur inside a value
130+occursCheck :: (Error e, Monad m, MonadError e m, Partial t) => Unknown -> t -> UnifyT t m ()
133+ Nothing -> when (u `elem` unknowns t) $ UnifyT . lift . throwError . strMsg $ "Occurs check fails"
137+-- Generate a fresh untyped unification variable
139+fresh' :: (Monad m) => UnifyT t m Unknown
142+ UnifyT $ modify $ \s -> s { unifyNextVar = succ (unifyNextVar s) }
143+ return $ unifyNextVar st
146+-- Generate a fresh unification variable at a specific type
148+fresh :: (Monad m, Partial t) => UnifyT t m t