Merge pull request #201 from github/types-as-syntax

Types as syntax

Author: robrix

semantic-core/src/Analysis/Typecheck.hs

@@ -1,130 +1,110 @@
-{-# 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
 
 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
 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 Scope = Scope Polytype
-  deriving (Eq, Ord, Show)
+newtype Polytype f a = PForAll (Scope () f a)
+  deriving (Foldable, Functor, Generic1, Traversable)
 
-forAll :: Gensym -> Polytype -> Polytype
-forAll n body = PForAll (Analysis.Typecheck.bind n body)
+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)
 
-forAlls :: Foldable t => t Gensym -> Polytype -> Polytype
-forAlls ns body = foldr forAll body ns
+instance HFunctor Polytype
+instance RightModule Polytype where
+  PForAll b >>=* f = PForAll (b >>=* f)
 
-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)
+forAll :: (Eq a, Carrier sig m, Member Polytype sig) => a -> m a -> m a
+forAll n body = send (PForAll (Data.Scope.bind1 n body))
 
--- | 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
+forAlls :: (Eq a, Carrier sig m, Member Polytype sig, Foldable t) => t a -> m a -> m a
+forAlls ns body = foldr forAll body ns
 
-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))
-
-
-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)
+mvs :: Foldable t => t Meta -> IntSet.IntSet
+mvs = foldMap IntSet.singleton
 
-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)

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)
 

semantic-core/src/Data/Term.hs

@@ -1,6 +1,7 @@
-{-# LANGUAGE DeriveTraversable, FlexibleInstances, MultiParamTypeClasses, QuantifiedConstraints, StandaloneDeriving, UndecidableInstances #-}
+{-# LANGUAGE DeriveTraversable, FlexibleInstances, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, StandaloneDeriving, UndecidableInstances #-}
 module Data.Term
 ( Term(..)
+, hoistTerm
 ) where
 
 import Control.Effect.Carrier
@@ -41,3 +42,9 @@ instance RightModule sig => Monad (Term sig) where
 
 instance RightModule sig => Carrier sig (Term sig) where
   eff = Term
+
+
+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))