Holes in GHC

[Simon Peyton-Jones]

A thought.  Based on my limited understanding of your goals, suppose instead of (say)

	f (__, True) __

you transformed to

	\xy -> f (x,True) y

That is, replace each hole with a variable.  Now do type inference.  You'll get a type like

	Int -> Bool -> ...

and that tells you the type of the two holes.  Or you might get a type like

	forall a.  a -> [a] -> ....

and that too tells you a lot about the types of the holes.  Or you might get a type like

	forall a. Ord a => a -> [a] -> ...

To me it looks like you get exactly the info that (I think) you want, and moreover you can do that without changing the type inference engine at all.

Simon
	

|  -----Original Message-----
|  From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
|  bounces at haskell.org] On Behalf Of Simon Peyton-Jones
|  Sent: 26 January 2012 14:25
|  To: Thijs Alkemade; glasgow-haskell-users at haskell.org
|  Subject: RE: Holes in GHC
|  
|  Thijs
|  
|  You are describing the implementation of something, but you do not give a
|  specification.  It's hard for me to help you with the design of something when I
|  don't know what the goal is.
|  
|  Can you give a series of concrete examples of what you want to happen?  Is this
|  just in GHCi?  Or do you expect the batch compiler to behave specially?
|  
|  Don't worry about the implementation: just say what you would LIKE to achieve.
|  
|  Simon
|  
|  |  -----Original Message-----
|  |  From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-
|  users-
|  |  bounces at haskell.org] On Behalf Of Thijs Alkemade
|  |  Sent: 25 January 2012 15:21
|  |  To: glasgow-haskell-users at haskell.org
|  |  Subject: Holes in GHC
|  |
|  |  Hello!
|  |
|  |  As mentioned in our previous mail [1], we've been working on
|  |  introducing Agda's holes into GHC [2]. Our general approach is as
|  |  follows: we've added a hole to the syntax, denoted here by two
|  |  underscores: "__". We've introduced a new HsExpr for this, which
|  |  stores the hole's source span (as this is the only thing that a user
|  |  needs to identify the hole).
|  |
|  |  Then, we extended the local environment of the typechecker to include
|  |  a mutable Map, mapping a SrcSpan to a Type and a WantedConstraints (we
|  |  need these later to produce the correct class constraints on the
|  |  type). In TcExpr.lhs, whenever the tcExpr function encounters a hole,
|  |  it adds the source position with the res_ty and the current tcl_lie to
|  |  the map.
|  |
|  |  After type checking has finished, these types can be taken out of the
|  |  map and shown to the user, however, we are not sure yet where to do
|  |  this. Currently the map is read in tcRnModule and tcRnExpr, so loading
|  |  modules and evaluating expressions with ":t" will show the types of
|  |  the holes in that module or expression. There, we call mkPiTypes,
|  |  mkForAllTys (with the quantified type variables we obtained from the
|  |  WantedConstraints), we zonk and tidy them all (most of this imitates
|  |  how tcRnExpr modifies a type before returning it, except the tidying,
|  |  which needs to pass the updated TidyEnv to the tidying of the next
|  |  hole).
|  |
|  |  Examples:
|  |
|  |  *Main> :t [__, ()]
|  |  tcRnExpr2: [(<interactive>:1:2-3, ())]
|  |  [__, ()] :: [()]
|  |
|  |  *Main> :t map __ __
|  |  tcRnExpr2: [(<interactive>:1:5-6, a0 -> b), (<interactive>:1:8-9, [a0])]
|  |  map __ __ :: [b]
|  |
|  |  Any feedback on this design would be appreciated. We would like to
|  |  know if this is something that could be considered to be added to GHC,
|  |  and what your requirements for that are.
|  |
|  |
|  |
|  |  Also, we have a confusing problem when type checking a module. Above,
|  |  we showed the result of ":t map __ __" in ghci. However, if we put "f
|  |  = map __ __" in a module, we get:
|  |
|  |  tcRnModule: [(f.hs:1:9-10, GHC.Prim.Any * -> b),
|  |  (f.hs:1:12-13, [GHC.Prim.Any *])]
|  |
|  |  If I read GHC.Prim.Any * as forall a. a, then this is not correct: the
|  |  GHC.Prim.Any * in both holes should have the same type. We assume it
|  |  shows up because the type that should be there does not occur in the
|  |  type signature of f (as it's just [b]), but so far we've been unable
|  |  to figure out why this behavior is different in interactive mode. Does
|  |  someone have an idea about what to do to avoid the introduction of
|  |  these GHC.Prim.Any * types?
|  |
|  |  Best regards,
|  |  Thijs Alkemade
|  |
|  |  [1] http://www.haskell.org/pipermail/glasgow-haskell-users/2012-
|  |  January/021453.html
|  |  [2] https://github.com/xnyhps/ghc/commits/master
|  |
|  |  _______________________________________________
|  |  Glasgow-haskell-users mailing list
|  |  Glasgow-haskell-users at haskell.org
|  |  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
|  
|  
|  
|  _______________________________________________
|  Glasgow-haskell-users mailing list
|  Glasgow-haskell-users at haskell.org
|  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users