Skip to content
This repository was archived by the owner on Apr 1, 2025. It is now read-only.

Commit b81cbf2

Browse files
robrixrobrix
committed
Represent Monotype in Term.
1 parent a5151d3 commit b81cbf2

1 file changed

Lines changed: 52 additions & 53 deletions

File tree

‎semantic-core/src/Analysis/Typecheck.hs‎

Lines changed: 52 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -36,14 +36,26 @@ import Data.Term
3636
import GHC.Generics (Generic1)
3737
import Prelude hiding (fail)
3838

39-
data Monotype a
39+
data Monotype f a
4040
= MBool
4141
| MUnit
4242
| MString
43-
| MMeta a
44-
| MArr (Monotype a) (Monotype a)
45-
| MRecord (Map.Map User (Monotype a))
46-
deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
43+
| MArr (f a) (f a)
44+
| MRecord (Map.Map User (f a))
45+
deriving (Foldable, Functor, Generic1, Traversable)
46+
47+
deriving instance (Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (Monotype f a)
48+
deriving instance (Ord a, forall a . Eq a => Eq (f a)
49+
, forall a . Ord a => Ord (f a), Monad f) => Ord (Monotype f a)
50+
deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Monotype f a)
51+
52+
instance HFunctor Monotype
53+
instance RightModule Monotype where
54+
MUnit >>=* _ = MUnit
55+
MBool >>=* _ = MBool
56+
MString >>=* _ = MString
57+
MArr a b >>=* f = MArr (a >>= f) (b >>= f)
58+
MRecord m >>=* f = MRecord ((>>= f) <$> m)
4759

4860
type Meta = Int
4961

@@ -77,20 +89,21 @@ forAll n body = send (PForAll (Data.Scope.bind1 n body))
7789
forAlls :: (Eq a, Carrier sig m, Member Polytype sig, Foldable t) => t a -> m a -> m a
7890
forAlls ns body = foldr forAll body ns
7991

80-
generalize :: (Carrier sig m, Member Naming sig) => Monotype Meta -> m (Term Polytype Gensym)
92+
generalize :: (Carrier sig m, Member Naming sig) => Term Monotype Meta -> m (Term Polytype Gensym)
8193
generalize ty = namespace "generalize" $ do
8294
Gensym root _ <- Name.fresh
8395
pure (forAlls (map (Gensym root) (IntSet.toList (mvs ty))) (fold root ty))
8496
where fold root = \case
85-
MUnit -> Term PUnit
86-
MBool -> Term PBool
87-
MString -> Term PString
88-
MMeta i -> Var (Gensym root i)
89-
MArr a b -> Term (PArr (fold root a) (fold root b))
90-
MRecord fs -> Term (PRecord (fold root <$> fs))
97+
Var v -> pure (Gensym root v)
98+
Term t -> Term $ case t of
99+
MUnit -> PUnit
100+
MBool -> PBool
101+
MString -> PString
102+
MArr a b -> PArr (fold root a) (fold root b)
103+
MRecord fs -> PRecord (fold root <$> fs)
91104

92105

93-
typecheckingFlowInsensitive :: [File (Term Core.Core Name)] -> (Heap Name (Monotype Meta), [File (Either (Loc, String) (Term Polytype Gensym))])
106+
typecheckingFlowInsensitive :: [File (Term Core.Core Name)] -> (Heap Name (Term Monotype Meta), [File (Either (Loc, String) (Term Polytype Gensym))])
94107
typecheckingFlowInsensitive
95108
= run
96109
. runFresh
@@ -103,15 +116,15 @@ runFile :: ( Carrier sig m
103116
, Effect sig
104117
, Member Fresh sig
105118
, Member Naming sig
106-
, Member (State (Heap Name (Monotype Meta))) sig
119+
, Member (State (Heap Name (Term Monotype Meta))) sig
107120
)
108121
=> File (Term Core.Core Name)
109-
-> m (File (Either (Loc, String) (Monotype Meta)))
122+
-> m (File (Either (Loc, String) (Term Monotype Meta)))
110123
runFile file = traverse run file
111124
where run
112125
= (\ m -> do
113126
(subst, t) <- m
114-
modify @(Heap Name (Monotype Meta)) (substAll subst)
127+
modify @(Heap Name (Term Monotype Meta)) (substAll subst)
115128
pure (substAll subst <$> t))
116129
. runState (mempty :: Substitution)
117130
. runReader (fileLoc file)
@@ -126,7 +139,7 @@ runFile file = traverse run file
126139
v <$ for_ bs (unify v))
127140
. convergeTerm (fix (cacheTerm . eval typecheckingAnalysis))
128141

129-
typecheckingAnalysis :: (Alternative m, Carrier sig m, Member Fresh sig, Member (State (Set.Set Constraint)) sig, Member (State (Heap Name (Monotype Meta))) sig, MonadFail m) => Analysis Name (Monotype Meta) m
142+
typecheckingAnalysis :: (Alternative m, Carrier sig m, Member Fresh sig, Member (State (Set.Set Constraint)) sig, Member (State (Heap Name (Term Monotype Meta))) sig, MonadFail m) => Analysis Name (Term Monotype Meta) m
130143
typecheckingAnalysis = Analysis{..}
131144
where alloc = pure
132145
bind _ _ = pure ()
@@ -139,58 +152,58 @@ typecheckingAnalysis = Analysis{..}
139152
arg <- meta
140153
assign addr arg
141154
ty <- eval body
142-
pure (MArr arg ty)
155+
pure (Term (MArr arg ty))
143156
apply _ f a = do
144157
_A <- meta
145158
_B <- meta
146-
unify (MArr _A _B) f
159+
unify (Term (MArr _A _B)) f
147160
unify _A a
148161
pure _B
149-
unit = pure MUnit
150-
bool _ = pure MBool
151-
asBool b = unify MBool b >> pure True <|> pure False
152-
string _ = pure MString
153-
asString s = unify MString s $> mempty
162+
unit = pure (Term MUnit)
163+
bool _ = pure (Term MBool)
164+
asBool b = unify (Term MBool) b >> pure True <|> pure False
165+
string _ = pure (Term MString)
166+
asString s = unify (Term MString) s $> mempty
154167
frame = fail "unimplemented"
155168
edge _ _ = pure ()
156169
_ ... m = m
157170

