Hi Simon,
On Tue, Aug 21, 2012 at 7:14 PM, Simon Peyton-Jones
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
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.
-
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
-
@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, d
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.
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
> 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 s
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 typ
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
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
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
try and provide feedback when
I can.
Chris
-Original Message-
From: glasgow-haskell-users-boun...@haskell.org
[mailto:glasgow-haskell-users-boun...@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
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 u
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
On 1/26/12 1:30 PM, Dan Doel wrote:
On Thu, Jan 26, 2012 at 12:45 PM, 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.
Also me. I want this feature. It pretty much singl
Thijs Alkemade gmail.com> writes:
>
> On Thu, Jan 26, 2012 at 8:33 PM, Simon Peyton-Jones
> 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 peop
| 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
On Thu, Jan 26, 2012 at 8:33 PM, Simon Peyton-Jones
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 som
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
On Thu, Jan 26, 2012 at 14:36, 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 i
| > 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 o
| 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,
On Thu, Jan 26, 2012 at 12:45 PM, 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.
Also me. I want this feature. It pretty much single handedly makes
prototyping things
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:
>
On 25/01/12 16:21, Thijs Alkemade wrote:
Hello!
...
Examples:
*Main> :t [__, ()]
tcRnExpr2: [(:1:2-3, ())]
[__, ()] :: [()]
*Main> :t map __ __
tcRnExpr2: [(:1:5-6, a0 -> b), (:1:8-9, [a0])]
map __ __ :: [b]
You can do something similar right now with implicit parameters:
Prelude>
s
| 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
whe
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'
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
Hi Iavor,
Thank you for your response.
On Wed, Jan 25, 2012 at 17:50, Iavor Diatchki wrote:
> On Wed, Jan 25, 2012 at 7:21 AM, Thijs Alkemade 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
Hello,
On Wed, Jan 25, 2012 at 7:21 AM, Thijs Alkemade 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),
>
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 th
30 matches
Mail list logo
