@@ -0,0 +1,154 @@
1+-----------------------------------------------------------------------------
2+--
3+-- Module : Control.Monad.Unify
4+-- Copyright : (c) Phil Freeman 2013
5+-- License : MIT
6+--
7+-- Maintainer : Phil Freeman <paf31@cantab.net>
8+-- Stability : experimental
9+-- Portability :
10+--
11+-- |
12+--
13+--
14+-----------------------------------------------------------------------------
15+
16+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
17+{-# LANGUAGE FlexibleInstances #-}
18+{-# LANGUAGE FlexibleContexts #-}
19+{-# LANGUAGE DeriveDataTypeable #-}
20+{-# LANGUAGE MultiParamTypeClasses #-}
21+{-# LANGUAGE FunctionalDependencies #-}
22+{-# LANGUAGE UndecidableInstances #-}
23+
24+module Control.Monad.Unify where
25+
26+import Data.Maybe
27+import Data.Monoid
28+
29+import Control.Applicative
30+import Control.Monad.State
31+import Control.Monad.Error.Class
32+
33+import Data.HashMap.Strict as M
34+
35+-- |
36+-- Untyped unification variables
37+--
38+type Unknown = Int
39+
40+-- |
41+-- A type which can contain unification variables
42+--
43+class Partial t where
44+ unknown :: Unknown -> t
45+ isUnknown :: t -> Maybe Unknown
46+ unknowns :: t -> [Unknown]
47+ ($?) :: Substitution t -> t -> t
48+
49+-- |
50+-- Identifies types which support unification
51+--
52+class (Partial t) => Unifiable m t | t -> m where
53+ (=?=) :: t -> t -> UnifyT t m ()
54+
55+-- |
56+-- A substitution maintains a mapping from unification variables to their values
57+--
58+data Substitution t = Substitution { runSubstitution :: M.HashMap Int t }
59+
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)
65+
66+-- |
67+-- State required for type checking
68+--
69+data UnifyState t = UnifyState {
70+ -- |
71+ -- The next fresh unification variable
72+ --
73+ unifyNextVar :: Int
74+ -- |
75+ -- The current substitution
76+ --
77+ , unifyCurrentSubstitution :: Substitution t
78+ }
79+
80+-- |
81+-- An empty @UnifyState@
82+--
83+defaultUnifyState :: (Partial t) => UnifyState t
84+defaultUnifyState = UnifyState 0 mempty
85+
86+-- |
87+-- The type checking monad, which provides the state of the type checker, and error reporting capabilities
88+--
89+newtype UnifyT t m a = UnifyT { unUnify :: StateT (UnifyState t) m a }
90+ deriving (Functor, Monad, Applicative, MonadPlus)
91+
92+instance (MonadState s m) => MonadState s (UnifyT t m) where
93+ get = UnifyT . lift $ get
94+ put = UnifyT . lift . put
95+
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)
99+
100+-- |
101+-- Run a computation in the Unify monad, failing with an error, or succeeding with a return value and the new next unification variable
102+--
103+runUnify :: UnifyState t -> UnifyT t m a -> m (a, UnifyState t)
104+runUnify s = flip runStateT s . unUnify
105+
106+-- |
107+-- Substitute a single unification variable
108+--
109+substituteOne :: (Partial t) => Unknown -> t -> Substitution t
110+substituteOne u t = Substitution $ M.singleton u t
111+
112+-- |
113+-- Replace a unification variable with the specified value in the current substitution
114+--
115+(=:=) :: (Error e, Monad m, MonadError e m, Unifiable m t) => Unknown -> t -> UnifyT t m ()
116+(=:=) u t' = do
117+ st <- UnifyT get
118+ let sub = unifyCurrentSubstitution st
119+ let t = sub $? t'
120+ occursCheck u t
121+ let current = sub $? unknown u
122+ case isUnknown current of
123+ Just u1 | u1 == u -> return ()
124+ _ -> current =?= t
125+ UnifyT $ modify $ \s -> s { unifyCurrentSubstitution = substituteOne u t <> unifyCurrentSubstitution s }
126+
127+-- |
128+-- Perform the occurs check, to make sure a unification variable does not occur inside a value
129+--
130+occursCheck :: (Error e, Monad m, MonadError e m, Partial t) => Unknown -> t -> UnifyT t m ()
131+occursCheck u t =
132+ case isUnknown t of
133+ Nothing -> when (u `elem` unknowns t) $ UnifyT . lift . throwError . strMsg $ "Occurs check fails"
134+ _ -> return ()
135+
136+-- |
137+-- Generate a fresh untyped unification variable
138+--
139+fresh' :: (Monad m) => UnifyT t m Unknown
140+fresh' = do
141+ st <- UnifyT get
142+ UnifyT $ modify $ \s -> s { unifyNextVar = succ (unifyNextVar s) }
143+ return $ unifyNextVar st
144+
145+-- |
146+-- Generate a fresh unification variable at a specific type
147+--
148+fresh :: (Monad m, Partial t) => UnifyT t m t
149+fresh = do
150+ u <- fresh'
151+ return $ unknown u
152+
153+
154+