1- {-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, QuantifiedConstraints, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications #-}
1+ {-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, QuantifiedConstraints, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators #-}
22module Analysis.Typecheck
33( Monotype (.. )
44, Meta
5- , Polytype (PForAll , PBool , PArr )
6- , Scope
5+ , Polytype (.. )
76, typecheckingFlowInsensitive
87, typecheckingAnalysis
98) where
@@ -59,13 +58,7 @@ instance RightModule Monotype where
5958
6059type Meta = Int
6160
62- data Polytype f a
63- = PForAll (Scope () f a )
64- | PUnit
65- | PBool
66- | PString
67- | PArr (f a ) (f a )
68- | PRecord (Map. Map User (f a ))
61+ newtype Polytype f a = PForAll (Scope () f a )
6962 deriving (Foldable , Functor , Generic1 , Traversable )
7063
7164deriving instance (Eq a , forall a . Eq a => Eq (f a ), Monad f ) => Eq (Polytype f a )
@@ -76,11 +69,6 @@ deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Po
7669instance HFunctor Polytype
7770instance RightModule Polytype where
7871 PForAll b >>=* f = PForAll (b >>=* f)
79- PUnit >>=* _ = PUnit
80- PBool >>=* _ = PBool
81- PString >>=* _ = PString
82- PArr a b >>=* f = PArr (a >>= f) (b >>= f)
83- PRecord m >>=* f = PRecord ((>>= f) <$> m)
8472
8573
8674forAll :: (Eq a , Carrier sig m , Member Polytype sig ) => a -> m a -> m a
@@ -89,21 +77,17 @@ forAll n body = send (PForAll (Data.Scope.bind1 n body))
8977forAlls :: (Eq a , Carrier sig m , Member Polytype sig , Foldable t ) => t a -> m a -> m a
9078forAlls ns body = foldr forAll body ns
9179
92- generalize :: (Carrier sig m , Member Naming sig ) => Term Monotype Meta -> m (Term Polytype Gensym )
80+ generalize :: (Carrier sig m , Member Naming sig ) => Term Monotype Meta -> m (Term ( Polytype :+: Monotype ) Gensym )
9381generalize ty = namespace " generalize" $ do
9482 Gensym root _ <- Name. fresh
95- pure (forAlls (map (Gensym root) (IntSet. toList (mvs ty))) (fold root ty))
96- where fold root = \ case
97- Var v -> pure (Gensym root v)
98- Term t -> Term $ case t of
99- Unit -> PUnit
100- Bool -> PBool
101- String -> PString
102- Arr a b -> PArr (fold root a) (fold root b)
103- Record fs -> PRecord (fold root <$> fs)
104-
105-
106- typecheckingFlowInsensitive :: [File (Term Core. Core Name )] -> (Heap Name (Term Monotype Meta ), [File (Either (Loc , String ) (Term Polytype Gensym ))])
83+ pure (Gensym root <$> forAlls (IntSet. toList (mvs ty)) (fold ty))
84+ where fold :: Term Monotype a -> Term (Polytype :+: Monotype ) a
85+ fold = \ case
86+ Var v -> Var v
87+ Term t -> Term (R (hmap fold t))
88+
89+
90+ typecheckingFlowInsensitive :: [File (Term Core. Core Name )] -> (Heap Name (Term Monotype Meta ), [File (Either (Loc , String ) (Term (Polytype :+: Monotype ) Gensym ))])
10791typecheckingFlowInsensitive
10892 = run
10993 . runFresh
0 commit comments