158171

159-
data Constraint = Monotype Meta :===: Monotype Meta
172+
data Constraint = Term Monotype Meta :===: Term Monotype Meta
160173
deriving (Eq, Ord, Show)
161174

162175
infix 4 :===:
163176

164177
data Solution
165-
= Int := Monotype Meta
178+
= Int := Term Monotype Meta
166179
deriving (Eq, Ord, Show)
167180

168181
infix 5 :=
169182

170-
meta :: (Carrier sig m, Member Fresh sig) => m (Monotype Meta)
171-
meta = MMeta <$> Fresh.fresh
183+
meta :: (Carrier sig m, Member Fresh sig) => m (Term Monotype Meta)
184+
meta = pure <$> Fresh.fresh
172185

173-
unify :: (Carrier sig m, Member (State (Set.Set Constraint)) sig) => Monotype Meta -> Monotype Meta -> m ()
186+
unify :: (Carrier sig m, Member (State (Set.Set Constraint)) sig) => Term Monotype Meta -> Term Monotype Meta -> m ()
174187
unify t1 t2
175188
| t1 == t2 = pure ()
176189
| otherwise = modify (<> Set.singleton (t1 :===: t2))
177190

178-
type Substitution = IntMap.IntMap (Monotype Meta)
191+
type Substitution = IntMap.IntMap (Term Monotype Meta)
179192

180193
solve :: (Carrier sig m, Member (State Substitution) sig, MonadFail m) => Set.Set Constraint -> m ()
181194
solve cs = for_ cs solve
182195
where solve = \case
183196
-- FIXME: how do we enforce proper subtyping? row polymorphism or something?
184-
MRecord f1 :===: MRecord f2 -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> ()
185-
MArr a1 b1 :===: MArr a2 b2 -> solve (a1 :===: a2) *> solve (b1 :===: b2)
186-
MMeta m1 :===: MMeta m2 | m1 == m2 -> pure ()
187-
MMeta m1 :===: t2 -> do
197+
Term (MRecord f1) :===: Term (MRecord f2) -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> ()
198+
Term (MArr a1 b1) :===: Term (MArr a2 b2) -> solve (a1 :===: a2) *> solve (b1 :===: b2)
199+
Var m1 :===: Var m2 | m1 == m2 -> pure ()
200+
Var m1 :===: t2 -> do
188201
sol <- solution m1
189202
case sol of
190203
Just (_ := t1) -> solve (t1 :===: t2)
191204
Nothing | m1 `IntSet.member` mvs t2 -> fail ("Occurs check failure: " <> show m1 <> " :===: " <> show t2)
192205
| otherwise -> modify (IntMap.insert m1 t2 . subst (m1 := t2))
193-
t1 :===: MMeta m2 -> solve (MMeta m2 :===: t1)
206+
t1 :===: Var m2 -> solve (Var m2 :===: t1)
194207
t1 :===: t2 -> unless (t1 == t2) $ fail ("Type mismatch:\nexpected: " <> show t1 <> "\n actual: " <> show t2)
195208

196209
solution m = fmap (m :=) <$> gets (IntMap.lookup m)
@@ -202,31 +215,17 @@ substAll s a = foldl' (flip subst) a (map (uncurry (:=)) (IntMap.toList s))
202215
class FreeVariables t where
203216
mvs :: t -> IntSet.IntSet
204217

205-
instance FreeVariables (Monotype Meta) where
206-
mvs MUnit = mempty
207-
mvs MBool = mempty
208-
mvs MString = mempty
209-
mvs (MArr a b) = mvs a <> mvs b
210-
mvs (MMeta m) = IntSet.singleton m
211-
mvs (MRecord fs) = foldMap mvs fs
218+
instance FreeVariables (Term Monotype Meta) where
219+
mvs = foldMap IntSet.singleton
212220

213221
instance FreeVariables Constraint where
214222
mvs (t1 :===: t2) = mvs t1 <> mvs t2
215223

216224
class Substitutable t where
217225
subst :: Solution -> t -> t
218226

219-
instance Substitutable (Monotype Meta) where
220-
subst s con = case con of
221-
MUnit -> MUnit
222-
MBool -> MBool
223-
MString -> MString
224-
MArr a b -> MArr (subst s a) (subst s b)
225-
MMeta m'
226-
| m := t <- s
227-
, m == m' -> t
228-
| otherwise -> MMeta m'
229-
MRecord fs -> MRecord (subst s <$> fs)
227+
instance Substitutable (Term Monotype Meta) where
228+
subst (i' := t') t = t >>= \ i -> if i == i' then t' else Var i
230229

231230
instance Substitutable Constraint where
232231
subst s (t1 :===: t2) = subst s t1 :===: subst s t2

0 commit comments

Comments
 (0)