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 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 ___ 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 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 > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Removal of #include from template-hsc.h breaks largefile support on 32bit Linux
On Sat, Feb 18, 2012 at 15:15, Eugene Crosser wrote: > I think it would be a right thing to provide the author of an external > module > with "baseline" C environment by default, compatible with the environment > under > which the modules bundled with the compiler where built. And on top of > that, > allow them to use autoconf/whatever else to deviate from that if they need > to. Agreed. There's a reason that languages with lots of experience with extensions (e.g. Perl, Python) make all the details of the environment the runtime was built under available to extensions/native code modules; you might be running a binary distribution on a system that is compatible with but not natively the same as the runtime's build environment, so using autoconf-type stuff to determine the native environment will lead to the extension having an inefficient, or at worst subtly (or not so subtly, as with 32 vs. 64 bit issues) incompatible, link to the runtime. You *really* don't want the runtime to be marshaling 32-bit values based on how it was built, but the module using autoconf to determine that the native value size is 64 bits and treating the marshaled value as such, or vice versa. (In fact, just based on its name, I would have assumed that the point of HsFFI.h is to insure hsc2hs-ed (that is, FFI-using) modules get the types right, so making hsc2hs not use HsFFI.h makes little sense on its face.) -- 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: Removal of #include from template-hsc.h breaks largefile support on 32bit Linux
I don't know enough to understand if the "hard" troubles described by John Meacham are real, but I think that even if they are not, the current situation violates the "principle of least surprise" for the author of a module. Such author may be unaware of the need to take special steps to make his module use the same file API as the builtin language functions, and that will lead to situations when the modules bundled with the compiler can deal with >4Gb files but the new module cannot. It may be even worse for instance with respect to reentrancy of the code: the author of the module may not realize that he needs to take special steps or e.g. the handling of errno will be broken in multithreaded environment. In extreme case, even the opposite situation is possible: the module's autoconf may detect some obscure incompatible feature of the system that the base build did not know about (even if this is a pure theoretical danger). I think it would be a right thing to provide the author of an external module with "baseline" C environment by default, compatible with the environment under which the modules bundled with the compiler where built. And on top of that, allow them to use autoconf/whatever else to deviate from that if they need to. Eugene signature.asc Description: OpenPGP digital signature ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users