headers
Philip K. F. Hölzenspies | 24 Jun 2012 11:49
Picon
Favicon

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.)
(Continue reading)

Permalink | Reply |
headers
Philip K. F. Hölzenspies | 24 Jun 2012 21:55
Picon
Favicon

Re: API function to check whether one type fits "in" another

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)
(Continue reading)

Permalink | Reply |
headers
Simon Peyton-Jones | 28 Jun 2012 09:07
Picon
Favicon
Gravatar

RE: API function to check whether one type fits "in" another

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.
(Continue reading)

Permalink | Reply |
headers
Philip K. F. Hölzenspies | 28 Jun 2012 12:11
Picon
Favicon

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?
(Continue reading)

Permalink | Reply |
headers
Simon Peyton-Jones | 29 Jun 2012 18:00
Picon
Favicon
Gravatar

RE: API function to check whether one type fits "in" another

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 <at> st-andrews.ac.uk]
|  Sent: 28 June 2012 11:11
|  To: Simon Peyton-Jones
|  Cc: thijsalkemade <at> gmail.com; glasgow-haskell-users <at> 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
(Continue reading)

Permalink | Reply |
headers
Philip Holzenspies | 19 Jul 2012 19:28
Picon
Favicon

Re: API function to check whether one type fits "in" another

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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Permalink | Reply |
headers
Thijs Alkemade | 23 Jul 2012 17:15
Picon
Gravatar

Re: API function to check whether one type fits "in" another


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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Permalink | Reply |

Gmane