Re: Holes in GHC
Hi Simon,
On Tue, Aug 21, 2012 at 7:14 PM, Simon Peyton-Jones
simo...@microsoft.com wrote:
Can you give me read/write access to your github repo? I'm simonpj on github.
That way I can add comments/questions in code, and generally clean up.
It would make things easier if you could merge with HEAD so that I don't have
to mess around moving libraries back in time.
Done. I've merged with HEAD as of right now. The only subrepository
I've forked is the testsuite repository, which you can find on
https://github.com/xnyhps/testsuite.
I've tried to get validate to pass all tests, I had to fix this one:
https://github.com/xnyhps/testsuite/commit/5016899250ace0d2db227569073ad83573909728,
and I've added this
https://github.com/xnyhps/testsuite/commit/47f1bb7f7c8aced6e59f8d3e2413f6c6c5b6016e
as a test case for holes. It's not a very complicated example of
holes, but I'm a bit unsure how to properly write a test case for it.
If you have some ideas to do this better, I'd be interested.
Some other tests were reporting to be too (in)efficient, but compared
to running validate on HEAD without my patch it seemed the same thing
happened there, so I haven't look further into those.
--
You've put LANGUAGE Holes in TcErrors which means I can't bootstrap.
Sorry, that was sloppy, I've fixed it.
--
You have this in your patch file, which can't be right
+ | CHoleCan {
+ cc_ev :: CtEvidence,
+ cc_hole_ty :: TcTauType, -- Not a Xi! See same not as above
+ cc_depth:: SubGoalDepth-- See Note [WorkList]
+}
+
\end{code}
\begin{code}
@@ -933,6 +940,9 @@ ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 })
= mkTcEqPred (mkTyConApp fn xis1) xi2
ctPred (CIrredEvCan { cc_ty = xi }) = xi
+ctPred (CHoleCan { cc_flavor = fl, cc_hole_ty = xi })
+ = xi
+
since c_flavor isn't a field of CHoleCan.
This code is gone after merging with HEAD.
---
| The 3 currently remaining issues:
|
| - Free type variables are not tidied consistently. For every one of
| these hole warnings, the same TidyEnv is reused, without taking the
| updates from the other holes into account. I'm pretty sure I know where
| this happens and how I could fix it.
This should be easy.
* TcErrors.reportUnsolved uses tyVarsOfWC to find the free type variables
of unsolved constraints
* It then uses tidyFreeTyVars to assign them names
* And that gives an env used in tidying.
So it should just work. I hope you are letting the various 'tidy' calls in
TcErrors do the work.
I traced the problem back to not zonking the hole constraint properly,
reporting them now works as it should (I've removed the hack I was
using, and cleaned up some code that didn't need to be monadic
anymore).
(The reason they weren't zonked properly is that I've given zonkCt a
special case for CHoleCans
(https://github.com/xnyhps/ghc/blob/eee4242df72cf0a7910e896c3bd6d0fb20b97e37/compiler/typecheck/TcMType.lhs#L619),
as holes themselves do not carry enough information for me to turn
them from CNonCanonicals back into CHoleCans (they become
CIrredEvCans). I'm still not sure this is the right thing to do here.)
| - What I thought would be the local environment doesn't actually seem
| to be it. The holes store in their origin the result of `getLclTypeEnv'
| at their location, but as the Note [Bindings with closed types] says,
| the TopLevelFlag of these don't actually differentiate the top level
| from the non-top level bindings. I think it would be more helpful to
| only show the non-top level bindings at the hole's location, any hints
| about how to obtain just these would be appreciated.
In this context local means this module rather than not top level. Use
isExternalName to distinguish top-level things from nested things.
This works now, thanks!
| - The holes do not have very accurate source location information, like
| some other errors have. The hole has its origin, (test2.hs:3:16), but
| somehow not something like: In the expression: folder _ x _, In an
| equation for `test': test x = foldr _ x _. Help with how that is
| supposed to work would also be appreciated.
That's odd. Every Wanted constraint has a WantedLoc (TcRnTypes), which
includes a [ErrCtxt], which is that stack of In ..; In... stuff you see.
Code looks plausible.
I've fixed the way I was constructing the CtLoc, this was wrong and
was always using [] as the [ErrCtxt].
Regards,
Thijs Alkemade
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Holes in GHC
Can you give me read/write access to your github repo? I'm simonpj on github.
That way I can add comments/questions in code, and generally clean up.
It would make things easier if you could merge with HEAD so that I don't have
to mess around moving libraries back in time.
--
You've put LANGUAGE Holes in TcErrors which means I can't bootstrap.
--
You have this in your patch file, which can't be right
+ | CHoleCan {
+ cc_ev :: CtEvidence,
+ cc_hole_ty :: TcTauType, -- Not a Xi! See same not as above
+ cc_depth:: SubGoalDepth-- See Note [WorkList]
+}
+
\end{code}
\begin{code}
@@ -933,6 +940,9 @@ ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 })
= mkTcEqPred (mkTyConApp fn xis1) xi2
ctPred (CIrredEvCan { cc_ty = xi }) = xi
+ctPred (CHoleCan { cc_flavor = fl, cc_hole_ty = xi })
+ = xi
+
since c_flavor isn't a field of CHoleCan.
---
| The 3 currently remaining issues:
|
| - Free type variables are not tidied consistently. For every one of
| these hole warnings, the same TidyEnv is reused, without taking the
| updates from the other holes into account. I'm pretty sure I know where
| this happens and how I could fix it.
This should be easy.
* TcErrors.reportUnsolved uses tyVarsOfWC to find the free type variables
of unsolved constraints
* It then uses tidyFreeTyVars to assign them names
* And that gives an env used in tidying.
So it should just work. I hope you are letting the various 'tidy' calls in
TcErrors do the work.
| - What I thought would be the local environment doesn't actually seem
| to be it. The holes store in their origin the result of `getLclTypeEnv'
| at their location, but as the Note [Bindings with closed types] says,
| the TopLevelFlag of these don't actually differentiate the top level
| from the non-top level bindings. I think it would be more helpful to
| only show the non-top level bindings at the hole's location, any hints
| about how to obtain just these would be appreciated.
In this context local means this module rather than not top level. Use
isExternalName to distinguish top-level things from nested things.
| - The holes do not have very accurate source location information, like
| some other errors have. The hole has its origin, (test2.hs:3:16), but
| somehow not something like: In the expression: folder _ x _, In an
| equation for `test': test x = foldr _ x _. Help with how that is
| supposed to work would also be appreciated.
That's odd. Every Wanted constraint has a WantedLoc (TcRnTypes), which
includes a [ErrCtxt], which is that stack of In ..; In... stuff you see.
Code looks plausible.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
Hi Simon and others,
Yes, an update on our holes in GHC project was very due.
What I've been working on:
- The command line flag -XHoles and as a language pragma {-# LANGUAGE Holes #-}
now work
- Holes print a warning message with:
- The origin of their type variables
- Their local environment
- Most of the code has been cleaned up to prepare it for submission as a patch.
As an example of the message, consider the module:
---
{-# LANGUAGE Holes #-}
test x = foldr _ x _
---
This prints:
---
[1 of 1] Compiling Main ( test2.hs, interpreted )
test2.hs:3:16: Warning:
Found hole `_' with type a0 - b - b
Where: `b' is a rigid type variable bound by
the inferred type of test :: b - b at test2.hs:3:1
`a0' is a free type variable
In scope: x :: b
test2.hs:3:20: Warning:
Found hole `_' with type [a0]
Where: `a0' is a free type variable
In scope: x :: b
Ok, modules loaded: Main
---
The 3 currently remaining issues:
- Free type variables are not tidied consistently. For every one of these hole
warnings, the same TidyEnv is reused, without taking the updates from the other
holes into account. I'm pretty sure I know where this happens and how I could
fix it.
- What I thought would be the local environment doesn't actually seem to be it.
The holes store in their origin the result of `getLclTypeEnv' at their
location, but as the Note [Bindings with closed types] says, the TopLevelFlag
of these don't actually differentiate the top level from the non-top level
bindings. I think it would be more helpful to only show the non-top level
bindings at the hole's location, any hints about how to obtain just these would
be appreciated.
- The holes do not have very accurate source location information, like some
other errors have. The hole has its origin, (test2.hs:3:16), but somehow not
something like: In the expression: folder _ x _, In an equation for `test':
test x = foldr _ x _. Help with how that is supposed to work would also be
appreciated.
I'm attaching a patch of all my changes compared to HEAD as of about a week
ago. All my work can also still be found on https://github.com/xnyhps/ghc.
patch.diff.gz
Description: GNU Zip compressed data
Best regards,
Thijs Alkemade
signature.asc
Description: Message signed with OpenPGP using GPGMail
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
Not sure if I misparsed your response or not. Its not just things that can or could match the type of the scope, but basically anything introduced in local scopes around the hole, those can have types that you can't talk about outside of a local context, due to existentials that were opened, etc. The usual agda idiom is to make the hole, then check to see what is available that you can use to build towards filling it in, but those locally introduced things may not have anything in common with the type of the hole. -Edward On Mon, Feb 13, 2012 at 4:09 AM, Thijs Alkemade thijsalkem...@gmail.comwrote: On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh andres.l...@googlemail.com wrote: Hi Thijs. Sorry if this has been discussed before. In my opinion, the main advantage of Agda goals is not that the type of the hole itself is shown, but that you get information about all the locally defined identifiers and their types in the context of the hole. Your page doesn't seem to discuss this at all. Without that extra info, I don't see much purpose in the feature, though, because as others have indicated, it can relatively easily be simulated already. Cheers, Andres Hi Andres, Thanks for your feedback. Showing everything in scope that matches or can match the type of a hole is certainly something I am interested in, but I'm afraid it's out of the scope of this project. I think finding the types of the holes is a good first step that should make this feature easier to implement later. Best regards, Thijs Alkemade ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Holes in GHC
For those of us unfamiliar with Agda would somebody explain what you mean by showing ‘anything introduced in local scopes around the hole’? If the hole were at the top level then this would be the module context and loading it into ghci would give you what you need? (Or more realistically you would be looking at the import statements and looking up the documentation, possibly with IDE tools.) Of course, if the hole is inside the scope of ‘let’ or ‘where’ clauses then you could be missing some details of important pieces needed to fill the hole. If I have understood this, the hole names a context in the code, which is generally *not* at the top level; the filling machinery is mostly concerned with reporting on that context. Thijs is proposing to start by providing tools to locate the context and report on its type, and add tools for extracting other context later. FWIW, I think Thijs is wise to focus on a core extension to start with. Chris From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-users-boun...@haskell.org] On Behalf Of Edward Kmett Sent: 19 February 2012 02:58 To: Thijs Alkemade Cc: Andres Löh; glasgow-haskell-users@haskell.org Subject: Re: Holes in GHC Not sure if I misparsed your response or not. Its not just things that can or could match the type of the scope, but basically anything introduced in local scopes around the hole, those can have types that you can't talk about outside of a local context, due to existentials that were opened, etc. The usual agda idiom is to make the hole, then check to see what is available that you can use to build towards filling it in, but those locally introduced things may not have anything in common with the type of the hole. -Edward On Mon, Feb 13, 2012 at 4:09 AM, Thijs Alkemade thijsalkem...@gmail.com wrote: On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh andres.l...@googlemail.com wrote: Hi Thijs. Sorry if this has been discussed before. In my opinion, the main advantage of Agda goals is not that the type of the hole itself is shown, but that you get information about all the locally defined identifiers and their types in the context of the hole. Your page doesn't seem to discuss this at all. Without that extra info, I don't see much purpose in the feature, though, because as others have indicated, it can relatively easily be simulated already. Cheers, Andres Hi Andres, Thanks for your feedback. Showing everything in scope that matches or can match the type of a hole is certainly something I am interested in, but I'm afraid it's out of the scope of this project. I think finding the types of the holes is a good first step that should make this feature easier to implement later. Best regards, Thijs Alkemade ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
On Sun, Feb 12, 2012 at 02:55:40PM +0100, Andres Löh wrote: Hi Thijs. Sorry if this has been discussed before. In my opinion, the main advantage of Agda goals is not that the type of the hole itself is shown, but that you get information about all the locally defined identifiers and their types in the context of the hole. Being able to see the available context is indeed a big advantage, but even just seeing the type of the hole is really helpful -- I would certainly use this feature if it were available in Haskell. And we have to start somewhere, don't we? There is certainly no reason we can't later *add* ways of extracting information about the context of a hole. as others have indicated, it can relatively easily be simulated already. I don't think this is true. The wiki page includes a discussion of the current methods for simulating holes and their (substantial) disadvantages. In order to be useful it seems to me that it must be possible to (1) obtain the inferred type of a hole (2) while still allowing the enclosing module to type check. As far as I know, none of the existing solutions satisfy (2). -Brent ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
Hi Brent. as others have indicated, it can relatively easily be simulated already. I don't think this is true. The wiki page includes a discussion of the current methods for simulating holes and their (substantial) disadvantages. In order to be useful it seems to me that it must be possible to (1) obtain the inferred type of a hole (2) while still allowing the enclosing module to type check. As far as I know, none of the existing solutions satisfy (2). You are right, and I want to apologize if I sounded overly negative. I think I was a bit disappointed to see the feature being sold as Agda goals where in fact a major aspect of Agda goals wasn't even being discussed. I agree now, however, that adding the feature in a limited form is still quite useful. Cheers, Andres ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh andres.l...@googlemail.com wrote: Hi Thijs. Sorry if this has been discussed before. In my opinion, the main advantage of Agda goals is not that the type of the hole itself is shown, but that you get information about all the locally defined identifiers and their types in the context of the hole. Your page doesn't seem to discuss this at all. Without that extra info, I don't see much purpose in the feature, though, because as others have indicated, it can relatively easily be simulated already. Cheers, Andres Hi Andres, Thanks for your feedback. Showing everything in scope that matches or can match the type of a hole is certainly something I am interested in, but I'm afraid it's out of the scope of this project. I think finding the types of the holes is a good first step that should make this feature easier to implement later. Best regards, Thijs Alkemade ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
Hi
Sorry to pile in late...
On 13 Feb 2012, at 09:09, Thijs Alkemade wrote:
On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh andres.l...@googlemail.com
wrote:
Hi Thijs.
Sorry if this has been discussed before.
In my opinion, the main advantage of Agda goals is not that the type
of the hole itself is shown, but that you get information about all
the locally defined identifiers and their types in the context of the
hole.
[..]
Thanks for your feedback. Showing everything in scope that matches or
can match the type of a hole is certainly something I am interested
in, but I'm afraid it's out of the scope of this project.
That's not quite what Andres said, although it would also be a useful
piece of functionality.
If I might plug a bit of kit I knocked together recently, if you
cabal install shplit
(see also https://personal.cis.strath.ac.uk/~conor/pub/shplit/ )
you'll get the beginnings of an editor-assistant which just works as
a stdin-stdout transducer. I've been able to wire it into emacs quite
neatly and gedit more clunkily. I'm told vi should be no problem.
Shplit turns
foo :: [x] - [x]
foo xs{-?-} =
into
foo :: [x] - [x]
foo [] =
foo (x : xs) =
by (i) snarfing the datatype declarations from your file (no import
chasing yet) and adding them to a standard collection, (ii) figuring
out the type of the pattern variables given the type signature
provided. Shplit is still very dumb and makes no use of ghc's
typechecker: shplit's typechecker could be used just as easily to
mark up pattern variables with their types, as to do case analysis.
It is rather tempting to push further and make the thing label holes
with their types. Sometimes, the adoption of primitive technology is
a spur to design. If one adopts the transducer model, the question
then arises in what format might we insert this data into the file?.
In the case of typed holes, we can go with types in comments, or
(with careful use of ScopedTypeVariables) we can really attach them
in a way that would get checked.
I think it could be quite a lot of fun to build a helpful tool,
splitting cases, supplying type information, perhaps even offering
a menu of possible ways to build a term. I think the transducer
method is a relatively cheap (* major caveat ahead) and editor-neutral
way to go about it. If you fix a text format for the markup (i.e., for
requests to and responses from the transducer-collaborator), at worst
it's usable just by running the thing on the buffer, but with more
programmable editors, you can easily make more convenient triggers
for the requests, and you can parse the responses (e.g. generating
tooltips or lifting out a list of options as a contextual menu). The
adoption of the transducer model effectively separates the choice of
information and functionality from the design of the user interface,
which has certainly helped me to get on and do something.
The caveat is that transducers require not just parsing source code
but the ability to reconstruct it, slightly modified. Currently,
she and shplit have very selective, primitive technology for doing
this. Parsing-for-transduction is surely worth a proper think.
All the best
Conor
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
Hi Thijs. Sorry if this has been discussed before. In my opinion, the main advantage of Agda goals is not that the type of the hole itself is shown, but that you get information about all the locally defined identifiers and their types in the context of the hole. Your page doesn't seem to discuss this at all. Without that extra info, I don't see much purpose in the feature, though, because as others have indicated, it can relatively easily be simulated already. Cheers, Andres ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
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-boun...@haskell.org [mailto:glasgow-haskell-users- | boun...@haskell.org] On Behalf Of Thijs Alkemade | Sent: 25 January 2012 15:21 | To: glasgow-haskell-users@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@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Holes in GHC
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-boun...@haskell.org [mailto:glasgow-haskell-users- | boun...@haskell.org] On Behalf Of Simon Peyton-Jones | Sent: 26 January 2012 14:25 | To: Thijs Alkemade; glasgow-haskell-users@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-boun...@haskell.org [mailto:glasgow-haskell- | users- | | boun...@haskell.org] On Behalf Of Thijs Alkemade | | Sent: 25 January 2012 15:21 | | To: glasgow-haskell-users@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@haskell.org | | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users | | | | ___ | Glasgow-haskell-users mailing list | Glasgow
Re: Holes in GHC
On 25/01/12 16:21, Thijs Alkemade wrote: Hello! ... 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] You can do something similar right now with implicit parameters: Prelude :set -XImplicitParams Prelude :t [?a, ()] [?a, ()] :: (?a::()) = [()] Prelude :t map ?a ?b map ?a ?b :: (?b::[a], ?a::a - b) = [b] Twan ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
On Thu, Jan 26, 2012 at 5:10 PM, Simon Peyton-Jones simo...@microsoft.com wrote: ... 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 On Thu, Jan 26, 2012 at 5:26 PM, Twan van Laarhoven twa...@gmail.com wrote: You can do something similar right now with implicit parameters: ... Twan Thanks for your feedback. Let me try to describe the goal better. The intended users are people new to Haskell or people working with existing code they are not familiar with. When starting with Haskell, at least in my experience, it happens lot that you have an idea about what you need to write, but there are some parts in the expression you're working on you don't know yet. For example, you might have a function you want to call, but some arguments you don't know yet how to supply. You can put `undefined` in those places, and after that it compiles (and maybe if you're lucky it will even run), but that will not help to figure out what the correct thing to put there is. This is where you would want to use a hole. Just like undefined, it has type `a`, so it can be used anywhere (and when compiling, we intend to turn it into an exception too), but the difference with undefined is that after the typechecking has succeeded, you get a list of your holes, with the type that was inferred for them, as a sort of todo-list. So there are certainly ways to figure out this information right now, but the goal is to use it as feedback to the user when writing code. Yes, it's possible to translate the expression by changing holes into arguments of a function, but that might be problematic when that expression is part of a module, as to properly typecheck that expression the whole module needs to be typechecked. I have not used them myself, but I think people learning Haskell will easily end up shooting themselves in the foot with implicit parameters. A more general, but different, way to achieve this goal we are considering is: being able to use the typechecker to get more than just the final type of an expression, but also the types of certain subexpressions. Imagine being able to annotate an expression (for example, with certain brackets), to say typecheck everything, and after that, also show me the type of this part. As an update to my problem with Any *: I think I've found the cause. The holes were inferred independently, not all of them at once (they are now all passed as name_taus to simplifyInfer), and this was happening after zonkTopDecls was already done, so all unbound type variables had already been zapped to Any * (as that uses emptyZonkEnv). Regards, Thijs Alkemade ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
On Thu, Jan 26, 2012 at 12:45 PM, Thijs Alkemade thijsalkem...@gmail.com wrote: Let me try to describe the goal better. The intended users are people new to Haskell or people working with existing code they are not familiar with. Also me. I want this feature. It pretty much single handedly makes prototyping things in Agda and then porting them to Haskell a better experience than writing them straight in Haskell to begin with. I can partially implement functions and get feedback on what I need to provide and what is available, add candidate terms, have them type checked and filled in if they work. Etc. It's significantly better than any Haskell editor I'm aware of, and adding undefined or ?foo and poking at things in ghci isn't comparable. -- Dan ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Holes in GHC
| This is where you would want to use a hole. Just like undefined, it | has type `a`, so it can be used anywhere (and when compiling, we | intend to turn it into an exception too), but the difference with | undefined is that after the typechecking has succeeded, you get a list | of your holes, with the type that was inferred for them, as a sort of | todo-list. I'm sorry to be slow, but I still don't understand what you intend. I wonder whether you could give a series of examples? Is this something to do with GHCi? Or some hypothetical IDE? Or do you expect to compile Foo.hs with some holes in it, and get some output relating to the holes? Be as concrete as you possibly can. Precisely how do you expect people to interact with the system you envisage? What do they type in? What output do they see on the screen? Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Holes in GHC
| Let me try to describe the goal better. The intended users are people | new to Haskell or people working with existing code they are not | familiar with. | | Also me. I want this feature. My question remains: what is the feature? Agda has a sophisticated IDE; is that a key part of the feature. I expect so. Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
On Thu, Jan 26, 2012 at 14:36, Simon Peyton-Jones simo...@microsoft.comwrote: | Let me try to describe the goal better. The intended users are people | new to Haskell or people working with existing code they are not | familiar with. | | Also me. I want this feature. My question remains: what is the feature? Agda has a sophisticated IDE; is that a key part of the feature. I expect so. As I understand it, the feature is IDE *support*; they're trying to provide information for use by an IDE (or by hand, but I don't think that's key) that GHC currently makes somewhat difficult to get, from past discussions about how to pull various things out of the typechecker via ghc-api. -- brandon s allbery allber...@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
On Thu, Jan 26, 2012 at 2:36 PM, Simon Peyton-Jones
simo...@microsoft.com wrote:
| Let me try to describe the goal better. The intended users are people
| new to Haskell or people working with existing code they are not
| familiar with.
|
| Also me. I want this feature.
My question remains: what is the feature? Agda has a sophisticated IDE; is
that a key part of the feature. I expect so.
The Agda piece of the feature is support for keeping a type checker
running continuously, which has the ability to type check expressions
with holes, like:
foo { }0 bar baz { }1
and can be queried for the type of expression that must be put into
the holes to make them type check, a list of all the variables in
scope at each hole together with their types, and the ability to type
check expressions against the necessary type for each hole without
rechecking the entire file (at least in the Agda case, checking the
part can be much faster than checking the whole; perhaps it'd matter
less in GHC). It probably must also be possible to tell the system
you're filling in a hole, because that might refine the type of the
other holes.
The rest is an emacs mode that interacts with the running type checker
appropriately.
Another view might be that the holes allow you to capture and interact
with contexts in the middle of type checking. A hole captures the
continuation, and then proceeds as if successful for any type, but the
continuation may be queried for the above information. Then you can
call the continuation to fill in the holes (possibly with expressions
having their own holes). But I'm not going to suggest that's a
feasible way to implement it.
The support of the compiler is necessary before you can build any
editor making use of it, though.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
On Thu, Jan 26, 2012 at 8:33 PM, Simon Peyton-Jones simo...@microsoft.com wrote: I'm sorry to be slow, but I still don't understand what you intend. I wonder whether you could give a series of examples? Is this something to do with GHCi? Or some hypothetical IDE? Or do you expect to compile Foo.hs with some holes in it, and get some output relating to the holes? Be as concrete as you possibly can. Precisely how do you expect people to interact with the system you envisage? What do they type in? What output do they see on the screen? Simon The primary goal is to make this part of GHCi. Say, you're working on a file Foo.hs in your favorite editor, and you have: --- foo = foldr __ 0 [1..5] --- And you have no idea what you should use at the location of the __. You bring up GHCi, and load it as a module: $ ghci GHCi, version 7.5.20120126: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Prelude :load Foo.hs [1 of 1] Compiling Main ( Foo.hs, interpreted ) Found a hole at Foo.hs:1:13-14: Integer - Integer - Integer ... You notice it needs a function, so you make some more changes and hit save, so Foo.hs now contains: --- foo = foldr (\x - __) 0 [1..5] --- You reload GHCi, to see if you made progress: *Main :r [1 of 1] Compiling Main ( Foo.hs, interpreted ) Found a hole at Foo.hs:1:20-21: Integer - Integer ... And that's it. It might help IDEs later on, but that is not our goal. Regards, Thijs Alkemade ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Holes in GHC
| The primary goal is to make this part of GHCi. Say, you're working on
| a file Foo.hs in your favorite editor, and you have:
Aha. That is helpful (below). Start a GHC wiki page to describe?
Now, if I compile
{-# LANGUAGE ImplicitParams #-}
module Foo where
foo = foldr ?x 'x' [True,False]
I get this:
Foo.hs:4:13:
Unbound implicit parameter (?x::Bool - Char - Char)
arising from a use of implicit parameter `?x'
That looks pretty close to what you want, no? You want the error
Foo.hs:4:13:
Found a hole of type: Bool - Char - Char
Same information, with different wording.
This reminds me of the recently implemented -fdefer-type-errors. You'd want to
be able to *run* a program with hole in it, getting the unfilled hole of type
Bool - Char - Char error if you ever need to evaluate the hole.
Anyway, now I understand more clearly what you are trying to do. Thanks.
Simon
| The primary goal is to make this part of GHCi. Say, you're working on
| a file Foo.hs in your favorite editor, and you have:
|
| ---
|
| foo = foldr __ 0 [1..5]
|
| ---
|
| And you have no idea what you should use at the location of the __.
| You bring up GHCi, and load it as a module:
|
| $ ghci
| GHCi, version 7.5.20120126: http://www.haskell.org/ghc/ :? for help
| Loading package ghc-prim ... linking ... done.
| Loading package integer-gmp ... linking ... done.
| Loading package base ... linking ... done.
| Prelude :load Foo.hs
| [1 of 1] Compiling Main ( Foo.hs, interpreted )
| Found a hole at Foo.hs:1:13-14: Integer - Integer - Integer
| ...
|
| You notice it needs a function, so you make some more changes and hit
| save, so Foo.hs now contains:
|
| ---
|
| foo = foldr (\x - __) 0 [1..5]
|
| ---
|
| You reload GHCi, to see if you made progress:
|
| *Main :r
| [1 of 1] Compiling Main ( Foo.hs, interpreted )
| Found a hole at Foo.hs:1:20-21: Integer - Integer
| ...
|
| And that's it. It might help IDEs later on, but that is not our goal.
|
| Regards,
| Thijs Alkemade
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
Thijs Alkemade thijsalkemade at gmail.com writes: On Thu, Jan 26, 2012 at 8:33 PM, Simon Peyton-Jones simonpj at microsoft.com wrote: I'm sorry to be slow, but I still don't understand what you intend. Hi Thijs, like Simon, I'm struggling to see the point. You said earlier: The intended users are people new to Haskell or people working with existing code they are not familiar with. I would expect newbies to at least work through some tutorials or 'try Haskeel on-line' before being let loose at the GHCi prompt. The primary goal is to make this part of GHCi. Say, you're working on a file Foo.hs in your favorite editor, and you have: --- foo = foldr __ 0 [1..5] --- And you have no idea what you should use at the location of the __. You bring up GHCi, and load it as a module: I would do: :t foldr or :t \__f - foldr __f 0 [1..5] If the user doesn't know why asking for the type of a term would help, or can't figure out which sub-term they need to worry about, or doesn't understand the type they get back, I don't see that any fancy extension to GHCi is going to help much. AntC ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
On 1/26/12 1:30 PM, Dan Doel wrote: On Thu, Jan 26, 2012 at 12:45 PM, Thijs Alkemade thijsalkem...@gmail.com wrote: Let me try to describe the goal better. The intended users are people new to Haskell or people working with existing code they are not familiar with. Also me. I want this feature. It pretty much single handedly makes prototyping things in Agda and then porting them to Haskell a better experience than writing them straight in Haskell to begin with. I can partially implement functions and get feedback on what I need to provide and what is available, add candidate terms, have them type checked and filled in if they work. Etc. It's significantly better than any Haskell editor I'm aware of, and adding undefined or ?foo and poking at things in ghci isn't comparable. Ditto. I've long wished for holes and sheds in Haskell. I do a lot of my programming in an interactive bric-a-brac manner. And ever since I've started hacking with Coq and Agda ---even more than the dependent types--- this sort of interactivity has become a must-have feature. Just think about how having a REPL makes life so much nicer than going through the build cycle every time you change something. Having holes and sheds is like making the same leap in utility and productivity, except that we're making the leap from where REPLs leave off. -- Live well, ~wren ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
Hello, On Wed, Jan 25, 2012 at 7:21 AM, Thijs Alkemade thijsalkem...@gmail.com wrote: 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? The type `Any` is just an ordinary monomorphic type, (e.g., like Int`). It is used to stand in for types that do not matter and may be thought of a special case of defaulting (i.e. resolving type ambiguity be selecting concrete types). How it is used is probably best illustrated with an example (you've found one, but I'll use a slightly simpler one). Consider the expression `null []`. It clearly has the type Bool, because `null` takes a list and returns a Bool, and `[]` is a list. However, there is nothing that forces the list elements to be of one type or another, so we cannot infer the full type of `[]`---in some sense, the expression `null []` is of type `forall a. Bool` where `a` is the type of the list elements. Inferring this type would not be useful because we have no way to specify what the `a` should be, and furthermore, it does not matter! So, whenever GHC infers a type `forall a. P = t` where `a` does not appear in `P` or `t`, it knows that the `a` does not matter, so t simply defaults it to `Any`. 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. I was just wondering if you could get the same behavior by using `undefined`? For example, :t [undefined, ()] [()] -Iavor ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Holes in GHC
On Wed, Jan 25, 2012 at 5:50 PM, Iavor Diatchki iavor.diatc...@gmail.com wrote: So, whenever GHC infers a type `forall a. P = t` where `a` does not appear in `P` or `t`, it knows that the `a` does not matter, so t simply defaults it to `Any`. Okay. Thanks for your explanation. But it's still not clear to me in which way using Any instead of a is advantageous here (unless the goal is simply to remove the unnecessary forall from the type signature.) But I guess what we really need: how can we indicate the `a` is does matter to us? I was just wondering if you could get the same behavior by using `undefined`? For example, :t [undefined, ()] [()] Yes, it typechecks the same way as undefined. However, the goal is to find the types of all the holes in the input and present them to the user, in, for example, a learning tool. Inserting `undefined` will make it typecheck, but gives you no information beyond that. And, as undefined is just a function in the Prelude, it doesn't get treated in a special way by the typechecker. So it was considered to use `undefined` to denote a hole, but that would require a much uglier implementation (something like checking the Name of all HsVars in tcExpr) than extending the syntax would. On Wed, Jan 25, 2012 at 6:37 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: Have you considered the monomorphism restriction? For instance, does f () = map __ __ exhibit the same problem when typechecked in a module? Yes, it shows the same Any * types. On Wed, Jan 25, 2012 at 6:10 PM, Simon Peyton-Jones simo...@microsoft.com wrote: are you or any of your colleagues at POPL? If so could talk in person. Simon Nope. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
