On Wed, Jan 25, 2012 at 5:50 PM, Iavor Diatchki 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 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 wrote:

are you or any of your colleagues at POPL? If so could talk in person. Simon

Nope.

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@haskell.org [mailto:glasgow-haskell-users- | bounces@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-bounces@haskell.org [mailto:glasgow-haskell- | users- | | bounces@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

On Thu, Jan 26, 2012 at 5:10 PM, Simon Peyton-Jones 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 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

| > 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

On Thu, Jan 26, 2012 at 2:36 PM, Simon Peyton-Jones 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.

| 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

| 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

On 26/01/2012, Thijs Alkemade 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. 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.

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.

Megawin. Many times, lost in a tangle of code, this was just what I needed, and, alas, just what I lacked.

Regards, Thijs Alkemade

Also, I think it would be nice to have a mode in which GHC would just print the type of each hole in a module. Otherwise, one might have to load each needed module in GHCi, which could be awkward, especially if the holed term is in definition of others. Cheers, MFD

Hi Alkenade, This is the way I do all of my Haskell programming, without any need for language support. I never use undefined for anything else -- or head, any other partial functions or partial case expressions. It may be because of wiring or habituation, but I have assumed that this is the way folks program Haskell. I suspect hardened Haskell hacks may not need it because they are so habituated to doing it anyway. If that is the case then it must be a great initiative! -- who cares about the has-beens, the future is the important thing! I have too much on to help out much but I will try and provide feedback when I can. Chris -----Original Message----- From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Thijs Alkemade Sent: 10 February 2012 13:07 To: glasgow-haskell-users@haskell.org Subject: Re: Holes in GHC Hello all, We've started a wiki-page discussing how this idea can be applied to GHC here: http://hackage.haskell.org/trac/ghc/wiki/Holes There have already been a number of people who indicated they'd want to use this, so feel free to use the page to leave your comments about how you'd want to use it. Any comments on the best way to implement it are welcome too. We are currently working with the idea of named holes[1], for which we are not using the method mentioned in our earlier mails, but we're working on an implementation more similar to how implicit parameters work. I.e. generating constrains when a hole is encountered, so the same name used multiple times will be inferred correctly. However, these should propagate differently from implicit parameters and should not create an error when the constraint is not in the type signature. Regards, Thijs Alkemade [1] http://hackage.haskell.org/trac/ghc/wiki/Holes#Namedholes _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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

On Sun, Feb 12, 2012 at 2:55 PM, 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. 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

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 wrote:

On Sun, Feb 12, 2012 at 2:55 PM, 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. 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