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
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
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.
@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
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
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
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
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
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
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
| 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
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
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
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
| 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
| 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
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
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
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
| 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
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
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
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
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,
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
26 matches
Mail list logo
