API function to check whether one type fits "in" another
L.S., I sent this to the cvs-ghc list, but was - correctly - redirected here. We're trying to write an alternative interactive front-end (alternative to ghci). This front-end is very type-driven; terms are composed not as characters on a prompt, but as applications of terms to terms. At every application of a term to another, we want to check whether the application is well typed and what type variables would have to change. Suppose I want to build the term flip fmap (+) :: Num n => ((n -> n) -> b) -> n -> b In our front-end, however, we do not need the flip; we leave unfilled holes with their type annotated, so the above would really look like this (where [[ and ]] denote a hole): fmap [[ (n -> n) -> b ]] (+) :: Num n => n -> b We start this off by asking for the types of these separate things, using GHC.exprType, giving: fmap: ForAllTy f (ForAllTy a (ForAllTy b (FunTy (TyConApp GHC.Base.Functor [TyVarTy f]) (FunTy (FunTy (TyVarTy a) (TyVarTy b)) (FunTy (AppTy (TyVarTy f) (TyVarTy a)) (AppTy (TyVarTy f) (TyVarTy b))))))) (+): ForAllTy a (FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (FunTy (TyVarTy a) (FunTy (TyVarTy a) (TyVarTy a)))) (Note that 'Var' things are pretty printed to just show their name, whereas all the constructors of Type are displayed using show.) The thing that we really want to ask the GHC-API is whether (+) 'fits into' the second argument-hole of fmap, i.e. we want to know whether (type of +) ForAllTy a (FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (FunTy (TyVarTy a) (FunTy (TyVarTy a) (TyVarTy a)))) fits into (type of second argument of fmap) ForAllTy f (ForAllTy a (FunTy (TyConApp GHC.Base.Functor [TyVarTy f]) (AppTy (TyVarTy f) (TyVarTy a)))) What I'm looking for is a function fitsInto :: TermType -> HoleType -> Maybe [(TyVar,Type)] I have found many functions in TcUnify / Unify / TcMatches that look somewhat like this, but in all cases they required extra arguments. When these extra arguments are filled with arbitrary values, the result is always Nothing or some sort of panic. Any pointers would be truly welcome. Regards, Philip
L.S., I've come up with some minor progress myself, but I could still do with a little help. The attached file is the smallest thing I could come up with to replicate my problem. I'm using tcMatchTy now to try and match two types, hoping to find TyVar substitutions when the types unify. Given the functions in the attached file and the ghci-session below this message (from the current Haskell Platform), could anyone explain the misses (the ones that result in Nothing)?? Regards, Philip P.S. Note that type variables are pretty printed to simply 'a' or 'b'. The names are disambiguated only locally, so in the trace below, not every 'a' is equal to every other 'a' (but this becomes obvious from the corresponding InScopeSet) Ghci session: *CheckType> matchHole "fmap" 0 "id" Hole: FunTy (TyVarTy a) (TyVarTy b) Term: FunTy (TyVarTy a) (TyVarTy a) Vars: [a,b,a] Just (TvSubst InScopeSet [(a15M9,a),(a15Ma,b),(a15Mg,a)] [(a15M9,TyVarTy a),(a15Ma,TyVarTy a)]) *CheckType> matchHole "fmap" 0 "(+)" Hole: FunTy (TyVarTy a) (TyVarTy b) Term: FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (FunTy (TyVarTy a) (FunTy (TyVarTy a) (TyVarTy a))) Vars: [a,b,a] Nothing *CheckType> matchHole "(+)" 0 "0" Hole: FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (TyVarTy a) Term: FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (TyVarTy a) Vars: [a,a] Just (TvSubst InScopeSet [(a168l,a),(a168s,a)] [(a168l,TyVarTy a)]) *CheckType> matchHole "fmap" 1 "[True]" Hole: FunTy (TyConApp GHC.Base.Functor [TyVarTy f]) (AppTy (TyVarTy f) (TyVarTy a)) Term: TyConApp [] [TyConApp GHC.Types.Bool []] Vars: [f,a] Nothing *CheckType> matchHole "map" 1 "[True]" Hole: TyConApp [] [TyVarTy a] Term: TyConApp [] [TyConApp GHC.Types.Bool []] Vars: [a] Just (TvSubst InScopeSet [(adpV,a)] [(adpV,TyConApp GHC.Types.Bool [])]) *CheckType>
Philip | What I'm looking for is a function | | fitsInto :: TermType -> HoleType -> Maybe [(TyVar,Type)] Happily there is such a function, but you will need to become quite familiar with GHC's type inference engine. We need to tighten up the specification first. I believe that you have function and argument, whose *most general types* are fun :: forall a b c. fun_ty arg :: forall p q. arg_ty You want to ask whether 'arg' could possibly be 'fun's second (say) argument. To answer this you must first instantiate 'fun' correctly. For example, suppose fun :: forall a. [a] -> Int arg :: [Bool] Then we can indeed pass 'arg' to 'fun' but only if we instantiate 'fun' at Bool, thus: fun Bool :: [Bool] -> Int Now indeed the first argument of (fun Bool) has precisely type [Bool] and we are done. This business of instantiating a polymorphic function with a type, using a type application (f Bool) is a fundamental part of how GHC works (and indeed type inference in general). If you aren't familiar with it, maybe try reading a couple of papers about GHC's intermediate language, System F or FC. To play this game we have to correctly "guess" the type at which to instantiate 'fun'. This is what type inference does: we instantiate 'fun' with a unification variable 'alpha' meaning "I'm not sure" and then accumulate equality constraints that tell us what type 'alpha' stands for. The other complication is that 'arg' might also need instantiation to fit, but I'll ignore that for now. It'll only show up in more complicated programs. So you want a function something like this: fits :: Type -- The type of the function -> Int -- Which argument position we are testing -> Type -- The argument -> TcM Bool -- Whether it fits fits fun_ty arg_no arg_ty = do { inst_fun_ty <- deeplyInstantiate fun_ty ; llet (fun_arg_tys, fun_res_ty) = splitFunTys inst_fun_ty the_arg_ty = fun_arg_tys !! arg_no ; unifyType the_arg_ty arg_ty } The first step instantiates the function type (deeplyInstantiate is in Inst.lhs) with fresh unification variables. The second extracts the appropriate argument. Then we unify the argument type the function expects with that of the supplied argument. Even then you aren't done. Unification collects constraints, and we need to check they are solutle. So we'll really need something like do { constraints <- captureConstriaints (fits fun_ty arg_no arg_ty) ; tcSimplifyTop constraints } And the final thing you need to do is intiate the type checker monad with initTc, and check whether any errors occurred. It occurs to me that a simpler way to do this might be to piggy back on the work of Thijs Alkemade [thijsalkemade@gmail.com] at Chalmers on "holes". He's going to make it possible to make an expression fun _ arg where the underscore means "hole". Then you can give this entire expression to the type checker and have it figure out whether it is typeable, and if so what the type the "_" is. This would mean you didn't need to do any of the above stuff (and I have simplified considerably in writing the above). Maybe look at the ticket http://hackage.haskell.org/trac/ghc/ticket/5910 and wiki page http://hackage.haskell.org/trac/ghc/wiki/Holes Simon
Dear Simon, et al, Thank you very much for your reply. Some of the pointers you gave, I wouldn't have come across, for not knowing to have to browse through the module Inst, for example. I read the OutsideIn paper (JFP), but that's a fair while back. I was pointed to Thijs's work in progress at an Agda talk recently. The front-end we're working on should be portable to any lambda-language with strong types, so the availability of holes in Agda and Idris makes the implementation for those back-ends a breeze. There is one limiting consideration, however: We want to get this up and running the next few weeks and we would like to keep things in-sync with the developments on the different back-ends. This is why I'm trying to stay as close as possible to the more "public" API parts (the things that are documented and haven't changed significantly since at least 7.0.4). In this light, I was wondering whether it's not worth having a function that does all this plumbing in the API that is persistent through future versions, much like pure interface to the parser (GHC.parser). Preferably it would look something like: typeCheck :: DynFlags -- the flags -> FilePath -- for source locations -> Type -- expected -> Type -- actual -> Either SomeSortOfErrorStructure SomeSubstitutionAndOrConstraintTable The implementation would have to make sure the pre-conditions of the type arguments are met. Is this worth pursuing? Would be a significant amount of work? Am I being pushy if I make this a feature-request? Regards, Philip PS. I'm going to study the Trac you pointed to in more detail; browsing it was already a learning experience about the whats and wheres of the GHC API.
Philip If you develop a function that does what you want, and want to make it part of the GHC API, we'd definitely consider including it. But I don't want to promise to develop something just for you; I'm just too snowed under with other stuff. I really think the "holes" that Thijs is working on might be good for you. He has a prototype already I think. Simon | -----Original Message----- | From: "Philip K. F. Hölzenspies" [mailto:pkfh@st-andrews.ac.uk] | Sent: 28 June 2012 11:11 | To: Simon Peyton-Jones | Cc: thijsalkemade@gmail.com; glasgow-haskell-users@haskell.org | Subject: Re: API function to check whether one type fits "in" another | | Dear Simon, et al, | | Thank you very much for your reply. Some of the pointers you gave, I wouldn't | have come across, for not knowing to have to browse through the module Inst, for | example. | | I read the OutsideIn paper (JFP), but that's a fair while back. I was pointed to | Thijs's work in progress at an Agda talk recently. The front-end we're working on | should be portable to any lambda-language with strong types, so the availability | of holes in Agda and Idris makes the implementation for those back-ends a | breeze. | | There is one limiting consideration, however: We want to get this up and running | the next few weeks and we would like to keep things in-sync with the | developments on the different back-ends. This is why I'm trying to stay as close | as possible to the more "public" API parts (the things that are documented and | haven't changed significantly since at least 7.0.4). | | In this light, I was wondering whether it's not worth having a function that does | all this plumbing in the API that is persistent through future versions, much like | pure interface to the parser (GHC.parser). Preferably it would look something like: | | typeCheck | :: DynFlags -- the flags | -> FilePath -- for source locations | -> Type -- expected | -> Type -- actual | -> Either | SomeSortOfErrorStructure | SomeSubstitutionAndOrConstraintTable | | The implementation would have to make sure the pre-conditions of the type | arguments are met. Is this worth pursuing? Would be a significant amount of | work? Am I being pushy if I make this a feature-request? | | Regards, | Philip | | PS. I'm going to study the Trac you pointed to in more detail; browsing it was | already a learning experience about the whats and wheres of the GHC API.
Dear Simon, et al, I finally got back around to working on this idea. I'm not yet quite sure whether I've now understood it all. I have reread the latest edition of "System F with Type Equality Coercions" (Jan 2011 version), so I understand that inference is now just percolating coercions upwards, as it were, and then solving the set of wanted constraints. If the set is consistent, the program type-checks. This is at the core of what I have now: typeCheck :: GhcMonad m => Type -> Type -> m (Messages, Maybe (TcCoercion, Bag EvBind)) typeCheck expectedTy actualTy = do let mod = mkModule mainPackageId $ mkModuleName "<NoModule>" env <- getSession liftIO $ initTc env HsSrcFile False mod $ do (coerce,wanted) <- captureConstraints $ do (expectedWrap, expectedRho) <- deeplyInstantiate DefaultOrigin expectedTy (actualWrap, actualRho ) <- deeplyInstantiate DefaultOrigin actualTy unifyType actualRho expectedRho binds <- simplifyTop wanted return (coerce,binds) It appears both the "hole" (expectedTy) and the thing to go into the hole (actualTy) need to be deeply instantiated, otherwise, this function rejects putting (exprType "1") into the first argument position of (exprType "(+)"), because it either can't match 'a' to 'Num b => b', or (if we take the rho-type), it misses 'Num b'. Anyway, deeply instantiating both seems to solve such problems and, in the cases I've tried, type checks the things I would expect and rejects the things I would expect. There are two missing bits, still: Firstly, when leaving variables ambiguous (i.e. filling a "Monad m => a -> m a" shaped hole with "return", leaving 'm' ambiguous), simplifyTop fails. Is it possible to allow for ambiguous variables, in roughly the same way that (exprType "mapM return") works just fine? I've looked at some other simplification functions (TcSimplify.*), but the lack of documentation makes my guesswork somewhat random. Secondly, is there a way in the API to find all the appropriate substitutions for the variables in the *original* types (i.e. loosing the fresh variables introduced by deeplyInstantiate)? Ultimately, I would really like to end up with a TvSubst, or any other mapping from TyVar to Type. Ideas? Regards, Philip
On 19 jul. 2012, at 19:28, Philip Holzenspies wrote:
Dear Simon, et al,
I finally got back around to working on this idea. I'm not yet quite sure whether I've now understood it all. I have reread the latest edition of "System F with Type Equality Coercions" (Jan 2011 version), so I understand that inference is now just percolating coercions upwards, as it were, and then solving the set of wanted constraints. If the set is consistent, the program type-checks. This is at the core of what I have now:
typeCheck :: GhcMonad m => Type -> Type -> m (Messages, Maybe (TcCoercion, Bag EvBind)) typeCheck expectedTy actualTy = do let mod = mkModule mainPackageId $ mkModuleName "<NoModule>" env <- getSession liftIO $ initTc env HsSrcFile False mod $ do (coerce,wanted) <- captureConstraints $ do (expectedWrap, expectedRho) <- deeplyInstantiate DefaultOrigin expectedTy (actualWrap, actualRho ) <- deeplyInstantiate DefaultOrigin actualTy unifyType actualRho expectedRho binds <- simplifyTop wanted return (coerce,binds)
It appears both the "hole" (expectedTy) and the thing to go into the hole (actualTy) need to be deeply instantiated, otherwise, this function rejects putting (exprType "1") into the first argument position of (exprType "(+)"), because it either can't match 'a' to 'Num b => b', or (if we take the rho-type), it misses 'Num b'. Anyway, deeply instantiating both seems to solve such problems and, in the cases I've tried, type checks the things I would expect and rejects the things I would expect.
There are two missing bits, still:
Firstly, when leaving variables ambiguous (i.e. filling a "Monad m => a -> m a" shaped hole with "return", leaving 'm' ambiguous), simplifyTop fails. Is it possible to allow for ambiguous variables, in roughly the same way that (exprType "mapM return") works just fine? I've looked at some other simplification functions (TcSimplify.*), but the lack of documentation makes my guesswork somewhat random.
Secondly, is there a way in the API to find all the appropriate substitutions for the variables in the *original* types (i.e. loosing the fresh variables introduced by deeplyInstantiate)? Ultimately, I would really like to end up with a TvSubst, or any other mapping from TyVar to Type.
Ideas?
Regards, Philip
Hi Philip, As Simon has said, I have been working on implementing Agda-like holes in GHC. This is somewhat similar to what you've been working on, but so far I've only been concerned into reporting these holes to the user, and not trying to figure out what could fit into it. Also, I was adding it to GHC directly, not using the GHC API, so our approaches are quite different. But I'm hoping my experience might help you a little. Could you show how simplifyTop fails, or show a bit more of you code? I wasn't able to get just this piece running as you described. If it is an ambiguity error as you say, it could just be the monomorphism restriction incorrectly assuming your types belong to top level declarations and rejecting them. Regards, Thijs Alkemade
participants (4)
-
"Philip K. F. Hölzenspies" -
Philip Holzenspies
-
Simon Peyton-Jones -
Thijs Alkemade