Types as syntax #201
Types as syntax #201
Conversation
robrix
left a comment
robrix
left a comment
There was a problem hiding this comment.
Ready for review (modulo dependencies).
| | MArr (Monotype a) (Monotype a) | ||
| | MRecord (Map.Map User (Monotype a)) | ||
| deriving (Eq, Functor, Ord, Show) | ||
| data Monotype f a |
There was a problem hiding this comment.
By abstracting Monotype and Polytype over their subterms and embedding them in Term, we’re able to (easily!) share the common constructors: everything but ForAll.
| -> (Int -> Int -> Polytype) | ||
| -> Polytype | ||
| -> Polytype | ||
| substIn free bound = go 0 |
There was a problem hiding this comment.
I love that all of this machinery just evaporates because we’re using Scope instead.
| 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))) |
There was a problem hiding this comment.
This fromJust is safe because we just bound all of the free variables.
| 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) |
There was a problem hiding this comment.
Both of those classes and all of those instances can be replaced with these two simple functions!
| incr z s = \case { Z a -> z a ; S b -> s b } | ||
|
|
||
|
|
||
| closed :: Traversable f => f a -> Maybe (f b) |
There was a problem hiding this comment.
Note from the type that b is completely unconstrained by the inputs—the only way for this to produce a Just is therefore if there are no free variables at all.
| generalize ty = fromJust (closed (forAlls (IntSet.toList (mvs ty)) (hoistTerm R ty))) | ||
|
|
||
|
|
||
| typecheckingFlowInsensitive :: [File (Term Core.Core Name)] -> (Heap Name (Term Monotype Meta), [File (Either (Loc, String) (Term (Polytype :+: Monotype) Void))]) |
There was a problem hiding this comment.
The types here are super interesting. Typechecking returns a polytype…
| . runNaming | ||
| . runHeap (Gen (Gensym (Nil :> "root") 0)) | ||
| . (>>= traverse (traverse (traverse generalize))) | ||
| . fmap (fmap (fmap (fmap generalize))) |
There was a problem hiding this comment.
…which is the result of generalizing (quantifying over all of the variables in)…
| ) | ||
| => File (Term Core.Core Name) | ||
| -> m (File (Either (Loc, String) (Monotype Meta))) | ||
| -> m (File (Either (Loc, String) (Term Monotype Meta))) |
There was a problem hiding this comment.
…the monotype produced by runFile. Classic Hindley-Milner type schemery!
This PR reframes
MonotypeandPolytypeas scope-safe syntax inTerm.