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