git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Prototype of a rows in instance contexts, based on @apsk's work.
commitf5f29257692bea5bdf04cdea8082bda66796e4fb authorPhil Freeman <paf31@cantab.net> dateTue 10 Feb 2015, 18:41 (12 years ago) parent6be7df9
3 files changed+60−3
compare with golang
unifiedsplit
examples/passing/RowPolyInstanceContext.purs+20 src/Language/PureScript/TypeChecker/Entailment.hs+23−3 src/Language/PureScript/TypeChecker/Unify.hs+17
examples/passing/RowPolyInstanceContext.pursnew file+20
@@ -0,0 +1,20 @@
1+module Main where
2+
3+class T s m where
4+ state :: (s -> s) -> m Unit
5+
6+data S s a = S (s -> { new :: s, ret :: a })
7+
8+instance st :: T s (S s) where
9+ state f = S $ \s -> { new: f s, ret: unit }
10+
11+test1 :: forall r . S { foo :: String | r } Unit
12+test1 = state $ \o -> o { foo = o.foo ++ "!" }
13+
14+test2 :: forall m r . (T { foo :: String | r } m) => m Unit
15+test2 = state $ \o -> o { foo = o.foo ++ "!" }
16+
17+main = do
18+ let t1 = test1
19+ let t2 = test2
20+ Debug.Trace.trace "Done"
src/Language/PureScript/TypeChecker/Entailment.hs+23−3
@@ -20,6 +20,7 @@ module Language.PureScript.TypeChecker.Entailment (
2020import Data.Function (on)
2121import Data.List
2222import Data.Maybe (maybeToList)
23+import Data.Foldable (foldMap)
2324import qualified Data.Map as M
2425
2526import Control.Applicative
@@ -199,13 +200,32 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt
199200-- and return a substitution from type variables to types which makes the type heads unify.
200201--
201202typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
202−typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
203−typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
203+typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
204+typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
204205typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
205−typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2 <*> typeHeadsAreEqual m e t1 t2
206+typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2
207+ <*> typeHeadsAreEqual m e t1 t2
206208typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
207209 Left _ -> Nothing
208210 Right t1 -> typeHeadsAreEqual m e t1 t2
211+typeHeadsAreEqual _ _ REmpty REmpty = Just []
212+typeHeadsAreEqual m e r1@(RCons _ _ _) r2@(RCons _ _ _) =
213+ let (s1, r1') = rowToList r1
214+ (s2, r2') = rowToList r2
215+
216+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
217+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
218+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
219+ in (++) <$> foldMap (\(t1, t2) -> typeHeadsAreEqual m e t1 t2) int
220+ <*> go sd1 r1' sd2 r2'
221+ where
222+ go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]
223+ go [] REmpty [] REmpty = Just []
224+ go [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = Just []
225+ go [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = Just []
226+ go _ (TUnknown _) _ _ = Just []
227+ go _ _ _ (TUnknown _) = Just []
228+ go _ _ _ _ = Nothing
209229typeHeadsAreEqual _ _ _ _ = Nothing
210230
211231-- |
src/Language/PureScript/TypeChecker/Unify.hs+17
@@ -153,6 +153,23 @@ unifiesWith e (SaturatedTypeSynonym name args) t2 =
153153 Left _ -> False
154154 Right t1 -> unifiesWith e t1 t2
155155unifiesWith e t1 t2@(SaturatedTypeSynonym _ _) = unifiesWith e t2 t1
156+unifiesWith _ REmpty REmpty = True
157+unifiesWith e r1@(RCons _ _ _) r2@(RCons _ _ _) =
158+ let (s1, r1') = rowToList r1
159+ (s2, r2') = rowToList r2
160+
161+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
162+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
163+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
164+ in all (\(t1, t2) -> unifiesWith e t1 t2) int && go sd1 r1' sd2 r2'
165+ where
166+ go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Bool
167+ go [] REmpty [] REmpty = True
168+ go [] (TypeVar v1) [] (TypeVar v2) = v1 == v2
169+ go [] (Skolem _ s1 _) [] (Skolem _ s2 _) = s1 == s2
170+ go _ (TUnknown _) _ _ = True
171+ go _ _ _ (TUnknown _) = True
172+ go _ _ _ _ = False
156173unifiesWith _ _ _ = False
157174
158175-- |