@@ -32,7 +32,7 @@ import Data.Traversable
3232import Nix.Atoms
3333import Nix.Expr
3434
35−getType :: NExprLoc -> (Either UnifyingError NTypeS, [(SrcSpan, Errors)])
35+getType :: NExprLoc -> (Either UnifyingError NType, [(SrcSpan, Errors)])
3636getType exp =
3737 let (((t, srcs), cons), errs) =
3838 run
@@ -48,36 +48,20 @@ getType exp =
4848newtype TypeVariable = TypeVariable Int
4949 deriving newtype (Show, Eq, Ord)
5050
51−data Constraint = !NTypeS :~ !NTypeS
51+data Constraint = !NType :~ !NType
5252
53−type NType = Fix NTypeF
53+newtype DeBrujin = DeBrujin {unDeBrujin :: Int}
54+ deriving newtype (Eq, Ord)
55+ deriving stock (Show)
5456
55−data NTypeF f
57+data NType
5658 = NTypeVariable !TypeVariable
59+ | NBrujin !DeBrujin
5760 | NAtomic !AtomicType
58− | List !f
59− | NAttrSet !(Map Text f)
60− | !f :-> !f
61− deriving stock (Functor, Eq, Ord, Show)
62−
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 <> ("}" <>)
68− where
69− x =
70− mconcat . fmap (\(k, v) -> (show k <>) <> (" :: " <>) <> s p v) $
71− M.toList a
72− liftShowsPrec s _ p (a :-> b) = s p a <> (" -> " <>) <> s p b
73−
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
80− liftEq _ _ _ = False
61+ | List !NType
62+ | NAttrSet !(Map Text NType)
63+ | !NType :-> !NType
64+ deriving stock (Eq, Ord, Show)
8165
8266data AtomicType
8367 = Integer
@@ -92,23 +76,14 @@ data AtomicType
9276class Free s where
9377 free :: s -> Set TypeVariable
9478
95−instance Free f => Free (NTypeF f) where
79+instance Free NType where
9680 free (NTypeVariable v) = S.singleton v
9781 free (NAtomic _) = S.empty
9882 free (List x) = free x
9983 free (NAttrSet attrs) = foldMap free . M.elems $ attrs
10084 free (x :-> y) = free x <> free y
10185
102−instance Free (f (Fix f)) => Free (Fix f) where
103− free (Fix f) = free f
104−
105−instance (Free (f (g x))) => Free (Compose f g x) where
106− free (Compose x) = free x
107−
108−instance Free f => Free (SchemeX f) where
109− free (Scheme vs x) = free x `S.difference` vs
110−
111−newtype Substitution = Substitution (Map TypeVariable NTypeS)
86+newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
11287
11388instance Semigroup Substitution where
11489 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)
@@ -116,33 +91,30 @@ instance Semigroup Substitution where
11691instance Monoid Substitution where
11792 mempty = Substitution mempty
11893
119−sub :: Substitution -> NTypeS -> NTypeS
120−sub (Substitution s) r'@(Fix (Compose (Scheme tvs r))) = case r of
121− NAtomic _ -> r'
94+sub :: Substitution -> NType -> NType
95+sub s r = case r of
96+ NAtomic _ -> r
12297 NTypeVariable x -> subTV x
123− List x -> rewrap . List $ sub' x
124− NAttrSet m -> rewrap . NAttrSet $ sub' <$> m
125− x :-> y -> rewrap $ sub' x :-> sub' y
98+ List x -> List $ sub s x
99+ NAttrSet m -> NAttrSet $ sub s <$> m
100+ x :-> y -> sub s x :-> sub s y
126101 where
127− s' = s `M.withoutKeys` tvs
128− subTV x = M.findWithDefault r' x s'
129− sub' = sub $ Substitution s'
130− rewrap = Fix . Compose . Scheme tvs
102+ subTV x = M.findWithDefault r x $ unSubstitution s
131103
132104subCon :: Substitution -> Constraint -> Constraint
133105subCon s (x :~ y) = sub s x :~ sub s y
134106
135107(<<-) ::
136108 TypeVariable ->
137− NTypeF (NTypeS) ->
109+ NType ->
138110 UnifyM Substitution
139111v <<- (NTypeVariable x) | v == x = return mempty
140−v <<- x | v `occursIn` x = throwError $ InfinityType $ normalType x
141−v <<- x = return $ Substitution $ M.singleton v $ normalType x
112+v <<- x | v `occursIn` x = throwError $ InfinityType x
113+v <<- x = return $ Substitution $ M.singleton v x
142114
143115unify :: Constraint -> UnifyM Substitution
144−unify (Fix (Compose (Scheme Sempty lhs')) :~ Fix (Compose (Scheme Sempty rhs'))) =
145− case (lhs', rhs') of
116+unify (lhs :~ rhs) =
117+ case (lhs, rhs) of
146118 (NAtomic x, NAtomic y) | x == y -> return mempty
147119 (NTypeVariable t, x) -> t <<- x
148120 (x, NTypeVariable t) -> t <<- x
@@ -163,24 +135,11 @@ solve (rest :|> c) = do
163135 s <- unify c
164136 solve $ fmap (subCon s) rest
165137
166−-- type NormalizeM = Eff '[State (Map TypeVariable TypeVariable), State (Set TypeVariable), Fresh]
167−
168−-- normalize :: NTypeS -> NormalizeM NTypeS
169−-- normalize (Fix (Compose u)) =
170−-- Fix . Compose <$> case u of
171−-- (Scheme tvs x) ->
172−
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
176−
177138pattern Sempty <- (S.null -> True) where Sempty = S.empty
178139
179140occursIn :: Free x => TypeVariable -> x -> Bool
180141occursIn t x = t `S.member` free x
181142
182−type NTypeS = Fix (Compose SchemeX NTypeF)
183−
184143data SchemeX x = Scheme (Set TypeVariable) x
185144 deriving stock (Eq, Ord, Show)
186145
@@ -191,7 +150,7 @@ instance Show1 SchemeX where
191150instance Eq1 SchemeX where
192151 liftEq eq (Scheme ts1 x1) (Scheme ts2 x2) = ts1 == ts2 && eq x1 x2
193152
194−-- type SchemeS = SchemeX NTypeS
153+-- type SchemeS = SchemeX NType
195154
196155data Errors
197156 = UndefinedVariable VarName
@@ -225,8 +184,8 @@ freshSrc = do
225184 return v
226185
227186data UnifyingError
228− = InfinityType NTypeS
229− | CanNotUnify (NTypeF NTypeS) (NTypeF NTypeS)
187+ = InfinityType NType
188+ | CanNotUnify NType NType
230189 deriving stock (Eq, Show)
231190
232191type UnifyM x = forall r. Members '[Error UnifyingError] r => Eff r x
@@ -265,18 +224,9 @@ throwSrcTV e = do
265224 throwSrc e
266225 freshSrc
267226
268−type VariableMap = Map VarName NTypeS
269−
270−normalType :: NTypeF NTypeS -> NTypeS
271−normalType = Fix . Compose . Scheme S.empty
272−
273−atomicType :: AtomicType -> NTypeS
274−atomicType = Fix . Compose . Scheme S.empty . NAtomic
275−
276−tv :: TypeVariable -> NTypeS
277−tv = Fix . Compose . Scheme S.empty . NTypeVariable
227+type VariableMap = Map VarName NType
278228
279−(~~) :: Member (Writer Constraint) r => NTypeS -> NTypeS -> Eff r ()
229+(~~) :: Member (Writer Constraint) r => NType -> NType -> Eff r ()
280230lhs ~~ rhs = tell $ lhs :~ rhs
281231
282232withBindings ::
@@ -286,27 +236,26 @@ withBindings ::
286236 Eff effs a
287237withBindings bindings = local (bindings <>)
288238
289−infer :: NExprLoc -> InferM NTypeS
239+infer :: NExprLoc -> InferM NType
290240infer (Fix (Compose (Ann src x))) = runReader src $ case x of
291− NConstant a -> return . normalType $
292− NAtomic $ case a of
293− NURI {} -> URI
294− NInt {} -> Integer
295− NFloat {} -> Float
296− NBool {} -> Bool
297− NNull {} -> Null
298− NLiteralPath {} -> return . normalType . NAtomic $ Path
299− NEnvPath {} -> return . normalType . NAtomic $ Path
300− NStr {} -> return . normalType $ NAtomic String
241+ NConstant a -> return . NAtomic $ case a of
242+ NURI {} -> URI
243+ NInt {} -> Integer
244+ NFloat {} -> Float
245+ NBool {} -> Bool
246+ NNull {} -> Null
247+ NLiteralPath {} -> return . NAtomic $ Path
248+ NEnvPath {} -> return . NAtomic $ Path
249+ NStr {} -> return $ NAtomic String
301250 NSym var ->
302251 ask @VariableMap
303− >>= maybe (tv <$> throwSrcTV (UndefinedVariable var)) return . M.lookup var
252+ >>= maybe (NTypeVariable <$> throwSrcTV (UndefinedVariable var)) return . M.lookup var
304253 NList xs -> do
305254 xs' <- traverse infer xs
306255 traverse_ tell . fmap (uncurry (:~)) $ zip xs' (tail xs')
307256 case xs' of
308− [] -> tv <$> freshSrc
309− y : _ -> return . normalType $ List y
257+ [] -> NTypeVariable <$> freshSrc
258+ y : _ -> return $ List y
310259 NUnary NNeg y -> do
311260 t <- infer y
312261 -- TODO: Infer either Float or Integer
@@ -314,7 +263,7 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
314263 return t
315264 NUnary NNot y -> do
316265 t <- infer y
317− t ~~ atomicType Bool
266+ t ~~ NAtomic Bool
318267 return t
319268 NBinary NUpdate lhs rhs -> do
320269 lhsT <- infer lhs
@@ -323,18 +272,18 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
323272 lhs' <- expectAttrSet lhsT
324273 rhs' <- expectAttrSet rhsT
325274 forM_ (M.toList $ M.intersectionWith (,) lhs' rhs') (\(_, (a, b)) -> a ~~ b)
326− return . normalType . NAttrSet $ rhs' <> lhs'
275+ return . NAttrSet $ rhs' <> lhs'
327276 NBinary NApp lhs rhs -> do
328277 lhst <- infer lhs
329278 rhst <- infer rhs
330− rest <- tv <$> freshSrc
331− lhst ~~ (normalType $ rhst :-> rest)
279+ rest <- NTypeVariable <$> freshSrc
280+ lhst ~~ (rhst :-> rest)
332281 return rhst
333282 NBinary NConcat lhs rhs -> do
334283 lhst <- infer lhs
335284 rhst <- infer rhs
336− t <- tv <$> freshSrc
337− let listt = normalType (List t)
285+ t <- NTypeVariable <$> freshSrc
286+ let listt = List t
338287 lhst ~~ listt
339288 rhst ~~ listt
340289 return $ listt
@@ -342,33 +291,33 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
342291 lhst <- infer lhs
343292 rhst <- infer rhs
344293 lhst ~~ rhst
345− return $ atomicType Bool
294+ return $ NAtomic Bool
346295 NBinary op lhs rhs
347296 | op `elem` [NLt, NLte, NGt, NGte, NPlus, NMinus, NMult, NDiv] -> do
348297 lhst <- infer lhs
349298 rhst <- infer rhs
350299 -- TODO: Infer lhst and rhst are either Integer or Double
351300 lhst ~~ rhst
352− return $ atomicType Bool
301+ return $ NAtomic Bool
353302 NBinary op lhs rhs | op `elem` [NAnd, NOr, NImpl] -> do
354303 lhst <- infer lhs
355304 rhst <- infer rhs
356− rhst ~~ atomicType Bool
357− lhst ~~ atomicType Bool
358− return $ atomicType Bool
305+ rhst ~~ NAtomic Bool
306+ lhst ~~ NAtomic Bool
307+ return $ NAtomic Bool
359308 NSelect r path' def -> do
360309 setT <- infer r
361310 path <- getPath path'
362311 resT <- case path of
363312 Just p -> lookupAttrSet p setT
364− Nothing -> tv <$> freshSrc
313+ Nothing -> NTypeVariable <$> freshSrc
365314 case def of
366315 Nothing -> return ()
367316 Just defR -> do
368317 defT <- infer defR
369318 defT ~~ resT
370319 return resT
371− NSet NNonRecursive xs -> normalType . NAttrSet <$> inferBinding xs
320+ NSet NNonRecursive xs -> NAttrSet <$> inferBinding xs
372321 NHasAttr attrSet path -> do
373322 setT <- infer attrSet
374323 expectAttrSet setT
@@ -377,26 +326,26 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
377326 (paramT, varMap :: VariableMap) <- case param of
378327 Param name -> do
379328 t <- freshSrc
380− return (tv t, M.singleton name $ tv t)
329+ return (NTypeVariable t, M.singleton name $ NTypeVariable t)
381330 ParamSet set variadic binding -> do
382331 setBindings <-
383332 M.fromList <$> set
384333 `for` ( \(name, def) -> do
385334 t <- case def of
386− Nothing -> tv <$> freshSrc
335+ Nothing -> NTypeVariable <$> freshSrc
387336 Just def' -> infer def'
388337 return (name, t)
389338 )
390− let setT = normalType . NAttrSet $ setBindings
339+ let setT = NAttrSet $ setBindings
391340 return (setT, maybe M.empty (`M.singleton` setT) binding <> setBindings)
392341 bodyT <- withBindings varMap $ infer body
393− return . normalType $ paramT :-> bodyT
342+ return $ paramT :-> bodyT
394343 NLet bindings body -> do
395344 bindingsT <- inferBinding bindings
396345 withBindings bindingsT $ infer body
397346 NIf cond t f -> do
398347 condT <- infer cond
399− condT ~~ atomicType Bool
348+ condT ~~ NAtomic Bool
400349 tT <- infer t
401350 fT <- infer f
402351 tT ~~ fT
@@ -407,11 +356,11 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
407356 withBindings vars $ infer body
408357 NAssert cond body -> do
409358 condT <- infer cond
410− condT ~~ atomicType Bool
359+ condT ~~ NAtomic Bool
411360 infer body
412− NSynHole _ -> tv <$> freshSrc
361+ NSynHole _ -> NTypeVariable <$> freshSrc
413362
414−inferBinding :: [Binding (Fix NExprLocF)] -> InferM' (Map VarName NTypeS)
363+inferBinding :: [Binding (Fix NExprLocF)] -> InferM' (Map VarName NType)
415364inferBinding bindings = do
416365 bindings' <-
417366 bindings >>.= \case
@@ -420,7 +369,7 @@ inferBinding bindings = do
420369 Nothing -> return []
421370 Just name -> do
422371 t <- infer r
423− return $ [stack ((,) <$> name) (normalType . NAttrSet . uncurry M.singleton) t]
372+ return $ [stack ((,) <$> name) (NAttrSet . uncurry M.singleton) t]
424373 Inherit attrSet keys src -> do
425374 vars <- case attrSet of
426375 Just attr -> do
@@ -435,13 +384,13 @@ inferBinding bindings = do
435384 Just r -> Just (name, r)
436385 return $ M.fromListWith mergeSetTypes bindings'
437386
438−expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NTypeS -> Eff r VariableMap
439−expectAttrSet (Fix (Compose (Scheme _ (NAttrSet x)))) = return x
440−expectAttrSet (Fix (Compose (Scheme _ g))) = do
387+expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NType -> Eff r VariableMap
388+expectAttrSet (NAttrSet x) = return x
389+expectAttrSet g = do
441390 throwSrc
442391 UnexpectedType
443− { expected = Fix $ NAttrSet M.empty,
444− got = Fix $ const (Fix $ NAtomic Null) <$> g
392+ { expected = NAttrSet M.empty,
393+ got = g
445394 }
446395 return M.empty
447396
@@ -458,9 +407,9 @@ stack (g :| gs) h x = g $ f gs
458407(>>.=) :: (Applicative f, Monad t, Traversable t) => t a -> (a -> f (t b)) -> f (t b)
459408ta >>.= f = join <$> traverse f ta
460409
461−mergeSetTypes :: NTypeS -> NTypeS -> NTypeS
462−mergeSetTypes (Fix (Compose (Scheme ts (NAttrSet ks)))) (Fix (Compose (Scheme ts' (NAttrSet ks')))) =
463− Fix . Compose . Scheme (ts' <> ts) . NAttrSet $ M.unionWith mergeSetTypes ks ks'
410+mergeSetTypes :: NType -> NType -> NType
411+mergeSetTypes (NAttrSet ks) (NAttrSet ks') =
412+ NAttrSet $ M.unionWith mergeSetTypes ks ks'
464413mergeSetTypes _ x = x
465414
466415-- TODO: process variables
@@ -501,8 +450,8 @@ lookupAttrSet ::
501450 ]
502451 r =>
503452 AttrSetPath ->
504− NTypeS ->
505− Eff r NTypeS
453+ NType ->
454+ Eff r NType
506455lookupAttrSet path = go (NE.toList path)
507456 where
508457 go ::
@@ -514,10 +463,10 @@ lookupAttrSet path = go (NE.toList path)
514463 ]
515464 r =>
516465 [VarName] ->
517− NTypeS ->
518− Eff r NTypeS
466+ NType ->
467+ Eff r NType
519468 go [] x = return x
520469 go (p : ps) x = do
521470 expectAttrSet x <&> M.lookup p >>= \case
522− Nothing -> tv <$> throwSrcTV (KeyNotPresent p)
471+ Nothing -> NTypeVariable <$> throwSrcTV (KeyNotPresent p)
523472 Just t -> go ps t