Holes in GHC
Simon PeytonJones
simonpj at microsoft.com
Thu Jan 26 17:10:29 CET 2012
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: glasgowhaskellusersbounces at haskell.org [mailto:glasgowhaskellusers
 bounces at haskell.org] On Behalf Of Simon PeytonJones
 Sent: 26 January 2012 14:25
 To: Thijs Alkemade; glasgowhaskellusers 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: glasgowhaskellusersbounces at haskell.org [mailto:glasgowhaskell
 users
  bounces at haskell.org] On Behalf Of Thijs Alkemade
  Sent: 25 January 2012 15:21
  To: glasgowhaskellusers 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:23, ())]
  [__, ()] :: [()]
 
  *Main> :t map __ __
  tcRnExpr2: [(<interactive>:1:56, a0 > b), (<interactive>:1:89, [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:910, GHC.Prim.Any * > b),
  (f.hs:1:1213, [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/glasgowhaskellusers/2012
  January/021453.html
  [2] https://github.com/xnyhps/ghc/commits/master
 
  _______________________________________________
  Glasgowhaskellusers mailing list
  Glasgowhaskellusers at haskell.org
  http://www.haskell.org/mailman/listinfo/glasgowhaskellusers



 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
More information about the Glasgowhaskellusers
mailing list