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