git.iko.soy/rowtype-yoga/purescript-native
on 00a4705 help sign in
rowtype-yoga/purescript-native/src/Control/Monad/Unify.hs
160 lines 4.5 kB history raw
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-----------------------------------------------------------------------------
16{-# LANGUAGE GeneralizedNewtypeDeriving #-}
17{-# LANGUAGE FlexibleInstances #-}
18{-# LANGUAGE FlexibleContexts #-}
19{-# LANGUAGE DeriveDataTypeable #-}
20{-# LANGUAGE MultiParamTypeClasses #-}
21{-# LANGUAGE FunctionalDependencies #-}
22{-# LANGUAGE UndecidableInstances #-}
24module Control.Monad.Unify where
26import Data.Monoid
28import Control.Applicative
29import Control.Monad.State
30import Control.Monad.Error.Class (MonadError(..))
31import Control.Monad.Writer.Class (MonadWriter(..))
33import Data.HashMap.Strict as M
35-- |
36-- Untyped unification variables
37--
38type Unknown = Int
40-- |
41-- A type which can contain unification variables
42--
43class Partial t where
44 unknown :: Unknown -> t
45 isUnknown :: t -> Maybe Unknown
46 unknowns :: t -> [Unknown]
47 ($?) :: Substitution t -> t -> t
49-- |
50-- Identifies types which support unification
51--
52class (Partial t) => Unifiable m t | t -> m where
53 (=?=) :: t -> t -> UnifyT t m ()
55-- |
56-- A substitution maintains a mapping from unification variables to their values
57--
58data Substitution t = Substitution { runSubstitution :: M.HashMap Int t }
60instance (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)
66-- |
67-- State required for type checking
68--
69data 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 }
80-- |
81-- An empty @UnifyState@
82--
83defaultUnifyState :: (Partial t) => UnifyState t
84defaultUnifyState = UnifyState 0 mempty
86-- |
87-- A class for errors which support unification errors
88--
89class UnificationError t e where
90 occursCheckFailed :: t -> e
92-- |
93-- The type checking monad, which provides the state of the type checker, and error reporting capabilities
94--
95newtype UnifyT t m a = UnifyT { unUnify :: StateT (UnifyState t) m a }
96 deriving (Functor, Monad, Applicative, Alternative, MonadPlus, MonadWriter w)
98instance (MonadState s m) => MonadState s (UnifyT t m) where
99 get = UnifyT . lift $ get
100 put = UnifyT . lift . put
102instance (MonadError e m) => MonadError e (UnifyT t m) where
103 throwError = UnifyT . throwError
104 catchError e f = UnifyT $ catchError (unUnify e) (unUnify . f)
106-- |
107-- Run a computation in the Unify monad, failing with an error, or succeeding with a return value and the new next unification variable
108--
109runUnify :: UnifyState t -> UnifyT t m a -> m (a, UnifyState t)
110runUnify s = flip runStateT s . unUnify
112-- |
113-- Substitute a single unification variable
114--
115substituteOne :: (Partial t) => Unknown -> t -> Substitution t
116substituteOne u t = Substitution $ M.singleton u t
118-- |
119-- Replace a unification variable with the specified value in the current substitution
120--
121(=:=) :: (UnificationError t e, Monad m, MonadError e m, Unifiable m t) => Unknown -> t -> UnifyT t m ()
122(=:=) u t' = do
123 st <- UnifyT get
124 let sub = unifyCurrentSubstitution st
125 let t = sub $? t'
126 occursCheck u t
127 let current = sub $? unknown u
128 case isUnknown current of
129 Just u1 | u1 == u -> return ()
130 _ -> current =?= t
131 UnifyT $ modify $ \s -> s { unifyCurrentSubstitution = substituteOne u t <> unifyCurrentSubstitution s }
133-- |
134-- Perform the occurs check, to make sure a unification variable does not occur inside a value
135--
136occursCheck :: (UnificationError t e, Monad m, MonadError e m, Partial t) => Unknown -> t -> UnifyT t m ()
137occursCheck u t =
138 case isUnknown t of
139 Nothing -> when (u `elem` unknowns t) $ UnifyT . lift . throwError $ occursCheckFailed t
140 _ -> return ()
142-- |
143-- Generate a fresh untyped unification variable
144--
145fresh' :: (Monad m) => UnifyT t m Unknown
146fresh' = do
147 st <- UnifyT get
148 UnifyT $ modify $ \s -> s { unifyNextVar = succ (unifyNextVar s) }
149 return $ unifyNextVar st
151-- |
152-- Generate a fresh unification variable at a specific type
153--
154fresh :: (Monad m, Partial t) => UnifyT t m t
155fresh = do
156 u <- fresh'
157 return $ unknown u