@@ -0,0 +1,523 @@
1+module Tix.Typechecker
2+ ( infer,
3+ solve,
4+ runFresh,
5+ runSeqWriter,
6+ getType,
7+ )
8+where
9+
10+import Control.Monad
11+import Control.Monad.Freer
12+import Control.Monad.Freer.Error
13+import Control.Monad.Freer.Internal (handleRelayS)
14+import Control.Monad.Freer.Reader
15+import Control.Monad.Freer.State
16+import Control.Monad.Freer.Writer
17+import Data.Fix
18+import Data.Foldable
19+import Data.Functor
20+import Data.Functor.Classes
21+import Data.List.NonEmpty (NonEmpty (..))
22+import qualified Data.List.NonEmpty as NE
23+import Data.Map.Strict (Map)
24+import qualified Data.Map.Strict as M
25+import Data.MonoTraversable
26+import Data.Sequence (Seq (..))
27+import Data.Sequences
28+import Data.Set (Set)
29+import qualified Data.Set as S
30+import Data.Text (Text)
31+import Data.Traversable
32+import Nix.Atoms
33+import Nix.Expr
34+
35+getType :: NExprLoc -> (Either UnifyingError NTypeS, [(SrcSpan, Errors)])
36+getType exp =
37+ let (((t, srcs), cons), errs) =
38+ run
39+ . runReader (M.empty :: VariableMap)
40+ . runSeqWriter @[(SrcSpan, Errors)]
41+ . runSeqWriter @(Seq Constraint)
42+ . runSeqWriter @[(TypeVariable, SrcSpan)]
43+ . runFresh
44+ $ infer exp
45+ s = run . runError @UnifyingError $ solve cons
46+ in ((`sub` t) <$> s, errs)
47+
48+newtype TypeVariable = TypeVariable Int
49+ deriving newtype (Show, Eq, Ord)
50+
51+data Constraint = !NTypeS :~ !NTypeS
52+
53+type NType = Fix NTypeF
54+
55+data NTypeF f
56+ = NTypeVariable !TypeVariable
57+ | 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
81+
82+data AtomicType
83+ = Integer
84+ | Float
85+ | Bool
86+ | String
87+ | Path
88+ | Null
89+ | URI
90+ deriving stock (Eq, Ord, Show)
91+
92+class Free s where
93+ free :: s -> Set TypeVariable
94+
95+instance Free f => Free (NTypeF f) where
96+ free (NTypeVariable v) = S.singleton v
97+ free (NAtomic _) = S.empty
98+ free (List x) = free x
99+ free (NAttrSet attrs) = foldMap free . M.elems $ attrs
100+ free (x :-> y) = free x <> free y
101+
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)
112+
113+instance Semigroup Substitution where
114+ x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)
115+
116+instance Monoid Substitution where
117+ mempty = Substitution mempty
118+
119+sub :: Substitution -> NTypeS -> NTypeS
120+sub (Substitution s) r'@(Fix (Compose (Scheme tvs r))) = case r of
121+ NAtomic _ -> r'
122+ 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
126+ 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
131+
132+subCon :: Substitution -> Constraint -> Constraint
133+subCon s (x :~ y) = sub s x :~ sub s y
134+
135+(<<-) ::
136+ TypeVariable ->
137+ NTypeF (NTypeS) ->
138+ UnifyM Substitution
139+v <<- (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
142+
143+unify :: Constraint -> UnifyM Substitution
144+unify (Fix (Compose (Scheme Sempty lhs')) :~ Fix (Compose (Scheme Sempty rhs'))) =
145+ case (lhs', rhs') of
146+ (NAtomic x, NAtomic y) | x == y -> return mempty
147+ (NTypeVariable t, x) -> t <<- x
148+ (x, NTypeVariable t) -> t <<- x
149+ (List x, List y) -> unify $ x :~ y
150+ (NAttrSet x, NAttrSet y) -> do
151+ foldr (\c s -> s >>= \s' -> (<> s') <$> unify (subCon s' c)) (pure mempty)
152+ . M.elems
153+ $ M.intersectionWith (:~) x y
154+ (x1 :-> y1, x2 :-> y2) -> do
155+ s <- unify (x1 :~ x2)
156+ s' <- unify $ subCon s $ y1 :~ y2
157+ return $ s' <> s
158+ (x, y) -> throwError $ CanNotUnify x y
159+
160+solve :: Seq Constraint -> UnifyM Substitution
161+solve Empty = return mempty
162+solve (rest :|> c) = do
163+ s <- unify c
164+ solve $ fmap (subCon s) rest
165+
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+
177+pattern Sempty <- (S.null -> True) where Sempty = S.empty
178+
179+occursIn :: Free x => TypeVariable -> x -> Bool
180+occursIn t x = t `S.member` free x
181+
182+type NTypeS = Fix (Compose SchemeX NTypeF)
183+
184+data SchemeX x = Scheme (Set TypeVariable) x
185+ deriving stock (Eq, Ord, Show)
186+
187+instance Show1 SchemeX where
188+ liftShowsPrec s _ p (Scheme Sempty x) = s p x
189+ liftShowsPrec s _ p (Scheme tvs x) = ((("forall " <> show tvs)) <>) <> s p x
190+
191+instance Eq1 SchemeX where
192+ liftEq eq (Scheme ts1 x1) (Scheme ts2 x2) = ts1 == ts2 && eq x1 x2
193+
194+-- type SchemeS = SchemeX NTypeS
195+
196+data Errors
197+ = UndefinedVariable VarName
198+ | UnexpectedType {expected :: NType, got :: NType}
199+ | KeyNotPresent Text
200+
201+data Fresh x where
202+ Fresh :: Fresh TypeVariable
203+
204+data ResumableExceptions x
205+
206+type Runner effect = forall effs a. Eff (effect ': effs) a -> Eff effs a
207+
208+runFresh :: Runner Fresh
209+runFresh =
210+ evalState (TypeVariable 0)
211+ . reinterpret
212+ ( \Fresh -> do
213+ (TypeVariable old) <- get
214+ put (TypeVariable $ old + 1)
215+ return (TypeVariable old)
216+ )
217+
218+freshSrc ::
219+ Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan)] r =>
220+ Eff r TypeVariable
221+freshSrc = do
222+ v <- send Fresh
223+ src <- ask @SrcSpan
224+ tell (v, src)
225+ return v
226+
227+data UnifyingError
228+ = InfinityType NTypeS
229+ | CanNotUnify (NTypeF NTypeS) (NTypeF NTypeS)
230+ deriving stock (Eq, Show)
231+
232+type UnifyM x = forall r. Members '[Error UnifyingError] r => Eff r x
233+
234+type InferEffs =
235+ '[ Fresh,
236+ Writer (TypeVariable, SrcSpan),
237+ Writer Constraint,
238+ Writer (SrcSpan, Errors),
239+ Reader VariableMap
240+ ]
241+
242+type InferM x = forall r. Members InferEffs r => Eff r x
243+
244+type InferM' x = forall r. Members (Reader SrcSpan ': InferEffs) r => Eff r x
245+
246+runSeqWriter :: forall s w r a. (IsSequence s, Element s ~ w) => Eff (Writer w ': r) a -> Eff r (a, s)
247+runSeqWriter = handleRelayS mempty (\s x -> return (x, s)) $ \s (Tell w) k -> k (cons w s) ()
248+
249+throwSrc :: Members '[Reader SrcSpan, Writer (SrcSpan, e)] r => e -> Eff r ()
250+throwSrc e = do
251+ src <- ask @SrcSpan
252+ tell (src, e)
253+
254+throwSrcTV ::
255+ Members
256+ '[ Reader SrcSpan,
257+ Writer (SrcSpan, e),
258+ Writer (TypeVariable, SrcSpan),
259+ Fresh
260+ ]
261+ r =>
262+ e ->
263+ Eff r TypeVariable
264+throwSrcTV e = do
265+ throwSrc e
266+ freshSrc
267+
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
278+
279+(~~) :: Member (Writer Constraint) r => NTypeS -> NTypeS -> Eff r ()
280+lhs ~~ rhs = tell $ lhs :~ rhs
281+
282+withBindings ::
283+ (Member (Reader r) effs, Semigroup r) =>
284+ r ->
285+ Eff effs a ->
286+ Eff effs a
287+withBindings bindings = local (bindings <>)
288+
289+infer :: NExprLoc -> InferM NTypeS
290+infer (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
301+ NSym var ->
302+ ask @VariableMap
303+ >>= maybe (tv <$> throwSrcTV (UndefinedVariable var)) return . M.lookup var
304+ NList xs -> do
305+ xs' <- traverse infer xs
306+ traverse_ tell . fmap (uncurry (:~)) $ zip xs' (tail xs')
307+ case xs' of
308+ [] -> tv <$> freshSrc
309+ y : _ -> return . normalType $ List y
310+ NUnary NNeg y -> do
311+ t <- infer y
312+ -- TODO: Infer either Float or Integer
313+ -- tell $ t :~ (normalType . NAtomic $ )
314+ return t
315+ NUnary NNot y -> do
316+ t <- infer y
317+ t ~~ atomicType Bool
318+ return t
319+ NBinary NUpdate lhs rhs -> do
320+ lhsT <- infer lhs
321+ rhsT <- infer rhs
322+ lhsT ~~ rhsT
323+ lhs' <- expectAttrSet lhsT
324+ rhs' <- expectAttrSet rhsT
325+ forM_ (M.toList $ M.intersectionWith (,) lhs' rhs') (\(_, (a, b)) -> a ~~ b)
326+ return . normalType . NAttrSet $ rhs' <> lhs'
327+ NBinary NApp lhs rhs -> do
328+ lhst <- infer lhs
329+ rhst <- infer rhs
330+ rest <- tv <$> freshSrc
331+ lhst ~~ (normalType $ rhst :-> rest)
332+ return rhst
333+ NBinary NConcat lhs rhs -> do
334+ lhst <- infer lhs
335+ rhst <- infer rhs
336+ t <- tv <$> freshSrc
337+ let listt = normalType (List t)
338+ lhst ~~ listt
339+ rhst ~~ listt
340+ return $ listt
341+ NBinary op lhs rhs | op `elem` [NEq, NNEq] -> do
342+ lhst <- infer lhs
343+ rhst <- infer rhs
344+ lhst ~~ rhst
345+ return $ atomicType Bool
346+ NBinary op lhs rhs
347+ | op `elem` [NLt, NLte, NGt, NGte, NPlus, NMinus, NMult, NDiv] -> do
348+ lhst <- infer lhs
349+ rhst <- infer rhs
350+ -- TODO: Infer lhst and rhst are either Integer or Double
351+ lhst ~~ rhst
352+ return $ atomicType Bool
353+ NBinary op lhs rhs | op `elem` [NAnd, NOr, NImpl] -> do
354+ lhst <- infer lhs
355+ rhst <- infer rhs
356+ rhst ~~ atomicType Bool
357+ lhst ~~ atomicType Bool
358+ return $ atomicType Bool
359+ NSelect r path' def -> do
360+ setT <- infer r
361+ path <- getPath path'
362+ resT <- case path of
363+ Just p -> lookupAttrSet p setT
364+ Nothing -> tv <$> freshSrc
365+ case def of
366+ Nothing -> return ()
367+ Just defR -> do
368+ defT <- infer defR
369+ defT ~~ resT
370+ return resT
371+ NSet NNonRecursive xs -> normalType . NAttrSet <$> inferBinding xs
372+ NHasAttr attrSet path -> do
373+ setT <- infer attrSet
374+ expectAttrSet setT
375+ return setT
376+ NAbs param body -> do
377+ (paramT, varMap :: VariableMap) <- case param of
378+ Param name -> do
379+ t <- freshSrc
380+ return (tv t, M.singleton name $ tv t)
381+ ParamSet set variadic binding -> do
382+ setBindings <-
383+ M.fromList <$> set
384+ `for` ( \(name, def) -> do
385+ t <- case def of
386+ Nothing -> tv <$> freshSrc
387+ Just def' -> infer def'
388+ return (name, t)
389+ )
390+ let setT = normalType . NAttrSet $ setBindings
391+ return (setT, maybe M.empty (`M.singleton` setT) binding <> setBindings)
392+ bodyT <- withBindings varMap $ infer body
393+ return . normalType $ paramT :-> bodyT
394+ NLet bindings body -> do
395+ bindingsT <- inferBinding bindings
396+ withBindings bindingsT $ infer body
397+ NIf cond t f -> do
398+ condT <- infer cond
399+ condT ~~ atomicType Bool
400+ tT <- infer t
401+ fT <- infer f
402+ tT ~~ fT
403+ return tT
404+ NWith set body -> do
405+ setT <- infer set
406+ vars <- expectAttrSet setT
407+ withBindings vars $ infer body
408+ NAssert cond body -> do
409+ condT <- infer cond
410+ condT ~~ atomicType Bool
411+ infer body
412+ NSynHole _ -> tv <$> freshSrc
413+
414+inferBinding :: [Binding (Fix NExprLocF)] -> InferM' (Map VarName NTypeS)
415+inferBinding bindings = do
416+ bindings' <-
417+ bindings >>.= \case
418+ (NamedVar path r src) -> do
419+ getPath path >>= \case
420+ Nothing -> return []
421+ Just name -> do
422+ t <- infer r
423+ return $ [stack ((,) <$> name) (normalType . NAttrSet . uncurry M.singleton) t]
424+ Inherit attrSet keys src -> do
425+ vars <- case attrSet of
426+ Just attr -> do
427+ t <- infer attr
428+ expectAttrSet t
429+ Nothing -> ask @VariableMap
430+ names <- catMaybes <$> traverse getKeyName keys
431+ return $
432+ catMaybes $
433+ names <&> \name -> case M.lookup name vars of
434+ Nothing -> Nothing
435+ Just r -> Just (name, r)
436+ return $ M.fromListWith mergeSetTypes bindings'
437+
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
441+ throwSrc
442+ UnexpectedType
443+ { expected = Fix $ NAttrSet M.empty,
444+ got = Fix $ const (Fix $ NAtomic Null) <$> g
445+ }
446+ return M.empty
447+
448+-- | Stacks functions recursively inside each other
449+-- >>> stack [f1, f2, f3] h x
450+-- f1 (h $ f2 (h $ f3 x))
451+stack :: forall x y. NonEmpty (x -> y) -> (y -> x) -> x -> y
452+stack (g :| gs) h x = g $ f gs
453+ where
454+ f :: [x -> y] -> x
455+ f [] = x
456+ f (k : ks) = h . k $ f ks
457+
458+(>>.=) :: (Applicative f, Monad t, Traversable t) => t a -> (a -> f (t b)) -> f (t b)
459+ta >>.= f = join <$> traverse f ta
460+
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'
464+mergeSetTypes _ x = x
465+
466+-- TODO: process variables
467+antiAntiQuote :: Antiquoted (NString r) r -> Maybe Text
468+antiAntiQuote (Plain s) = unNString s
469+antiAntiQuote (EscapedNewline) = Just "\n"
470+antiAntiQuote (Antiquoted _) = Nothing
471+
472+-- TODO: process variables
473+antiAntiQuoteText :: Antiquoted Text r -> Maybe Text
474+antiAntiQuoteText (Plain t) = Just t
475+antiAntiQuoteText EscapedNewline = Just "\n"
476+antiAntiQuoteText (Antiquoted _) = Nothing
477+
478+-- TODO: process variables
479+unNString :: NString r -> Maybe Text
480+unNString (DoubleQuoted ss) = foldMap antiAntiQuoteText ss
481+unNString (Indented _ ss) = foldMap antiAntiQuoteText ss
482+
483+getKeyName :: Monad m => NKeyName r -> m (Maybe VarName)
484+getKeyName (StaticKey k) = return $ Just k
485+getKeyName (DynamicKey k) = return $ antiAntiQuote k
486+
487+getPath ::
488+ (Traversable t, Monad f) =>
489+ t (NKeyName r) ->
490+ f (Maybe (t Text))
491+getPath path = sequence <$> traverse getKeyName path
492+
493+type AttrSetPath = NonEmpty Text
494+
495+lookupAttrSet ::
496+ Members
497+ '[ Reader SrcSpan,
498+ Writer (SrcSpan, Errors),
499+ Writer (TypeVariable, SrcSpan),
500+ Fresh
501+ ]
502+ r =>
503+ AttrSetPath ->
504+ NTypeS ->
505+ Eff r NTypeS
506+lookupAttrSet path = go (NE.toList path)
507+ where
508+ go ::
509+ Members
510+ '[ Reader SrcSpan,
511+ Writer (SrcSpan, Errors),
512+ Writer (TypeVariable, SrcSpan),
513+ Fresh
514+ ]
515+ r =>
516+ [VarName] ->
517+ NTypeS ->
518+ Eff r NTypeS
519+ go [] x = return x
520+ go (p : ps) x = do
521+ expectAttrSet x <&> M.lookup p >>= \case
522+ Nothing -> tv <$> throwSrcTV (KeyNotPresent p)
523+ Just t -> go ps t