diff --git a/semantic-core/src/Analysis/Typecheck.hs b/semantic-core/src/Analysis/Typecheck.hs index d0d0bbdab..4c83a933f 100644 --- a/semantic-core/src/Analysis/Typecheck.hs +++ b/semantic-core/src/Analysis/Typecheck.hs @@ -1,11 +1,8 @@ -{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, RecordWildCards, ScopedTypeVariables, TypeApplications #-} +{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, QuantifiedConstraints, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators #-} module Analysis.Typecheck ( Monotype (..) , Meta -, Polytype (PForAll, PBool, PFree, PArr) -, Scope -, Analysis.Typecheck.bind -, Analysis.Typecheck.instantiate +, Polytype (..) , typecheckingFlowInsensitive , typecheckingAnalysis ) where @@ -13,15 +10,16 @@ module Analysis.Typecheck import Analysis.Eval import Analysis.FlowInsensitive import Control.Applicative (Alternative (..)) -import Control.Effect +import Control.Effect.Carrier import Control.Effect.Fail import Control.Effect.Fresh as Fresh import Control.Effect.Reader hiding (Local) import Control.Effect.State import Control.Monad (unless) +import Control.Monad.Module import qualified Data.Core as Core import Data.File -import Data.Foldable (foldl', for_) +import Data.Foldable (for_) import Data.Function (fix) import Data.Functor (($>)) import qualified Data.IntMap as IntMap @@ -29,102 +27,84 @@ import qualified Data.IntSet as IntSet import Data.List.NonEmpty (nonEmpty) import Data.Loc import qualified Data.Map as Map +import Data.Maybe (fromJust, fromMaybe) import Data.Name as Name +import Data.Scope import qualified Data.Set as Set import Data.Stack import Data.Term +import Data.Void +import GHC.Generics (Generic1) import Prelude hiding (fail) -data Monotype a - = MBool - | MUnit - | MString - | MMeta a - | MFree Gensym - | MArr (Monotype a) (Monotype a) - | MRecord (Map.Map User (Monotype a)) - deriving (Eq, Functor, Ord, Show) +data Monotype f a + = Bool + | Unit + | String + | Arr (f a) (f a) + | Record (Map.Map User (f a)) + deriving (Foldable, Functor, Generic1, Traversable) + +deriving instance (Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (Monotype f a) +deriving instance (Ord a, forall a . Eq a => Eq (f a) + , forall a . Ord a => Ord (f a), Monad f) => Ord (Monotype f a) +deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Monotype f a) + +instance HFunctor Monotype +instance RightModule Monotype where + Unit >>=* _ = Unit + Bool >>=* _ = Bool + String >>=* _ = String + Arr a b >>=* f = Arr (a >>= f) (b >>= f) + Record m >>=* f = Record ((>>= f) <$> m) type Meta = Int -data Polytype - = PForAll Scope - | PUnit - | PBool - | PString - | PBound Int - | PFree Gensym - | PArr Polytype Polytype - | PRecord (Map.Map User Polytype) - deriving (Eq, Ord, Show) +newtype Polytype f a = PForAll (Scope () f a) + deriving (Foldable, Functor, Generic1, Traversable) -newtype Scope = Scope Polytype - deriving (Eq, Ord, Show) +deriving instance (Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (Polytype f a) +deriving instance (Ord a, forall a . Eq a => Eq (f a) + , forall a . Ord a => Ord (f a), Monad f) => Ord (Polytype f a) +deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Polytype f a) -forAll :: Gensym -> Polytype -> Polytype -forAll n body = PForAll (Analysis.Typecheck.bind n body) +instance HFunctor Polytype +instance RightModule Polytype where + PForAll b >>=* f = PForAll (b >>=* f) -forAlls :: Foldable t => t Gensym -> Polytype -> Polytype + +forAll :: (Eq a, Carrier sig m, Member Polytype sig) => a -> m a -> m a +forAll n body = send (PForAll (Data.Scope.bind1 n body)) + +forAlls :: (Eq a, Carrier sig m, Member Polytype sig, Foldable t) => t a -> m a -> m a forAlls ns body = foldr forAll body ns -generalize :: (Carrier sig m, Member Naming sig) => Monotype Meta -> m Polytype -generalize ty = namespace "generalize" $ do - Gensym root _ <- Name.fresh - pure (forAlls (map (Gensym root) (IntSet.toList (mvs ty))) (fold root ty)) - where fold root = \case - MUnit -> PUnit - MBool -> PBool - MString -> PString - MMeta i -> PFree (Gensym root i) - MFree n -> PFree n - MArr a b -> PArr (fold root a) (fold root b) - MRecord fs -> PRecord (fold root <$> fs) - --- | Bind occurrences of a 'Gensym' in a 'Polytype' term, producing a 'Scope' in which the 'Gensym' is bound. -bind :: Gensym -> Polytype -> Scope -bind name = Scope . substIn (\ i n -> if name == n then PBound i else PFree n) (const PBound) - --- | Substitute a 'Polytype' term for the free variable in a given 'Scope', producing a closed 'Polytype' term. -instantiate :: Polytype -> Scope -> Polytype -instantiate image (Scope body) = substIn (const PFree) (\ i j -> if i == j then image else PBound j) body - -substIn :: (Int -> Gensym -> Polytype) - -> (Int -> Int -> Polytype) - -> Polytype - -> Polytype -substIn free bound = go 0 - where go i (PFree name) = free i name - go i (PBound j) = bound i j - go i (PForAll (Scope body)) = PForAll (Scope (go (succ i) body)) - go _ PUnit = PUnit - go _ PBool = PBool - go _ PString = PString - go i (PArr a b) = PArr (go i a) (go i b) - go i (PRecord fs) = PRecord (go i <$> fs) +generalize :: Term Monotype Meta -> Term (Polytype :+: Monotype) Void +generalize ty = fromJust (closed (forAlls (IntSet.toList (mvs ty)) (hoistTerm R ty))) -typecheckingFlowInsensitive :: [File (Term Core.Core Name)] -> (Heap Name (Monotype Meta), [File (Either (Loc, String) Polytype)]) +typecheckingFlowInsensitive :: [File (Term Core.Core Name)] -> (Heap Name (Term Monotype Meta), [File (Either (Loc, String) (Term (Polytype :+: Monotype) Void))]) typecheckingFlowInsensitive = run . runFresh . runNaming . runHeap (Gen (Gensym (Nil :> "root") 0)) - . (>>= traverse (traverse (traverse generalize))) + . fmap (fmap (fmap (fmap generalize))) . traverse runFile runFile :: ( Carrier sig m , Effect sig , Member Fresh sig , Member Naming sig - , Member (State (Heap Name (Monotype Meta))) sig + , Member (State (Heap Name (Term Monotype Meta))) sig ) => File (Term Core.Core Name) - -> m (File (Either (Loc, String) (Monotype Meta))) + -> m (File (Either (Loc, String) (Term Monotype Meta))) runFile file = traverse run file where run = (\ m -> do (subst, t) <- m - modify @(Heap Name (Monotype Meta)) (substAll subst) + modify @(Heap Name (Term Monotype Meta)) (fmap (Set.map (substAll subst))) pure (substAll subst <$> t)) . runState (mempty :: Substitution) . runReader (fileLoc file) @@ -139,7 +119,7 @@ runFile file = traverse run file v <$ for_ bs (unify v)) . convergeTerm (fix (cacheTerm . eval typecheckingAnalysis)) -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 +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 typecheckingAnalysis = Analysis{..} where alloc = pure bind _ _ = pure () @@ -152,108 +132,65 @@ typecheckingAnalysis = Analysis{..} arg <- meta assign addr arg ty <- eval body - pure (MArr arg ty) + pure (Term (Arr arg ty)) apply _ f a = do _A <- meta _B <- meta - unify (MArr _A _B) f + unify (Term (Arr _A _B)) f unify _A a pure _B - unit = pure MUnit - bool _ = pure MBool - asBool b = unify MBool b >> pure True <|> pure False - string _ = pure MString - asString s = unify MString s $> mempty + unit = pure (Term Unit) + bool _ = pure (Term Bool) + asBool b = unify (Term Bool) b >> pure True <|> pure False + string _ = pure (Term String) + asString s = unify (Term String) s $> mempty frame = fail "unimplemented" edge _ _ = pure () _ ... m = m -data Constraint = Monotype Meta :===: Monotype Meta +data Constraint = Term Monotype Meta :===: Term Monotype Meta deriving (Eq, Ord, Show) infix 4 :===: data Solution - = Int := Monotype Meta + = Int := Term Monotype Meta deriving (Eq, Ord, Show) infix 5 := -meta :: (Carrier sig m, Member Fresh sig) => m (Monotype Meta) -meta = MMeta <$> Fresh.fresh +meta :: (Carrier sig m, Member Fresh sig) => m (Term Monotype Meta) +meta = pure <$> Fresh.fresh -unify :: (Carrier sig m, Member (State (Set.Set Constraint)) sig) => Monotype Meta -> Monotype Meta -> m () +unify :: (Carrier sig m, Member (State (Set.Set Constraint)) sig) => Term Monotype Meta -> Term Monotype Meta -> m () unify t1 t2 | t1 == t2 = pure () | otherwise = modify (<> Set.singleton (t1 :===: t2)) -type Substitution = IntMap.IntMap (Monotype Meta) +type Substitution = IntMap.IntMap (Term Monotype Meta) solve :: (Carrier sig m, Member (State Substitution) sig, MonadFail m) => Set.Set Constraint -> m () solve cs = for_ cs solve where solve = \case -- FIXME: how do we enforce proper subtyping? row polymorphism or something? - MRecord f1 :===: MRecord f2 -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> () - MArr a1 b1 :===: MArr a2 b2 -> solve (a1 :===: a2) *> solve (b1 :===: b2) - MMeta m1 :===: MMeta m2 | m1 == m2 -> pure () - MMeta m1 :===: t2 -> do + Term (Record f1) :===: Term (Record f2) -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> () + Term (Arr a1 b1) :===: Term (Arr a2 b2) -> solve (a1 :===: a2) *> solve (b1 :===: b2) + Var m1 :===: Var m2 | m1 == m2 -> pure () + Var m1 :===: t2 -> do sol <- solution m1 case sol of Just (_ := t1) -> solve (t1 :===: t2) Nothing | m1 `IntSet.member` mvs t2 -> fail ("Occurs check failure: " <> show m1 <> " :===: " <> show t2) - | otherwise -> modify (IntMap.insert m1 t2 . subst (m1 := t2)) - t1 :===: MMeta m2 -> solve (MMeta m2 :===: t1) + | otherwise -> modify (IntMap.insert m1 t2 . fmap (substAll (IntMap.singleton m1 t2))) + t1 :===: Var m2 -> solve (Var m2 :===: t1) t1 :===: t2 -> unless (t1 == t2) $ fail ("Type mismatch:\nexpected: " <> show t1 <> "\n actual: " <> show t2) solution m = fmap (m :=) <$> gets (IntMap.lookup m) -substAll :: Substitutable t => Substitution -> t -> t -substAll s a = foldl' (flip subst) a (map (uncurry (:=)) (IntMap.toList s)) +mvs :: Foldable t => t Meta -> IntSet.IntSet +mvs = foldMap IntSet.singleton -class FreeVariables t where - mvs :: t -> IntSet.IntSet - -instance FreeVariables (Monotype Meta) where - mvs MUnit = mempty - mvs MBool = mempty - mvs MString = mempty - mvs (MArr a b) = mvs a <> mvs b - mvs (MMeta m) = IntSet.singleton m - mvs (MFree _) = mempty - mvs (MRecord fs) = foldMap mvs fs - -instance FreeVariables Constraint where - mvs (t1 :===: t2) = mvs t1 <> mvs t2 - -class Substitutable t where - subst :: Solution -> t -> t - -instance Substitutable (Monotype Meta) where - subst s con = case con of - MUnit -> MUnit - MBool -> MBool - MString -> MString - MArr a b -> MArr (subst s a) (subst s b) - MMeta m' - | m := t <- s - , m == m' -> t - | otherwise -> MMeta m' - MFree n -> MFree n - MRecord fs -> MRecord (subst s <$> fs) - -instance Substitutable Constraint where - subst s (t1 :===: t2) = subst s t1 :===: subst s t2 - -instance Substitutable Solution where - subst s (m := t) = m := subst s t - -instance Substitutable a => Substitutable (IntMap.IntMap a) where - subst s = IntMap.map (subst s) - -instance (Ord a, Substitutable a) => Substitutable (Set.Set a) where - subst s = Set.map (subst s) - -instance Substitutable v => Substitutable (Map.Map k v) where - subst s = fmap (subst s) +substAll :: Monad t => IntMap.IntMap (t Meta) -> t Meta -> t Meta +substAll s a = a >>= \ i -> fromMaybe (pure i) (IntMap.lookup i s) diff --git a/semantic-core/src/Data/Core.hs b/semantic-core/src/Data/Core.hs index 1bb9934af..e3a6d8c27 100644 --- a/semantic-core/src/Data/Core.hs +++ b/semantic-core/src/Data/Core.hs @@ -194,25 +194,8 @@ annWith :: (Carrier sig m, Member Core sig) => CallStack -> m a -> m a annWith callStack = maybe id (fmap send . Ann) (stackLoc callStack) -stripAnnotations :: (Member Core sig, Syntax sig) => Term sig a -> Term sig a -stripAnnotations = iter id alg Var Var - where alg t | Just c <- prj t, Ann _ b <- c = b - | otherwise = Term t - - -instance Syntax Core where - foldSyntax go k h = \case - Let a -> Let a - a :>> b -> go h a :>> go h b - Lam u b -> Lam u (foldSyntax go k h b) - a :$ b -> go h a :$ go h b - Unit -> Unit - Bool b -> Bool b - If c t e -> If (go h c) (go h t) (go h e) - String s -> String s - Load t -> Load (go h t) - Edge e t -> Edge e (go h t) - Frame -> Frame - a :. b -> go h a :. go h b - a := b -> go h a := go h b - Ann loc t -> Ann loc (go h t) +stripAnnotations :: (Member Core sig, HFunctor sig, forall g . Functor g => Functor (sig g)) => Term sig a -> Term sig a +stripAnnotations (Var v) = Var v +stripAnnotations (Term t) + | Just c <- prj t, Ann _ b <- c = stripAnnotations b + | otherwise = Term (hmap stripAnnotations t) diff --git a/semantic-core/src/Data/Core/Pretty.hs b/semantic-core/src/Data/Core/Pretty.hs index 70cc97197..57e70c7cb 100644 --- a/semantic-core/src/Data/Core/Pretty.hs +++ b/semantic-core/src/Data/Core/Pretty.hs @@ -11,7 +11,6 @@ module Data.Core.Pretty import Control.Effect.Reader import Data.Core import Data.File -import Data.Functor.Const import Data.Name import Data.Scope import Data.Term @@ -56,57 +55,58 @@ inParens amount go = do body <- with amount go pure (encloseIf (amount >= prec) (symbol "(") (symbol ")") body) -prettify :: (Member (Reader [AnsiDoc]) sig, Member (Reader Prec) sig, Carrier sig m) - => Style - -> Core (Const (m AnsiDoc)) a - -> m AnsiDoc -prettify style = \case - Let a -> pure $ keyword "let" <+> name a - Const a :>> Const b -> do - prec <- ask @Prec - fore <- with 12 a - aft <- with 12 b +prettyCore :: Style -> Term Core User -> AnsiDoc +prettyCore style = run . runReader @Prec 0 . go (pure . name) + where go :: (Member (Reader Prec) sig, Carrier sig m) => (a -> m AnsiDoc) -> Term Core a -> m AnsiDoc + go var = \case + Var v -> var v + Term t -> case t of + Let a -> pure $ keyword "let" <+> name a + a :>> b -> do + prec <- ask @Prec + fore <- with 12 (go var a) + aft <- with 12 (go var b) - let open = symbol ("{" <> softline) - close = symbol (softline <> "}") - separator = ";" <> Pretty.line - body = fore <> separator <> aft + let open = symbol ("{" <> softline) + close = symbol (softline <> "}") + separator = ";" <> Pretty.line + body = fore <> separator <> aft - pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body) + pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body) - Lam n f -> inParens 11 $ do - (x, body) <- bind n f - pure (lambda <> x <+> arrow <+> body) + Lam n f -> inParens 11 $ do + (x, body) <- bind n f + pure (lambda <> x <+> arrow <+> body) - Frame -> pure $ primitive "frame" - Unit -> pure $ primitive "unit" - Bool b -> pure $ primitive (if b then "true" else "false") - String s -> pure . strlit $ Pretty.viaShow s + Frame -> pure $ primitive "frame" + Unit -> pure $ primitive "unit" + Bool b -> pure $ primitive (if b then "true" else "false") + String s -> pure . strlit $ Pretty.viaShow s - Const f :$ Const x -> inParens 11 $ (<+>) <$> f <*> x + f :$ x -> inParens 11 $ (<+>) <$> go var f <*> go var x - If (Const con) (Const tru) (Const fal) -> do - con' <- "if" `appending` con - tru' <- "then" `appending` tru - fal' <- "else" `appending` fal - pure $ Pretty.sep [con', tru', fal'] + If con tru fal -> do + con' <- "if" `appending` go var con + tru' <- "then" `appending` go var tru + fal' <- "else" `appending` go var fal + pure $ Pretty.sep [con', tru', fal'] - Load (Const p) -> "load" `appending` p - Edge Lexical (Const n) -> "lexical" `appending` n - Edge Import (Const n) -> "import" `appending` n - Const item :. Const body -> inParens 4 $ do - f <- item - g <- body - pure (f <> symbol "." <> g) + Load p -> "load" `appending` go var p + Edge Lexical n -> "lexical" `appending` go var n + Edge Import n -> "import" `appending` go var n + item :. body -> inParens 4 $ do + f <- go var item + g <- go var body + pure (f <> symbol "." <> g) - Const lhs := Const rhs -> inParens 3 $ do - f <- lhs - g <- rhs - pure (f <+> symbol "=" <+> g) + lhs := rhs -> inParens 3 $ do + f <- go var lhs + g <- go var rhs + pure (f <+> symbol "=" <+> g) - -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly. - Ann _ (Const c) -> c - where bind (Ignored x) f = let x' = name x in (,) x' <$> local (x':) (getConst (unScope f)) + -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly. + Ann _ c -> go var c + where bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope f) lambda = case style of Unicode -> symbol "λ" Ascii -> symbol "\\" @@ -117,8 +117,3 @@ prettify style = \case appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc appending k item = (keyword k <+>) <$> item - -prettyCore :: Style -> Term Core User -> AnsiDoc -prettyCore s = run . runReader @Prec 0 . runReader @[AnsiDoc] [] . cata id (prettify s) bound (pure . name) - where bound (Z _) = asks (head @AnsiDoc) - bound (S n) = local (tail @AnsiDoc) n diff --git a/semantic-core/src/Data/Scope.hs b/semantic-core/src/Data/Scope.hs index f7abe219a..3f591a2d2 100644 --- a/semantic-core/src/Data/Scope.hs +++ b/semantic-core/src/Data/Scope.hs @@ -2,6 +2,7 @@ module Data.Scope ( Incr(..) , incr +, closed , Scope(..) , fromScope , toScope @@ -44,6 +45,10 @@ incr :: (a -> c) -> (b -> c) -> Incr a b -> c incr z s = \case { Z a -> z a ; S b -> s b } +closed :: Traversable f => f a -> Maybe (f b) +closed = traverse (const Nothing) + + newtype Scope a f b = Scope { unScope :: f (Incr a (f b)) } deriving (Foldable, Functor, Traversable) diff --git a/semantic-core/src/Data/Term.hs b/semantic-core/src/Data/Term.hs index 0557116a1..54bc6bf70 100644 --- a/semantic-core/src/Data/Term.hs +++ b/semantic-core/src/Data/Term.hs @@ -1,18 +1,12 @@ -{-# LANGUAGE DeriveTraversable, FlexibleInstances, LambdaCase, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, ScopedTypeVariables, StandaloneDeriving, TypeOperators, UndecidableInstances #-} +{-# LANGUAGE DeriveTraversable, FlexibleInstances, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, StandaloneDeriving, UndecidableInstances #-} module Data.Term ( Term(..) -, Syntax(..) -, iter -, cata -, interpret +, hoistTerm ) where import Control.Effect.Carrier import Control.Monad (ap) import Control.Monad.Module -import Data.Coerce (coerce) -import Data.Functor.Const -import Data.Scope data Term sig a = Var a @@ -50,44 +44,7 @@ instance RightModule sig => Carrier sig (Term sig) where eff = Term -class (HFunctor sig, forall g . Functor g => Functor (sig g)) => Syntax sig where - foldSyntax :: (forall x y . (x -> m y) -> f x -> n y) - -> (forall a . Incr () (n a) -> m (Incr () (n a))) - -> (a -> m b) - -> sig f a - -> sig n b - -instance Syntax (Scope ()) where - foldSyntax go bound free = Scope . go (bound . fmap (go free)) . unScope - -instance (Syntax l, Syntax r) => Syntax (l :+: r) where - foldSyntax go bound free (L l) = L (foldSyntax go bound free l) - foldSyntax go bound free (R r) = R (foldSyntax go bound free r) - - -iter :: forall m n sig a b - . Syntax sig - => (forall a . m a -> n a) - -> (forall a . sig n a -> n a) - -> (forall a . Incr () (n a) -> m (Incr () (n a))) - -> (a -> m b) - -> Term sig a - -> n b -iter var alg bound = go - where go :: forall x y . (x -> m y) -> Term sig x -> n y - go free = \case - Var a -> var (free a) - Term t -> alg (foldSyntax go bound free t) - -cata :: Syntax sig - => (a -> b) - -> (forall a . sig (Const b) a -> b) - -> (Incr () b -> a) - -> (x -> a) - -> Term sig x - -> b -cata var alg k h = getConst . iter (coerce var) (Const . alg) (coerce k) (Const . h) - - -interpret :: (Carrier sig m, Member eff sig, Syntax eff) => (forall a . Incr () (m a) -> m (Incr () (m a))) -> (a -> m b) -> Term eff a -> m b -interpret = iter id send +hoistTerm :: (HFunctor sig, forall g . Functor g => Functor (sig g)) => (forall m x . sig m x -> sig' m x) -> Term sig a -> Term sig' a +hoistTerm f = go + where go (Var v) = Var v + go (Term t) = Term (f (hmap (hoistTerm f) t))