Holes in GHC
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.
| -----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
| 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.
| | -----Original Message-----
| | From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-
| | 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 , we've been working on
| | introducing Agda's holes into GHC . 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
| |  http://www.haskell.org/pipermail/glasgow-haskell-users/2012-
| | January/021453.html
| |  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
More information about the Glasgow-haskell-users