@@ -32,7 +32,7 @@ import Data.Traversable
32import Nix.Atoms
32import Nix.Atoms
33import Nix.Expr
33import Nix.Expr
35−getType :: NExprLoc -> (Either UnifyingError NTypeS, [(SrcSpan, Errors)])
35+getType :: NExprLoc -> (Either UnifyingError NType, [(SrcSpan, Errors)])
36getType exp =
36getType exp =
37 let (((t, srcs), cons), errs) =
37 let (((t, srcs), cons), errs) =
@@ -48,36 +48,20 @@ getType exp =
48newtype TypeVariable = TypeVariable Int
48newtype TypeVariable = TypeVariable Int
49 deriving newtype (Show, Eq, Ord)
49 deriving newtype (Show, Eq, Ord)
51−data Constraint = !NTypeS :~ !NTypeS
51+data Constraint = !NType :~ !NType
53−type NType = Fix NTypeF
53+newtype DeBrujin = DeBrujin {unDeBrujin :: Int}
54+ deriving newtype (Eq, Ord)
55+ deriving stock (Show)
55−data NTypeF f
57+data NType
56 = NTypeVariable !TypeVariable
58 = NTypeVariable !TypeVariable
57 | NAtomic !AtomicType
60 | NAtomic !AtomicType
58− | List !f
61+ | List !NType
59− | NAttrSet !(Map Text f)
62+ | NAttrSet !(Map Text NType)
60− | !f :-> !f
63+ | !NType :-> !NType
61− deriving stock (Functor, Eq, Ord, Show)
64+ deriving stock (Eq, Ord, Show)
63−instance Show1 NTypeF where
64− liftShowsPrec s _ p (NAtomic a) = (show a <>)
65− liftShowsPrec s _ p (NTypeVariable a) = (show a <>)
66− liftShowsPrec s _ p (List a) = ("[" <>) <> s p a <> ("]" <>)
67− liftShowsPrec s _ p (NAttrSet a) = ("{" <>) <> x <> ("}" <>)
70− mconcat . fmap (\(k, v) -> (show k <>) <> (" :: " <>) <> s p v) $
72− liftShowsPrec s _ p (a :-> b) = s p a <> (" -> " <>) <> s p b
74−instance Eq1 NTypeF where
75− liftEq _ (NTypeVariable x) (NTypeVariable y) = x == y
76− liftEq _ (NAtomic x) (NAtomic y) = x == y
77− liftEq eq (List x) (List y) = eq x y
78− liftEq eq (NAttrSet x) (NAttrSet y) = liftEq eq x y
79− liftEq eq (x1 :-> y1) (x2 :-> y2) = eq x1 x2 && eq y1 y2
82data AtomicType
66data AtomicType
@@ -92,23 +76,14 @@ data AtomicType
92class Free s where
76class Free s where
93 free :: s -> Set TypeVariable
77 free :: s -> Set TypeVariable
95−instance Free f => Free (NTypeF f) where
79+instance Free NType where
96 free (NTypeVariable v) = S.singleton v
80 free (NTypeVariable v) = S.singleton v
97 free (NAtomic _) = S.empty
81 free (NAtomic _) = S.empty
98 free (List x) = free x
82 free (List x) = free x
99 free (NAttrSet attrs) = foldMap free . M.elems $ attrs
83 free (NAttrSet attrs) = foldMap free . M.elems $ attrs
100 free (x :-> y) = free x <> free y
84 free (x :-> y) = free x <> free y
102−instance Free (f (Fix f)) => Free (Fix f) where
103− free (Fix f) = free f
105−instance (Free (f (g x))) => Free (Compose f g x) where
106− free (Compose x) = free x
108−instance Free f => Free (SchemeX f) where
109− free (Scheme vs x) = free x `S.difference` vs
111−newtype Substitution = Substitution (Map TypeVariable NTypeS)
86+newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
113instance Semigroup Substitution where
88instance Semigroup Substitution where
114 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)
89 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)
@@ -116,33 +91,30 @@ instance Semigroup Substitution where
116instance Monoid Substitution where
91instance Monoid Substitution where
117 mempty = Substitution mempty
92 mempty = Substitution mempty
119−sub :: Substitution -> NTypeS -> NTypeS
94+sub :: Substitution -> NType -> NType
120−sub (Substitution s) r'@(Fix (Compose (Scheme tvs r))) = case r of
95+sub s r = case r of
121− NAtomic _ -> r'
96+ NAtomic _ -> r
122 NTypeVariable x -> subTV x
97 NTypeVariable x -> subTV x
123− List x -> rewrap . List $ sub' x
98+ List x -> List $ sub s x
124− NAttrSet m -> rewrap . NAttrSet $ sub' <$> m
99+ NAttrSet m -> NAttrSet $ sub s <$> m
125− x :-> y -> rewrap $ sub' x :-> sub' y
100+ x :-> y -> sub s x :-> sub s y
127− s' = s `M.withoutKeys` tvs
128− subTV x = M.findWithDefault r' x s'
102+ subTV x = M.findWithDefault r x $ unSubstitution s
129− sub' = sub $ Substitution s'
130− rewrap = Fix . Compose . Scheme tvs
132subCon :: Substitution -> Constraint -> Constraint
104subCon :: Substitution -> Constraint -> Constraint
133subCon s (x :~ y) = sub s x :~ sub s y
105subCon s (x :~ y) = sub s x :~ sub s y
136 TypeVariable ->
108 TypeVariable ->
137− NTypeF (NTypeS) ->
109+ NType ->
138 UnifyM Substitution
110 UnifyM Substitution
139v <<- (NTypeVariable x) | v == x = return mempty
111v <<- (NTypeVariable x) | v == x = return mempty
140−v <<- x | v `occursIn` x = throwError $ InfinityType $ normalType x
112+v <<- x | v `occursIn` x = throwError $ InfinityType x
141−v <<- x = return $ Substitution $ M.singleton v $ normalType x
113+v <<- x = return $ Substitution $ M.singleton v x
143unify :: Constraint -> UnifyM Substitution
115unify :: Constraint -> UnifyM Substitution
144−unify (Fix (Compose (Scheme Sempty lhs')) :~ Fix (Compose (Scheme Sempty rhs'))) =
116+unify (lhs :~ rhs) =
145− case (lhs', rhs') of
117+ case (lhs, rhs) of
146 (NAtomic x, NAtomic y) | x == y -> return mempty
118 (NAtomic x, NAtomic y) | x == y -> return mempty
147 (NTypeVariable t, x) -> t <<- x
119 (NTypeVariable t, x) -> t <<- x
148 (x, NTypeVariable t) -> t <<- x
120 (x, NTypeVariable t) -> t <<- x
@@ -163,24 +135,11 @@ solve (rest :|> c) = do
163 s <- unify c
135 s <- unify c
164 solve $ fmap (subCon s) rest
136 solve $ fmap (subCon s) rest
166−-- type NormalizeM = Eff '[State (Map TypeVariable TypeVariable), State (Set TypeVariable), Fresh]
168−-- normalize :: NTypeS -> NormalizeM NTypeS
169−-- normalize (Fix (Compose u)) =
170−-- Fix . Compose <$> case u of
173−-- normalize :: SchemeX (NTypeF NTypeS) -> SchemeX (NTypeF NTypeS)
174−-- normalize (Scheme tvs t) = case t of
175−-- (NTypeVariable t) -> if t `S.member` tvs then
177pattern Sempty <- (S.null -> True) where Sempty = S.empty
138pattern Sempty <- (S.null -> True) where Sempty = S.empty
179occursIn :: Free x => TypeVariable -> x -> Bool
140occursIn :: Free x => TypeVariable -> x -> Bool
180occursIn t x = t `S.member` free x
141occursIn t x = t `S.member` free x
182−type NTypeS = Fix (Compose SchemeX NTypeF)
184data SchemeX x = Scheme (Set TypeVariable) x
143data SchemeX x = Scheme (Set TypeVariable) x
185 deriving stock (Eq, Ord, Show)
144 deriving stock (Eq, Ord, Show)
@@ -191,7 +150,7 @@ instance Show1 SchemeX where
191instance Eq1 SchemeX where
150instance Eq1 SchemeX where
192 liftEq eq (Scheme ts1 x1) (Scheme ts2 x2) = ts1 == ts2 && eq x1 x2
151 liftEq eq (Scheme ts1 x1) (Scheme ts2 x2) = ts1 == ts2 && eq x1 x2
194−-- type SchemeS = SchemeX NTypeS
153+-- type SchemeS = SchemeX NType
196data Errors
155data Errors
197 = UndefinedVariable VarName
156 = UndefinedVariable VarName
@@ -225,8 +184,8 @@ freshSrc = do
227data UnifyingError
186data UnifyingError
228− = InfinityType NTypeS
187+ = InfinityType NType
229− | CanNotUnify (NTypeF NTypeS) (NTypeF NTypeS)
188+ | CanNotUnify NType NType
230 deriving stock (Eq, Show)
189 deriving stock (Eq, Show)
232type UnifyM x = forall r. Members '[Error UnifyingError] r => Eff r x
191type UnifyM x = forall r. Members '[Error UnifyingError] r => Eff r x
@@ -265,18 +224,9 @@ throwSrcTV e = do
265 throwSrc e
224 throwSrc e
268−type VariableMap = Map VarName NTypeS
227+type VariableMap = Map VarName NType
270−normalType :: NTypeF NTypeS -> NTypeS
271−normalType = Fix . Compose . Scheme S.empty
273−atomicType :: AtomicType -> NTypeS
274−atomicType = Fix . Compose . Scheme S.empty . NAtomic
276−tv :: TypeVariable -> NTypeS
277−tv = Fix . Compose . Scheme S.empty . NTypeVariable
279−(~~) :: Member (Writer Constraint) r => NTypeS -> NTypeS -> Eff r ()
229+(~~) :: Member (Writer Constraint) r => NType -> NType -> Eff r ()
280lhs ~~ rhs = tell $ lhs :~ rhs
230lhs ~~ rhs = tell $ lhs :~ rhs
282withBindings ::
232withBindings ::
@@ -286,27 +236,26 @@ withBindings ::
286 Eff effs a
236 Eff effs a
287withBindings bindings = local (bindings <>)
237withBindings bindings = local (bindings <>)
289−infer :: NExprLoc -> InferM NTypeS
239+infer :: NExprLoc -> InferM NType
290infer (Fix (Compose (Ann src x))) = runReader src $ case x of
240infer (Fix (Compose (Ann src x))) = runReader src $ case x of
291− NConstant a -> return . normalType $
292− NAtomic $ case a of
241+ NConstant a -> return . NAtomic $ case a of
293− NURI {} -> URI
242+ NURI {} -> URI
294− NInt {} -> Integer
243+ NInt {} -> Integer
295− NFloat {} -> Float
244+ NFloat {} -> Float
296− NBool {} -> Bool
245+ NBool {} -> Bool
297− NNull {} -> Null
246+ NNull {} -> Null
298− NLiteralPath {} -> return . normalType . NAtomic $ Path
247+ NLiteralPath {} -> return . NAtomic $ Path
299− NEnvPath {} -> return . normalType . NAtomic $ Path
248+ NEnvPath {} -> return . NAtomic $ Path
300− NStr {} -> return . normalType $ NAtomic String
249+ NStr {} -> return $ NAtomic String
301 NSym var ->
250 NSym var ->
302 ask @VariableMap
251 ask @VariableMap
303− >>= maybe (tv <$> throwSrcTV (UndefinedVariable var)) return . M.lookup var
252+ >>= maybe (NTypeVariable <$> throwSrcTV (UndefinedVariable var)) return . M.lookup var
304 NList xs -> do
253 NList xs -> do
305 xs' <- traverse infer xs
254 xs' <- traverse infer xs
306 traverse_ tell . fmap (uncurry (:~)) $ zip xs' (tail xs')
255 traverse_ tell . fmap (uncurry (:~)) $ zip xs' (tail xs')
307 case xs' of
256 case xs' of
308− [] -> tv <$> freshSrc
257+ [] -> NTypeVariable <$> freshSrc
309− y : _ -> return . normalType $ List y
258+ y : _ -> return $ List y
310 NUnary NNeg y -> do
259 NUnary NNeg y -> do
311 t <- infer y
260 t <- infer y
312 -- TODO: Infer either Float or Integer
261 -- TODO: Infer either Float or Integer
@@ -314,7 +263,7 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
315 NUnary NNot y -> do
264 NUnary NNot y -> do
316 t <- infer y
265 t <- infer y
317− t ~~ atomicType Bool
266+ t ~~ NAtomic Bool
319 NBinary NUpdate lhs rhs -> do
268 NBinary NUpdate lhs rhs -> do
320 lhsT <- infer lhs
269 lhsT <- infer lhs
@@ -323,18 +272,18 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
323 lhs' <- expectAttrSet lhsT
272 lhs' <- expectAttrSet lhsT
324 rhs' <- expectAttrSet rhsT
273 rhs' <- expectAttrSet rhsT
325 forM_ (M.toList $ M.intersectionWith (,) lhs' rhs') (\(_, (a, b)) -> a ~~ b)
274 forM_ (M.toList $ M.intersectionWith (,) lhs' rhs') (\(_, (a, b)) -> a ~~ b)
326− return . normalType . NAttrSet $ rhs' <> lhs'
275+ return . NAttrSet $ rhs' <> lhs'
327 NBinary NApp lhs rhs -> do
276 NBinary NApp lhs rhs -> do
328 lhst <- infer lhs
277 lhst <- infer lhs
329 rhst <- infer rhs
278 rhst <- infer rhs
330− rest <- tv <$> freshSrc
279+ rest <- NTypeVariable <$> freshSrc
331− lhst ~~ (normalType $ rhst :-> rest)
280+ lhst ~~ (rhst :-> rest)
332 return rhst
281 return rhst
333 NBinary NConcat lhs rhs -> do
282 NBinary NConcat lhs rhs -> do
334 lhst <- infer lhs
283 lhst <- infer lhs
335 rhst <- infer rhs
284 rhst <- infer rhs
336− t <- tv <$> freshSrc
285+ t <- NTypeVariable <$> freshSrc
337− let listt = normalType (List t)
286+ let listt = List t
338 lhst ~~ listt
287 lhst ~~ listt
339 rhst ~~ listt
288 rhst ~~ listt
340 return $ listt
289 return $ listt
@@ -342,33 +291,33 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
342 lhst <- infer lhs
291 lhst <- infer lhs
343 rhst <- infer rhs
292 rhst <- infer rhs
344 lhst ~~ rhst
293 lhst ~~ rhst
345− return $ atomicType Bool
294+ return $ NAtomic Bool
346 NBinary op lhs rhs
295 NBinary op lhs rhs
347 | op `elem` [NLt, NLte, NGt, NGte, NPlus, NMinus, NMult, NDiv] -> do
296 | op `elem` [NLt, NLte, NGt, NGte, NPlus, NMinus, NMult, NDiv] -> do
348 lhst <- infer lhs
297 lhst <- infer lhs
349 rhst <- infer rhs
298 rhst <- infer rhs
350 -- TODO: Infer lhst and rhst are either Integer or Double
299 -- TODO: Infer lhst and rhst are either Integer or Double
351 lhst ~~ rhst
300 lhst ~~ rhst
352− return $ atomicType Bool
301+ return $ NAtomic Bool
353 NBinary op lhs rhs | op `elem` [NAnd, NOr, NImpl] -> do
302 NBinary op lhs rhs | op `elem` [NAnd, NOr, NImpl] -> do
354 lhst <- infer lhs
303 lhst <- infer lhs
355 rhst <- infer rhs
304 rhst <- infer rhs
356− rhst ~~ atomicType Bool
305+ rhst ~~ NAtomic Bool
357− lhst ~~ atomicType Bool
306+ lhst ~~ NAtomic Bool
358− return $ atomicType Bool
307+ return $ NAtomic Bool
359 NSelect r path' def -> do
308 NSelect r path' def -> do
360 setT <- infer r
309 setT <- infer r
361 path <- getPath path'
310 path <- getPath path'
362 resT <- case path of
311 resT <- case path of
363 Just p -> lookupAttrSet p setT
312 Just p -> lookupAttrSet p setT
364− Nothing -> tv <$> freshSrc
313+ Nothing -> NTypeVariable <$> freshSrc
365 case def of
314 case def of
366 Nothing -> return ()
315 Nothing -> return ()
367 Just defR -> do
316 Just defR -> do
368 defT <- infer defR
317 defT <- infer defR
369 defT ~~ resT
318 defT ~~ resT
370 return resT
319 return resT
371− NSet NNonRecursive xs -> normalType . NAttrSet <$> inferBinding xs
320+ NSet NNonRecursive xs -> NAttrSet <$> inferBinding xs
372 NHasAttr attrSet path -> do
321 NHasAttr attrSet path -> do
373 setT <- infer attrSet
322 setT <- infer attrSet
374 expectAttrSet setT
323 expectAttrSet setT
@@ -377,26 +326,26 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
377 (paramT, varMap :: VariableMap) <- case param of
326 (paramT, varMap :: VariableMap) <- case param of
378 Param name -> do
327 Param name -> do
379 t <- freshSrc
328 t <- freshSrc
380− return (tv t, M.singleton name $ tv t)
329+ return (NTypeVariable t, M.singleton name $ NTypeVariable t)
381 ParamSet set variadic binding -> do
330 ParamSet set variadic binding -> do
382 setBindings <-
331 setBindings <-
383 M.fromList <$> set
332 M.fromList <$> set
384 `for` ( \(name, def) -> do
333 `for` ( \(name, def) -> do
385 t <- case def of
334 t <- case def of
386− Nothing -> tv <$> freshSrc
335+ Nothing -> NTypeVariable <$> freshSrc
387 Just def' -> infer def'
336 Just def' -> infer def'
388 return (name, t)
337 return (name, t)
390− let setT = normalType . NAttrSet $ setBindings
339+ let setT = NAttrSet $ setBindings
391 return (setT, maybe M.empty (`M.singleton` setT) binding <> setBindings)
340 return (setT, maybe M.empty (`M.singleton` setT) binding <> setBindings)
392 bodyT <- withBindings varMap $ infer body
341 bodyT <- withBindings varMap $ infer body
393− return . normalType $ paramT :-> bodyT
342+ return $ paramT :-> bodyT
394 NLet bindings body -> do
343 NLet bindings body -> do
395 bindingsT <- inferBinding bindings
344 bindingsT <- inferBinding bindings
396 withBindings bindingsT $ infer body
345 withBindings bindingsT $ infer body
397 NIf cond t f -> do
346 NIf cond t f -> do
398 condT <- infer cond
347 condT <- infer cond
399− condT ~~ atomicType Bool
348+ condT ~~ NAtomic Bool
400 tT <- infer t
349 tT <- infer t
401 fT <- infer f
350 fT <- infer f
@@ -407,11 +356,11 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
407 withBindings vars $ infer body
356 withBindings vars $ infer body
408 NAssert cond body -> do
357 NAssert cond body -> do
409 condT <- infer cond
358 condT <- infer cond
410− condT ~~ atomicType Bool
359+ condT ~~ NAtomic Bool
411 infer body
360 infer body
412− NSynHole _ -> tv <$> freshSrc
361+ NSynHole _ -> NTypeVariable <$> freshSrc
414−inferBinding :: [Binding (Fix NExprLocF)] -> InferM' (Map VarName NTypeS)
363+inferBinding :: [Binding (Fix NExprLocF)] -> InferM' (Map VarName NType)
415inferBinding bindings = do
364inferBinding bindings = do
416 bindings' <-
365 bindings' <-
417 bindings >>.= \case
366 bindings >>.= \case
@@ -420,7 +369,7 @@ inferBinding bindings = do
420 Nothing -> return []
369 Nothing -> return []
421 Just name -> do
370 Just name -> do
422 t <- infer r
371 t <- infer r
423− return $ [stack ((,) <$> name) (normalType . NAttrSet . uncurry M.singleton) t]
372+ return $ [stack ((,) <$> name) (NAttrSet . uncurry M.singleton) t]
424 Inherit attrSet keys src -> do
373 Inherit attrSet keys src -> do
425 vars <- case attrSet of
374 vars <- case attrSet of
426 Just attr -> do
375 Just attr -> do
@@ -435,13 +384,13 @@ inferBinding bindings = do
435 Just r -> Just (name, r)
384 Just r -> Just (name, r)
436 return $ M.fromListWith mergeSetTypes bindings'
385 return $ M.fromListWith mergeSetTypes bindings'
438−expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NTypeS -> Eff r VariableMap
387+expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NType -> Eff r VariableMap
439−expectAttrSet (Fix (Compose (Scheme _ (NAttrSet x)))) = return x
388+expectAttrSet (NAttrSet x) = return x
440−expectAttrSet (Fix (Compose (Scheme _ g))) = do
389+expectAttrSet g = do
442 UnexpectedType
391 UnexpectedType
443− { expected = Fix $ NAttrSet M.empty,
392+ { expected = NAttrSet M.empty,
444− got = Fix $ const (Fix $ NAtomic Null) <$> g
393+ got = g
446 return M.empty
395 return M.empty
@@ -458,9 +407,9 @@ stack (g :| gs) h x = g $ f gs
458(>>.=) :: (Applicative f, Monad t, Traversable t) => t a -> (a -> f (t b)) -> f (t b)
407(>>.=) :: (Applicative f, Monad t, Traversable t) => t a -> (a -> f (t b)) -> f (t b)
459ta >>.= f = join <$> traverse f ta
408ta >>.= f = join <$> traverse f ta
461−mergeSetTypes :: NTypeS -> NTypeS -> NTypeS
410+mergeSetTypes :: NType -> NType -> NType
462−mergeSetTypes (Fix (Compose (Scheme ts (NAttrSet ks)))) (Fix (Compose (Scheme ts' (NAttrSet ks')))) =
411+mergeSetTypes (NAttrSet ks) (NAttrSet ks') =
463− Fix . Compose . Scheme (ts' <> ts) . NAttrSet $ M.unionWith mergeSetTypes ks ks'
412+ NAttrSet $ M.unionWith mergeSetTypes ks ks'
464mergeSetTypes _ x = x
413mergeSetTypes _ x = x
466-- TODO: process variables
415-- TODO: process variables
@@ -501,8 +450,8 @@ lookupAttrSet ::
503 AttrSetPath ->
452 AttrSetPath ->
504− NTypeS ->
453+ NType ->
505− Eff r NTypeS
454+ Eff r NType
506lookupAttrSet path = go (NE.toList path)
455lookupAttrSet path = go (NE.toList path)
@@ -514,10 +463,10 @@ lookupAttrSet path = go (NE.toList path)
516 [VarName] ->
465 [VarName] ->
517− NTypeS ->
466+ NType ->
518− Eff r NTypeS
467+ Eff r NType
519 go [] x = return x
468 go [] x = return x
520 go (p : ps) x = do
469 go (p : ps) x = do
521 expectAttrSet x <&> M.lookup p >>= \case
470 expectAttrSet x <&> M.lookup p >>= \case
522− Nothing -> tv <$> throwSrcTV (KeyNotPresent p)
471+ Nothing -> NTypeVariable <$> throwSrcTV (KeyNotPresent p)
523 Just t -> go ps t
472 Just t -> go ps t