On Mon, Feb 13, 2012 at 3:27 PM, Simon Marlow wrote:
> On 13/02/12 18:16, Edward Kmett wrote:
>
>> You could probably get away with something like
>>
>> data Proxy = Proxy a
>>
>> class Typeable a where
>> typeOfProxy :: Proxy a -> TypeRep
>>
>> typeOf :: forall a. Typeable a => a -> TypeRep
>>
On 13/02/12 18:16, Edward Kmett wrote:
You could probably get away with something like
data Proxy = Proxy a
class Typeable a where
typeOfProxy :: Proxy a -> TypeRep
typeOf :: forall a. Typeable a => a -> TypeRep
typeOf = typeOfProxy (Proxy :: Proxy a)
which being outside of the class won't
Serge D. Mechveliani wrote:
> Who can tell, please, how read string :: Integer
> is implemented in ghc-7.4.1 ?
> Is it linked from the GMP (Gnu Multi-Precision) library?
I believe your numbers simply were not large enough. I changed
strs n to be
strs n = if n == 0 then [""]
You could probably get away with something like
data Proxy = Proxy a
class Typeable a where
typeOfProxy :: Proxy a -> TypeRep
typeOf :: forall a. Typeable a => a -> TypeRep
typeOf = typeOfProxy (Proxy :: Proxy a)
which being outside of the class won't contribute to the inference of 'a's
kind.
On 10/02/2012 16:03, Simon Peyton-Jones wrote:
Friends
The page describes an improved implementation of the Typeable class, making use
of polymorphic kinds. Technically it is straightforward, but it represents a
non-backward-compatible change to a widely used library, so we need to make a
pla
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
| Should there perhaps be a NewTypeable module which could then be renamed
| into Typeable once it is sufficiently well established?
I started with that idea, but there would be a 2-stage process:
* Step 1: (when PolyTypable becomes available) People change to import
Data.PolyTypeable
* Step
On 10/02/2012 08:01, Evan Laforge wrote:
I like the idea! And it should be possible to build this without modifying
GHC at all, on top of the GHC API. As you say, you'll need a server
process, which accepts command lines, executes them, and sends back the
results. A local socket should be fine
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
11 matches
Mail list logo