On Mon, Feb 13, 2012 at 6:07 AM, Bas van Dijk wrote:

Edward,

it was my impression that you have to use ScopedTypeVariables or other tricks to work with Proxy to.

But with Tagged the situation is similar:

{-# LANGUAGE ScopedTypeVariables #-} typeOf :: forall a. Typeable a => a -> TypeRep typeOf _ = unTagged (typeRep :: Tagged a TypeRep)

or without extensions:

typeOf :: Typeable a => a -> TypeRep typeOf x = unTagged (t x) where t :: Typeable b => b -> Tagged b TypeRep t _ = typeRep

Where is the "huge pain" you are talking about?

The pain is the need to define t. With Proxy you can often use pre-existing combinators, because as a data type, it admits a ton of instances. In this case you can just use 'return' or 'pure'. typeOf :: Typeable a => a -> TypeRep typeOf = typeRep . pure There are fewer combinators from commonly used classes for working with the left argument of a bifunctor, however. -Edward

On Tue, Feb 14, 2012 at 11:18 AM, Iavor Diatchki wrote:

Hello,

On Mon, Feb 13, 2012 at 5:32 PM, Edward Kmett wrote:

...

There are fewer combinators from commonly used classes for working with the left argument of a bifunctor, however.

I think that the bifunctor part of Bas's version is a bit of a red herring. What I like about it is that it overloads exactly what needs to be overloaded---the representation of the type---without the need for any fake parameters. To make things concrete, here is some code:

...

newtype TypeRepT t = TR TypeRep

class Typeable t where typeRep :: TypeRepT t

instacne Typeable Int where typeRep = TR type_rep_for_int instance Typeable [] where typeRep = TR type_rep_for_list

I have no problem with this version either, although the Proxy type is useful for a lot of other purposes, while this type is single use. -Edward

Hi, I'm late to reply, but I'd like to advocate a tagged type for typeRep, for a technical reason rather than usability and aesthetics. John Meacham wrote:

Proxy also has the advantage that it almost exactly mirrors what it ends up looking like in core. The application to proxy is the user visible type application.

But type applications can be safely erased by the compiler (in ghc's type class story, only dictionaries will be left -- jhc's story is different). With values, the compiler can never be sure whether they can be erased and therefore doesn't, except for some State# magic. I have been bitten by this difference when playing with type-level nats to implement modular arithmetic. I had code similar to the following. ------------------------------------------------------------------------ {-# LANGUAGE RankNTypes #-} module Nat (modulo) where data Z = Z newtype D1 a = D1 a newtype D2 a = D2 a class Nat a where nat :: a -> Integer instance Nat Z where nat = \_ -> 0 instance Nat a => Nat (D1 a) where nat = \(D1 a) -> 2*nat a + 1 instance Nat a => Nat (D2 a) where nat = \(D2 a) -> 2*nat a + 2 reflect :: (forall a . Nat a => a -> r) -> Integer -> r reflect f 0 = f Z reflect f n = case (n - 1) `divMod` 2 of (d, 0) -> reflect (f . D1) d (d, 1) -> reflect (f . D2) d ------------------------------------------------------------------------ Then I defined a type for integers modulo m, ------------------------------------------------------------------------ newtype R a = R { unR :: Integer } deriving (Eq, Ord, Show) rtag :: R a -> a rtag _ = undefined mkR :: Nat a => Integer -> R a mkR a = let res = R (a `mod` nat (rtag res)) in res instance Nat a => Num (R a) where R a + R b = mkR (a + b) R a * R b = mkR (a * b) R a - R b = mkR (a - b) fromInteger = mkR abs a = 1 signum a = a modulo :: (forall a . Num a => a) -> Integer -> Integer modulo f = reflect (unR . addR f) where addR :: Nat m => (forall a . Num a => a) -> m -> R m addR v _ = v ------------------------------------------------------------------------ The problem was, it's slow. Prelude NatP> modulo (product (map fromInteger [1..1000])) (3^500) `mod` 17 2 (0.25 secs, 426408368 bytes) Can you spot the reason? It took me a while to figure out. The problem is that due to the dummy parameter of 'nat', the modulus is recomputed all the time. One can mostly fix this (relying on let-floating) by using Proxy or changing the instances to ------------------------------------------------------------------------ instance Nat a => Nat (D1 a) where nat = \(D1 a) -> 2*nat (undefined `asTypeOf` a) + 1 instance Nat a => Nat (D2 a) where nat = \(D2 a) -> 2*nat (undefined `asTypeOf` a) + 2 ------------------------------------------------------------------------ but I feel the dummy parameter is ugly - we're representing constants by functions. The tagged representation, on the other hand, creates a class dictionary that contains the constant immediately. To wit, define Tag as ------------------------------------------------------------------------ newtype Tag t a = Tag a proxy :: (Tag t a) -> t -> a proxy (Tag a) _ = a tag :: (t -> a) -> Tag t a tag f = Tag (f undefined) ------------------------------------------------------------------------ and then we can implement the Nat typeclass as ------------------------------------------------------------------------ data Z = Z newtype D1 a = D1 a newtype D2 a = D2 a class Nat a where nat' :: Tag a Integer nat :: Nat a => a -> Integer nat = proxy nat' instance Nat Z where nat' = tag (\_ -> 0) instance Nat a => Nat (D1 a) where nat' = tag (\(D1 a) -> 2*nat a + 1) instance Nat a => Nat (D2 a) where nat' = tag (\(D2 a) -> 2*nat a + 2) reflect :: (forall a . Nat a => a -> r) -> Integer -> r reflect f 0 = f Z reflect f n = case (n - 1) `divMod` 2 of (d, 0) -> reflect (f . D1) d (d, 1) -> reflect (f . D2) d ------------------------------------------------------------------------ Note the use of 'proxy' and 'tag' to avoid most of the pain associated with using tagged types. They are small functions that are inlined and optimised away, and what remains will be the direct computation on class dictionaries that we're after. The rest of the code remains unchanged, and is much faster. Prelude NatT> modulo (product (map fromInteger [1..1000])) (3^500) `mod` 17 2 (0.01 secs, 3751624 bytes) In my view, Typeable and Nat serve a very similar purpose, namely associating a constant of some fixed type to another, varying type. Given that similarity, I feel that the same reasons as above apply to Typeable as well, suggesting to use a tagged type. Best regards, Bertram P.S. complete code is available from http://int-e.cohomology.org/~bf3/haskell/NatP.hs (dummy version) http://int-e.cohomology.org/~bf3/haskell/NatT.hs (tagged version) P.P.S. This is related to my favourite (ab)use of 'unsafeCoerce' -- ghc only -- equivalent to 'reflect', tagged version: reflect' :: (forall a . Nat a => a -> r) -> Integer -> r reflect' f = fromDict (tag f) where fromDict :: (forall a . Nat a => Tag a r) -> Integer -> r fromDict = unsafeCoerce

| - Will it be possible to write e.g. deriving instance Typeable Eq? Not at the moment; we've only been thinking about Typable for things whose kinds bottom out in *, not Constraint. There doesn't seem to be any fundamental obstacle -- but I can't yet see how it would be useful. | - How about deriving instance Typeable Typeable? (It seems Proxy Proxy | works, so maybe this would too.) Ditto. | - Does it make sense to have an instance for (~)? Ditto. | - Will instances be provided for the types in base and built-in to GHC? Yes, that would make sense. | Automatically generate Typeable instances for every type constructor | that is declared. 'deriving Typeable' becomes a no-op. Well, at the moment a type ONLY becomes an instance of a class if you ask for it to be so, so your proposal would be a change of principle. Sometimes *omitting* an instance declaration may be important (eg to prevent a type being serialisable). That said, I can't see when I'd want a type not to be Typeable. I suppose it could be a compiler option. I think the questions here are ones of software engineering rather than being technical. Simon

Aha. Gabor, you're right. Here's my summary. * As soon as we allow constraint kinds, we can abstract over them. Example: data T (c :: * -> Constraint) = MkT (forall a. c a => a -> a) * Hence, (T Eq) and (T Num) are valid types. * Hence they need to be Typable * And hence we must have something very like instance Typeable Eq where ... * All this is fine. But we don't (ever) want the programmer to write any instance of Typeable; that ways lies seg-faults, since we may rely on their veracity. * For normal type we can say "use deriving", but not for classes, which don't have a deriving clause * We could use "standalone deriving" deriving instance Typeable Eq * Or alternatively we could make every data type and class an instance of Typeable automatically; that would save tons of lookup in the massive Typeable-instance table. On reflection I'm quite in favour of this. * If we do make Typeable instances by default, there are two paths Plan A (easy): make GHC derive Typeable for everything, deprecate all uses of 'deriving Typeable'. Small downside: some programs that are currently rejected will be accepted. Plan B (tiresome): have AutoDeriveTypable as an extension. That means maintaining the massive instance table. Personally I vote for Plan A. It's easier and more efficient to implement, and the upside of Plan B is modest in the extreme. Opinions from anyone else? Simon | -----Original Message----- | From: Gábor Lehel [mailto:illissius@gmail.com] | Sent: 25 September 2012 10:30 | To: Simon Peyton-Jones | Cc: libraries@haskell.org | Subject: Re: Changes to Typeable | | On Mon, Sep 24, 2012 at 6:28 PM, Simon Peyton-Jones | wrote: | > | - Will it be possible to write e.g. deriving instance Typeable Eq? | > | > Not at the moment; we've only been thinking about Typable for things whose | kinds bottom out in *, not Constraint. There doesn't seem to be any fundamental | obstacle -- but I can't yet see how it would be useful. | | One aspect is that if you have SomeType :: Constraint -> * and want | Typeable for SomeType c, which is *, you need Typeable c. | | But the particular application I had in mind is that you could | implement OO-style casting-to-interfaces in a relatively clean way. | | class InterfaceCastable a where | icast :: Typeable c => Proxy c -> a -> Maybe (Interface c) | | data Interface c = forall a. (c a, InterfaceCastable a) => Interface a | | instance InterfaceCastable (Interface c) where icast (Interface a) = icast a | | deriveInterfaceCastable :: Name -> Q [Dec] | | deriveInterfaceCastable could, for example, generate a Map TypeRep (a | -> Any) based on the instances in scope for the named type, where the | (a -> Any) is in reality a -> Interface c and the TypeRep is typeOf c, | and then icast looks up the TypeRep for the constraint that it got, | applies the function to its 'a' argument, and then unsafeCoerces the | result back to Interface c. Which might be going into too much detail, | but the point is that Typeable on constraints would be useful. | (Workarounds are possible, the reason I ask whether this will be | possible is whether it's worth working on them.) | | > | > | - How about deriving instance Typeable Typeable? (It seems Proxy Proxy | > | works, so maybe this would too.) | > | > Ditto. | > | > | - Does it make sense to have an instance for (~)? | > | > Ditto. | > | > | - Will instances be provided for the types in base and built-in to GHC? | > | > Yes, that would make sense. | | I should have said "for types which don't already have them and now | could". But it seems you got my meaning. | | > | > | Automatically generate Typeable instances for every type constructor | > | that is declared. 'deriving Typeable' becomes a no-op. | > | > Well, at the moment a type ONLY becomes an instance of a class if you ask for it | to be so, so your proposal would be a change of principle. Sometimes *omitting* | an instance declaration may be important (eg to prevent a type being | serialisable). That said, I can't see when I'd want a type not to be Typeable. I | suppose it could be a compiler option. I think the questions here are ones of | software engineering rather than being technical. | | Yes, it would be unorthodox. And it's definitely not applicable | willy-nilly to other classes (where not having an instance can be | important, as you say). But at the moment the only consequence I see | of having to derive Typeable manually is hassle, with no upside. | Typeable is increasingly a language feature rather than a library, | with manual instances getting more-and-more discouraged, this would | just take that train of thought further. | | Although, even if this were implemented, you would still need | 'deriving Typeable' if you wanted to stay backwards compatible; and | because it's a significant change to the language you would presumably | have to hide it behind a language pragma, at which point instead of | {-# LANGUAGE AutoDeriveTypeable #-} you might as well write 'deriving | Typeable'; so maybe it wouldn't be so useful in practice. | | > | > Simon | > | | | | -- | Your ship was destroyed in a monadic eruption.

Uhm, you answered my question already, I just didn't read your email carefully: On Wed, Oct 3, 2012 at 1:01 PM, Simon Peyton-Jones wrote:

* All this is fine. But we don't (ever) want the programmer to write any instance of Typeable; that ways lies seg-faults, since we may rely on their veracity.

I think I agree, but, then again, I have never written my own Typeable instances. Do note, however, that GHC currently uses the `time` package, which gives manual `Typeable` instances (CC-ing Ashley; maybe he can defend writing Typeable instances manually). I noticed this while working on the change-over to the kind-polymorphic `Typeable`. Cheers, Pedro

| I've only manually implemented Typeable instances where GHC couldn't | derive one due to some extension Can you give some examples please? Simon

Plan A does seem better. Speaking of making changes to Typeable, is there a chance of connecting/converting between Data.Typeable.TypeRep and Language.Haskell.TH.Type? Oren Ben-Kiki On Wed, Oct 3, 2012 at 3:03 PM, Edward Kmett wrote:

I'm definitely in favor of Plan A.

-Edward

On Wed, Oct 3, 2012 at 8:01 AM, Simon Peyton-Jones wrote:

...

* If we do make Typeable instances by default, there are two paths Plan A (easy): make GHC derive Typeable for everything, deprecate all uses of 'deriving Typeable'. Small downside: some programs that are currently rejected will be accepted.

Plan B (tiresome): have AutoDeriveTypable as an extension. That means maintaining the massive instance table.

Personally I vote for Plan A. It's easier and more efficient to implement, and the upside of Plan B is modest in the extreme.

I don't think anyone has proposed weakening parametricity in this way. You'd definitely still need f :: (Typeable a, Typeable b) => a -> Maybe b to make that function work. The proposal is just to make the instances available for any concrete type so you don't have to write them (and therefore can't screw them up or do hinky things with them.) -Edward On Wed, Oct 3, 2012 at 9:12 AM, Ian Lynagh wrote:

On Wed, Oct 03, 2012 at 12:01:15PM +0000, Simon Peyton-Jones wrote:

...

* If we do make Typeable instances by default, there are two paths Plan A (easy): make GHC derive Typeable for everything, deprecate all uses of 'deriving Typeable'. Small downside: some

programs

...

that are currently rejected will be accepted.

Do you literally mean "derive Typeable for everything", or do you mean that Typeable would be available for all types, similar to how seq is?

i.e. would this be valid, or would it complain that it cannot infer (Typeable a, Typeable b)?:

f :: a -> Maybe b f = Data.Typeable.cast

Thanks Ian

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

On Wed, Oct 03, 2012 at 09:26:37PM +0100, Robin KAY wrote:

On 03/10/12 14:20, Edward Kmett wrote:

...

I don't think anyone has proposed weakening parametricity in this way. [snip]

I don't think so either, but is there any reason it shouldn't be done?

Yes!! foo :: a -> Int foo x = case typeOf x of Int -> 3 Char -> 4 _ -> 5 A function of type a -> Int is not supposed to be able to do this. If it can, then parametricity goes completely out the window. If we really get rid of parametricity like this then I'm moving to Can^H^H^H Agda. Just because a function has a type like Typeable a => ... doesn't mean the compiler has to use the same mechanism as other type classes to implement it. The idea is that a Typeable dictionary for a concrete type can just be generated "out of thin air", instead of having to maintain a big table of what instances are in scope.

If you give every type a Typeable instance automatically, then it's not effective as a constraint. The compiler would be free to either still use the type-class mechanism behind the scenes or "simply" replace it with magic:-

typeOf :: a -> TypeRep typeOf = rtsInternalGetTypeOf

Note that this doesn't make sense: all types get erased before compile time so there is no way to get a TypeRep from the RTS. In fact we really do need to pass in a Typeable dictionary to a polymorphic function, regardless of how that dictionary was generated at compile time.

Simon's comment that it "would save tons of lookup in the massive Typeable-instance table" seemed to me to imply that there was some kind of optimisation you could make if Typeable wasn't really a type-class internally anyway.

It's not about whether or not Typeable is a type class, it's about where Typeable dictionaries come from --- from a big table, or generated on the fly? -Brent

So back to the Plan A vs Plan B discussion.

I'm sorry, I don't completely understand why Plan A is an "optimization". As far as I know, the typechecker doesn't merely have the task of answering the question "does Typeable X" hold, but rather it has to come up with evidence that "Typeable X" holds. I fail to see how even the knowledge that every concrete datatype is in principle Typeable makes it any easier to come up with the type representation that's required during run-time. For example, if you consider data AnyTypeable = forall a. (Typeable a) => AnyTypeable a and you unpack and use such a value in a function, then clearly the only place to get the type representation from is the constructor itself, and similarly, data Any = forall a. Any a should really not have any type representation available at runtime at all. Similarly, for less extreme cases, we'd still need dictionary transformers and plug together type representations from different components. So why can we get rid of the instance table? What am I missing? Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com

I have some nebulous concerns about abstraction violation, but since Typeable only lets you find out what the structure is, not actually take apart the contained data, it doesn't seem too much of a problem. On 04/10/2012 10:44, Simon Peyton-Jones wrote:

I'm beginning to regret mentioning optimisation -- it's purely an implementation matter. Yes the same dictionaries get constructed, the runtime behaviour is unchanged. The difference is that when GHC asks "Is type constructor T an instance of Typeable" it would know that the answer is "yes, and the dictionary is called $dfTypeableT". That's all. Its saves the lookup, and more important, saves the very existence of the table.

I think it would be better to focus the discussion on the question of whether you would ever NOT want a type constructor to be an instance of Typeable

S

| -----Original Message----- | From: libraries-bounces@haskell.org [mailto:libraries- | bounces@haskell.org] On Behalf Of Andres Löh | Sent: 04 October 2012 10:30 | To: Simon Peyton-Jones | Cc: libraries@haskell.org | Subject: Re: Changes to Typeable | | > So back to the Plan A vs Plan B discussion. | | I'm sorry, I don't completely understand why Plan A is an | "optimization". As far as I know, the typechecker doesn't merely have | the task of answering the question "does Typeable X" hold, but rather it | has to come up with evidence that "Typeable X" holds. I fail to see how | even the knowledge that every concrete datatype is in principle Typeable | makes it any easier to come up with the type representation that's | required during run-time. | | For example, if you consider | | data AnyTypeable = forall a. (Typeable a) => AnyTypeable a | | and you unpack and use such a value in a function, then clearly the only | place to get the type representation from is the constructor itself, and | similarly, | | data Any = forall a. Any a | | should really not have any type representation available at runtime at | all. | | Similarly, for less extreme cases, we'd still need dictionary | transformers and plug together type representations from different | components. So why can we get rid of the instance table? What am I | missing? | | Cheers, | Andres | | -- | Andres Löh, Haskell Consultant | Well-Typed LLP, http://www.well-typed.com | | _______________________________________________ | Libraries mailing list | Libraries@haskell.org | http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

On Thu, Oct 4, 2012 at 5:03 PM, Tyson Whitehead wrote:

On October 4, 2012 07:59:29 Ganesh Sittampalam wrote:

...

I have some nebulous concerns about abstraction violation, but since Typeable only lets you find out what the structure is, not actually take apart the contained data, it doesn't seem too much of a problem.

Ummm. Isn't that what cast (in Data.Typeable) does?

cast :: (Typeable a, Typeable b) => a -> Maybe b

For example, the following function

import Data.Typeable import Data.Maybe

magic :: Typeable a => a -> a magic x = case cast x of Just x -> cast $ fromJust $ x ++ " (ta da)" _ -> x

gives you id except for strings.

ITYM fromJust $ cast rather than the other way around. But the ability to cast like this does not give you access to data structure you didn't already have – it does not violate abstraction. On the other hand, were we to do the same with Data, we /would/ violate abstraction, since Data is capable of synthesising constructors and retrieving fields and so forth. Hence manual instances of Data are fairly common, e.g. for Map and Set. Typeable doesn't seem to give you anything like that, so it seems safe.

On Thu, Oct 4, 2012 at 10:58 PM, Tyson Whitehead wrote:

On October 4, 2012 13:48:42 Ben Millwood wrote:

...

On Thu, Oct 4, 2012 at 5:03 PM, Tyson Whitehead

...

import Data.Typeable import Data.Maybe

magic :: Typeable a => a -> a magic x =

case cast x of

Just x -> cast $ fromJust $ x ++ " (ta da)" _ -> x

gives you id except for strings.

ITYM fromJust $ cast rather than the other way around. But the ability to cast like this does not give you access to data structure you didn't already have – it does not violate abstraction.

Indeed. I did mean those to be swapped. Thanks for picking up on that.

I have to confess though, I'm not really following on how this doesn't give you access to data structure you didn't already have? Perhaps we are not thinking of the same thing when you say "access to data structure"?

Doesn't the above "a -> a" function (under the proposed system where you don't need a "Typeable a" constraint") take apart some of its argument

magic 1 ---> 1 magic 2 ---> 2 magic "hello world" ---> "hello world (ta da)"

Doesn't this mean then that whole "theorems for free" stuff goes out the window? Isn't its whole basis the idea that unconstrained types are actually statements that those arguments won't be constructed/deconstructed?

Thanks! -Tyson

You still need a Typeable constraint! There would *not* be an instance Typeable a there would only be instance Typeable Foo instance Typeable Bar instance Typeable Baz ... for every concrete type that is declared. But there's no universal instance, and there's no way to take advantage of the fact that every particular type has an instance. If you had foo :: a -> a and it was doing things like you described, that would be a big problem! But as discussed previously, that _will not_ happen. You will still need a Typeable constraint to be able to use typeOf and cast. On the other hand if you have bar :: Typeable a => a -> a and it did those, it's unremarkable (it can already do those things). That's a very different type signature from what 'foo' has. The change would be that you could you use 'bar' with any _concrete_ types you supply (so 'Int', or 'Bool', or 'MyData', 'Foo', 'Bar', or 'Baz', but not 'a' or 'b'), instead of only the ones that explicitly have 'deriving Typeable'. The question is whether that's bad in any way -- whether there's any case where you do *not* want a particular type to be an instance of Typeable. The classic case where you do not want a type to implement a class is when the instance would expose implementation details of the type which you want to keep hidden (for example if want to hide data constructors, Data or Generic would be purpose-defeating). So the questions are: (1) Does Typeable expose anything internal to a type which you might want to keep hidden (I don't think so) (2) Are there any other reasons you might want to avoid having an instance (I can't think of any) -- Your ship was destroyed in a monadic eruption.

On 04/10/2012 10:44, Simon Peyton-Jones wrote:

I'm beginning to regret mentioning optimisation -- it's purely an implementation matter. Yes the same dictionaries get constructed, the runtime behaviour is unchanged. The difference is that when GHC asks "Is type constructor T an instance of Typeable" it would know that the answer is "yes, and the dictionary is called $dfTypeableT". That's all. Its saves the lookup, and more important, saves the very existence of the table.

I think it would be better to focus the discussion on the question of whether you would ever NOT want a type constructor to be an instance of Typeable

Code size? It might only be a small effect for most code, but we occasionally see large files of automatically-generated data declarations. Also I rather like it that making a new data type is so cheap in terms of code size. A single module containing "data T = A | B": $ size foo.o text data bss dec hex filename 91 32 0 123 7b foo.o If I add "deriving Typeable": text data bss dec hex filename 587 312 0 899 383 foo.o 7x larger! Cheers, Simon

S

| -----Original Message----- | From: libraries-bounces@haskell.org [mailto:libraries- | bounces@haskell.org] On Behalf Of Andres Löh | Sent: 04 October 2012 10:30 | To: Simon Peyton-Jones | Cc: libraries@haskell.org | Subject: Re: Changes to Typeable | | > So back to the Plan A vs Plan B discussion. | | I'm sorry, I don't completely understand why Plan A is an | "optimization". As far as I know, the typechecker doesn't merely have | the task of answering the question "does Typeable X" hold, but rather it | has to come up with evidence that "Typeable X" holds. I fail to see how | even the knowledge that every concrete datatype is in principle Typeable | makes it any easier to come up with the type representation that's | required during run-time. | | For example, if you consider | | data AnyTypeable = forall a. (Typeable a) => AnyTypeable a | | and you unpack and use such a value in a function, then clearly the only | place to get the type representation from is the constructor itself, and | similarly, | | data Any = forall a. Any a | | should really not have any type representation available at runtime at | all. | | Similarly, for less extreme cases, we'd still need dictionary | transformers and plug together type representations from different | components. So why can we get rid of the instance table? What am I | missing? | | Cheers, | Andres | | -- | Andres Löh, Haskell Consultant | Well-Typed LLP, http://www.well-typed.com | | _______________________________________________ | Libraries mailing list | Libraries@haskell.org | http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

On 08/10/2012 13:12, Ivan Lazar Miljenovic wrote:

On 8 October 2012 22:27, Simon Marlow wrote:

...

On 04/10/2012 10:44, Simon Peyton-Jones wrote:

...

I'm beginning to regret mentioning optimisation -- it's purely an implementation matter. Yes the same dictionaries get constructed, the runtime behaviour is unchanged. The difference is that when GHC asks "Is type constructor T an instance of Typeable" it would know that the answer is "yes, and the dictionary is called $dfTypeableT". That's all. Its saves the lookup, and more important, saves the very existence of the table.

I think it would be better to focus the discussion on the question of whether you would ever NOT want a type constructor to be an instance of Typeable

Code size? It might only be a small effect for most code, but we occasionally see large files of automatically-generated data declarations.

Also I rather like it that making a new data type is so cheap in terms of code size. A single module containing "data T = A | B":

$ size foo.o text data bss dec hex filename 91 32 0 123 7b foo.o

If I add "deriving Typeable":

text data bss dec hex filename 587 312 0 899 383 foo.o

7x larger!

I assume this would affect compilation time as well? I have code containing data types containing large number of constructors (biggest case has 150+) that takes long enough to compile as is :/

The extra time + space would be proportional to the number of data types, not the number of constructors. But it would probably have a big effect on compilation time for a module with lots of data types. Actually we could probably generate a lot less stuff for a derived Typeable instance. Right now we pre-generate both the TypeRep and the TyCon, but we could generate them at runtime from the (package,module,name) triple instead. Cheers, Simon

...

Cheers, Simon

...

S

| -----Original Message----- | From: libraries-bounces@haskell.org [mailto:libraries- | bounces@haskell.org] On Behalf Of Andres Löh | Sent: 04 October 2012 10:30 | To: Simon Peyton-Jones | Cc: libraries@haskell.org | Subject: Re: Changes to Typeable | | > So back to the Plan A vs Plan B discussion. | | I'm sorry, I don't completely understand why Plan A is an | "optimization". As far as I know, the typechecker doesn't merely have | the task of answering the question "does Typeable X" hold, but rather it | has to come up with evidence that "Typeable X" holds. I fail to see how | even the knowledge that every concrete datatype is in principle Typeable | makes it any easier to come up with the type representation that's | required during run-time. | | For example, if you consider | | data AnyTypeable = forall a. (Typeable a) => AnyTypeable a | | and you unpack and use such a value in a function, then clearly the only | place to get the type representation from is the constructor itself, and | similarly, | | data Any = forall a. Any a | | should really not have any type representation available at runtime at | all. | | Similarly, for less extreme cases, we'd still need dictionary | transformers and plug together type representations from different | components. So why can we get rid of the instance table? What am I | missing? | | Cheers, | Andres | | -- | Andres Löh, Haskell Consultant | Well-Typed LLP, http://www.well-typed.com | | _______________________________________________ | Libraries mailing list | Libraries@haskell.org | http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

On 10/8/12 7:27 AM, Simon Marlow wrote:

Code size? It might only be a small effect for most code, but we occasionally see large files of automatically-generated data declarations.

Also I rather like it that making a new data type is so cheap in terms of code size. A single module containing "data T = A | B":

$ size foo.o text data bss dec hex filename 91 32 0 123 7b foo.o

If I add "deriving Typeable":

text data bss dec hex filename 587 312 0 899 383 foo.o

7x larger!

Just in terms of optimization: because they're so lightweight, I've been a big fan of making new data types whenever the slightest need arises--- as opposed to the common practice in other languages of using some "close enough" data type to avoid making a new one. For example, with accumulator-based functions I often codify the accumulator with a data type to help clarify the code and ensure the appropriate strictness. The majority of these throw-away data types are ones which are only used internally and will never leave the module. It'd be nice, therefore, to only autogenerate Typeable instances for data types which actually have a chance of needing them--- i.e., are exported (or use Typeable internally). -- Live well, ~wren

On Wed, Oct 3, 2012 at 10:26 PM, Robin KAY wrote:

Simon's comment that it "would save tons of lookup in the massive Typeable-instance table" seemed to me to imply that there was some kind of optimisation you could make if Typeable wasn't really a type-class internally anyway.

I would think the opposite is true; GHC is good at optimizing overloaded functions when the type is known (this is what INLINABLE does).

On Wed, Oct 3, 2012 at 10:25 PM, Ben Millwood wrote:

On Wed, Oct 3, 2012 at 9:26 PM, Robin KAY wrote:

...

On 03/10/12 14:20, Edward Kmett wrote:

...

I don't think anyone has proposed weakening parametricity in this way.

[snip]

I don't think so either, but is there any reason it shouldn't be done?

Uh, because it weakens parametricity? :) Free theorems would promptly vanish, since we would have effectively added typecase to the language: it would no longer be possible to conclude from a type signature a -> a that the function was the identity, for example.

Oh goodness, I need to stop taking more than six minutes to write a reply :P Feel free to ignore the above, the other comments along the same line are better.

Well, I think there is a general consensus that the existing manual instances for Typeable are more of a liability than a feature, and were a necessary evil given the limitations of the previous system, so either ignoring them or making them an error would make a lot of sense. -Edward On Thu, Oct 4, 2012 at 3:42 PM, Dominique Devriese < dominique.devriese@cs.kuleuven.be> wrote:

Small note while I happen to be reading the list:

...

Plan A (easy): make GHC derive Typeable for everything, deprecate all uses of 'deriving Typeable'. Small downside: some

2012/10/3 Simon Peyton-Jones : programs

...

that are currently rejected will be accepted.

Does this imply forbidding user-written instances of Typeable? If yes, then I guess some currently accepted programs would also be rejected (those with manual instances)? If not, then wouldn't there be duplicate instances? Or would manual instances somehow take priority? Or be ignored?

Dominique

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

Allowing users to write instances leads to potential un-soundness when doing dynamic type casts, so it has always been a Bad Idea.

Related to this, I'm sure several of us remember Bob Harper's blog post[1] regarding exceptions that uses a hand-written Typeable instance. The ideal scenario would be for the compiler to automatically derive Typeable for all types, and completely disallow the user from providing hand-written instances. To take advantage of Typeable, though, the user should still have to annotate the necessary Typeable constraints. Whether this is special-cased in the compiler for optimization is an implementation detail and is largely irrelevant to the Haskell programmer; I say let's follow the common Haskell mentality of making it correct first and fast second. Most typeclasses come with some "laws" that make them useful; I don't see any documented laws for Typeable, but presumably there are some (e.g. no type should say it is another type), and the compiler can automatically derive instances that are guaranteed to follow them. It would be nice to be able to enforce typeclass laws on instances at compile time, but that's stepping into theorem prover territory. [1] http://existentialtype.wordpress.com/2012/08/14/haskell-is-exceptionally-uns... -- Dan Burton

On Sun, Oct 14, 2012 at 2:34 PM, Gábor Lehel wrote:

So apologies for constantly suggesting new things, but if we have,

- All Typeable instances for type constructors are generated by the compiler, and - All Typeable instances for composite types (if that's the word?) are via instance (Typeable f, Typeable a) => Typeable (f a), and - User-written instances, and therefore overlap, are disallowed,

how difficult would it be to add:

foo :: Typeable (f a) => Dict (Typeable f, Typeable a) -- data Dict c where Dict :: c => Dict c

i.e. to make it possible to go in the other direction, and deduce that if a composite type is Typeable, its components must also be?

(alternate encoding: foo :: Typeable (f a) => ((Typeable f, Typeable a) => r) -> r)

Use case: nothing very serious, if it would take significant work, it's not worth it.

Update: I think there's at least one way: class Typeable a where proxyTypeOf :: Proxy a -> TypeRep split :: (a ~ f i) => Dict (Typeable f, Typeable i) -- split :: (a ~ f i) => ((Typeable f, Typeable i) => r) -> r instance (Typeable f, Typeable i) => Typeable (f i) where split = Dict -- split x = x and all the compiler-generated instances for type constructors would just not define split. Which if it were a user writing the code would generate a warning about unimplemented methods (or inaccessible code if they /did/ implement it), but it's not a user writing it, and nothing bad can happen, because the constraint has to hold before you can call the method (so there's no way to hit a bottom). (This would require an extension or two, but if we're already depending on PolyKinds that doesn't seem like a huge deal? And presumably a libraries proposal...)

On Fri, Oct 5, 2012 at 9:06 AM, Simon Peyton-Jones wrote:

...

| Does this imply forbidding user-written instances of Typeable? If yes, | then I guess some currently accepted programs would also be rejected | (those with manual instances)?

Yes, that's the idea; I should have said that. Allowing users to write instances leads to potential un-soundness when doing dynamic type casts, so it has always been a Bad Idea.

Simon

-- Your ship was destroyed in a monadic eruption.

-- Your ship was destroyed in a monadic eruption.

Just want to follow up that I've finally figured out why my original sketch of an implementation was wrong. To recap and narrow it somewhat my idea was essentially: class Typeable a where typeOf :: ... right_ :: (a ~ f b) => PTypeRep b instance (Typeable f, Typeable b) => Typeable (f b) where right_ = PTR The problem is that in 'a ~ f b' the 'b' can have any kind of the caller's choice, and 'instance Typeable (f b)' can also be chosen at any kind for 'b' of the caller's choice, but these are separate choices, and you can't use the one to satisfy the other. (Inside of the instance the kind is fixed by one caller, so it can't by used to satisfy /any other/ kind chosen by the (separate) caller of the method). It's kind of a strange situation where you have to cover the whole space of kinds and types, and 'instance Typeable (f b)' *does* cover the whole space of kinds and types, but you can't make the two halves talk to each other. I'll follow up again if I happen on a solution (but it's possibly impossible). Again, this isn't of any real practical importance for me, just an object of my curiosity. (And aside from all of that, 'PTypeRep' seems like a sensible idea.) On Mon, Oct 29, 2012 at 11:28 PM, Simon Peyton-Jones wrote:

My brain is too small to accommodate all this, and I agree with Pedro that we should keep the "splitting TypeRep" question separate from the "derive Typeable for everything" question.

This response is only about splitting TypeReps. I think Gabor's proposal below will lead to lots of ambiguity, because there is no way to fix the result type of 'split' except by giving it a type signature, which seems a bit clumsy.

Here are some related suggestions though. Consider:

· Currently TypeRep is not parameterised (ie not TypeRep a), for good reason.

· But consider Gabor’s Dict (Typeable t). It is a data constructor containing a dictionary that contains the typeOf function, whose only payload is a TypeRep. So in effect, Dict (Typeable t) is a type-parameterised versoin of TypeRep.

OK suppose we pulled that out, so we have (hidden in the library)

class Typeable a where

typeOf :: Proxy a -> TypeRep

newtype PTypeRep a where

PTR :: Typeable a => PTypeRep a

ptr :: Typeable a => Proxy a => PTypeRep a

ptr _ = PTR

ptrToTR :: forall a. PTypeRep a -> TypeRep

ptrToTR PTR = typeOf (undefined :: Proxy a)

(Pay no attention to the choice of names.) Now PTypeRep is the type-parameterised version of TypeRep. I’m guessing this is a generally-useful thing to have, because it’s a first-class Typeable dictionary.

· You can get it from Typeable via ‘ptr’

· By pattern matching on it you can bring the Typable dictionary into scope if you want.

· You can drop down to TypeRep via ptrToTR.

Now to split. This has to be unsafe, just like Typeable.cast is.

right :: forall f a. PTypeRep (f a) -> PTypeRep a

left PTR = let instance Typeable f where

typeOf _ = case typeOf (undefined :: Proxy (f a)) of

TyConApp tc tys -> last tys

in PTR

We can get the TypeRep for f by decomposing the TypeRep for (f a). But then we need a dictionary for Typable a, and we don’t have a way to build that in Haskell. But it’s trivial in Core. And unsafe of course.

I’m not sure I have all this right, and I’m not at all sure that it’s urgent. But I thought I’d jot it down in case it’s useful.

Simon

| -----Original Message-----

| From: Gábor Lehel [mailto:illissius@gmail.com

]

| Sent: 14 October 2012 14:34

| To: Simon Peyton-Jones

| Cc: Dominique Devriese; José Pedro Magalhães; libraries@haskell.org

| Subject: Re: Changes to Typeable

|

| On Sun, Oct 14, 2012 at 2:34 PM, Gábor Lehel wrote:

| > So apologies for constantly suggesting new things, but if we have,

| >

| > - All Typeable instances for type constructors are generated by the

| > compiler, and

| > - All Typeable instances for composite types (if that's the word?) are

| > via instance (Typeable f, Typeable a) => Typeable (f a), and

| > - User-written instances, and therefore overlap, are disallowed,

| >

| > how difficult would it be to add:

| >

| > foo :: Typeable (f a) => Dict (Typeable f, Typeable a)

| > -- data Dict c where Dict :: c => Dict c

| >

| > i.e. to make it possible to go in the other direction, and deduce that

| > if a composite type is Typeable, its components must also be?

| >

| > (alternate encoding: foo :: Typeable (f a) => ((Typeable f, Typeable

| > a) => r) -> r)

| >

| > Use case: nothing very serious, if it would take significant work,

| > it's not worth it.

|

| Update: I think there's at least one way:

|

| class Typeable a where

| proxyTypeOf :: Proxy a -> TypeRep

| split :: (a ~ f i) => Dict (Typeable f, Typeable i)

| -- split :: (a ~ f i) => ((Typeable f, Typeable i) => r) -> r

|

| instance (Typeable f, Typeable i) => Typeable (f i) where

| split = Dict

| -- split x = x

|

| and all the compiler-generated instances for type constructors would

| just not define split. Which if it were a user writing the code would

| generate a warning about unimplemented methods (or inaccessible code

| if they /did/ implement it), but it's not a user writing it, and

| nothing bad can happen, because the constraint has to hold before you

| can call the method (so there's no way to hit a bottom).

|

| (This would require an extension or two, but if we're already

| depending on PolyKinds that doesn't seem like a huge deal? And

| presumably a libraries proposal...)

|

| >

| > On Fri, Oct 5, 2012 at 9:06 AM, Simon Peyton-Jones

| > wrote:

| >> | Does this imply forbidding user-written instances of Typeable? If yes,

| >> | then I guess some currently accepted programs would also be rejected

| >> | (those with manual instances)?

| >>

| >> Yes, that's the idea; I should have said that. Allowing users to write instances

| leads to potential un-soundness when doing dynamic type casts, so it has always

| been a Bad Idea.

| >>

| >> Simon

| >>

| >>

| >

| >

| >

| > --

| > Your ship was destroyed in a monadic eruption.

|

|

|

| --

| Your ship was destroyed in a monadic eruption.

-- Your ship was destroyed in a monadic eruption.

On Mon, Oct 15, 2012 at 7:58 AM, Emil Axelsson wrote:

I have a use case:

http://hackage.haskell.org/packages/archive/syntactic/1.3/doc/html/Data-Dyna...

This is a reimplementation of Data.Dynamic to support casting type `a` to `Dynamic` given a constraint `Typeable (a -> b)`:

toDyn :: Typeable (a -> b) => P (a -> b) -> a -> Dynamic

With your suggestion, it seems I should be able to use the ordinary Data.Dynamic instead.

/ Emil

Great! Do you like my plan? Or perhaps know of a better one? (Relatedly, *does* this have to go through a separate libraries process? Or are we considering Typeable as getting completely replaced, and everything pertaining to it gets discussed here?) -- Your ship was destroyed in a monadic eruption.

Sorry, I got a bit lost in this discussion. Let me try to provide a summary. Current status: I have a local branch with the new poly-kinded Typeable working fine. It works as described in [1]. It actually allows deriving Typeable for things involving the Constraint kind, but this can be easily disabled. Either way, I think most of this is necessary for whatever might follow next. But I'm not sure of how to push the changes, because I had to make some changes to these repos: array, containers, dph, template-haskell, and vector. Worse, I also had to change time, which gets built from a tarball. It might not be worth contacting the authors of these packages for changes if we're still going to get rid of "deriving Typeable" altogether, so I've been holding this back. It's been proposed to remove the possibility to derive Typeable or write instances for it. I'm supposing the way that this would be implemented would be: 7.8: Any uses of "deriving Typeable" would give rise to a warning saying that it is no longer necessary. Any instances of Typeable would give rise to a warning saying that this code is being ignored, and replaced by an internal Typeable instance. Packages might break, or change runtime behaviour due to this change. 7.10: Explicit uses of "deriving Typeable" or instances are an error. Regarding split :: (a ~ f i) => Dict (Typeable f, Typeable i), I'm not sure I can judge how much work that would be. But let's first try to draft a plan for removing Typeable definitions from the user, and then consider more extensions. Cheers, Pedro [1] http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/PolyTypeable On Tue, Oct 16, 2012 at 8:32 AM, Emil Axelsson wrote:

2012-10-15 23:50, Gábor Lehel skrev:

On Mon, Oct 15, 2012 at 7:58 AM, Emil Axelsson wrote:

...

...

I have a use case:

http://hackage.haskell.org/**packages/archive/syntactic/1.** 3/doc/html/Data-DynamicAlt.**htmlhttp://hackage.haskell.org/packages/archive/syntactic/1.3/doc/html/Data-Dyna...

This is a reimplementation of Data.Dynamic to support casting type `a` to `Dynamic` given a constraint `Typeable (a -> b)`:

toDyn :: Typeable (a -> b) => P (a -> b) -> a -> Dynamic

With your suggestion, it seems I should be able to use the ordinary Data.Dynamic instead.

/ Emil

Great! Do you like my plan? Or perhaps know of a better one?

(Relatedly, *does* this have to go through a separate libraries process? Or are we considering Typeable as getting completely replaced, and everything pertaining to it gets discussed here?)

Your plan certainly seems general enough! But I'm afraid I can't really speak about the implications on libraries etc.

/ Emil

Hi, On Mon, Oct 29, 2012 at 10:28 PM, Simon Peyton-Jones wrote:

Right. Re the library packages that have to change, I replied (4 Oct) thus****

It’s tiresome, but for good reasons. You have to talk to each of the maintainers of the other repos, and ask them to implement a patch, which you’ll supply. The patch will probably have ****

#ifdef __GLASGOW_HASKELL__ >= 7.7****

so that it’ll still work with older versions of the compiler. To give them the background you’ll probably want to update the wiki page describing the design and its benefits.****

** **

However, you are right that if Typeable is always derived for all types, then maybe we can get away with no changes in those packages, which would be good.

Well, they will at least start throwing warnings, which means validate won't pass.

****

** **

7.8: Any uses of "deriving Typeable" would give rise to a warning saying that it is no longer necessary. Any instances of Typeable would give rise to a warning saying that this code is being ignored, and replaced by an internal Typeable instance. Packages might break, or change runtime behaviour due to this change.****

** **

Yes, that looks right. Actually I think it’s extremely unlikely that anything would break unless there is something Extremely Naughty happening. ****

** **

I say, go for it. Any objections? Would you be willing to do that Pedro? Thanks!

Yes, but you'll have to guide me a bit on how to internalise the Typeable instances... Cheers, Pedro

****

** **

Simon****

** **

*From:* josepedromagalhaes@gmail.com [mailto:josepedromagalhaes@gmail.com] *On Behalf Of *José Pedro Magalhães *Sent:* 29 October 2012 09:06 *To:* Gábor Lehel; Simon Peyton-Jones; libraries@haskell.org

*Subject:* Re: Changes to Typeable****

** **

Sorry, I got a bit lost in this discussion. Let me try to provide a summary.

Current status: I have a local branch with the new poly-kinded Typeable working fine. It works as described in [1]. It actually allows deriving Typeable for things involving the Constraint kind, but this can be easily disabled. Either way, I think most of this is necessary for whatever might follow next. But I'm not sure of how to push the changes, because I had to make some changes to these repos: array, containers, dph, template-haskell, and vector. Worse, I also had to change time, which gets built from a tarball. It might not be worth contacting the authors of these packages for changes if we're still going to get rid of "deriving Typeable" altogether, so I've been holding this back.

It's been proposed to remove the possibility to derive Typeable or write instances for it. I'm supposing the way that this would be implemented would be:

7.8: Any uses of "deriving Typeable" would give rise to a warning saying that it is no longer necessary. Any instances of Typeable would give rise to a warning saying that this code is being ignored, and replaced by an internal Typeable instance. Packages might break, or change runtime behaviour due to this change.

7.10: Explicit uses of "deriving Typeable" or instances are an error.

Regarding split :: (a ~ f i) => Dict (Typeable f, Typeable i), I'm not sure I can judge how much work that would be. But let's first try to draft a plan for removing Typeable definitions from the user, and then consider more extensions.

Cheers, Pedro

[1] http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/PolyTypeable****

On Tue, Oct 16, 2012 at 8:32 AM, Emil Axelsson wrote:* ***

2012-10-15 23:50, Gábor Lehel skrev:****

** **

On Mon, Oct 15, 2012 at 7:58 AM, Emil Axelsson wrote:** **

I have a use case:

http://hackage.haskell.org/packages/archive/syntactic/1.3/doc/html/Data-Dyna...

This is a reimplementation of Data.Dynamic to support casting type `a` to `Dynamic` given a constraint `Typeable (a -> b)`:

toDyn :: Typeable (a -> b) => P (a -> b) -> a -> Dynamic

With your suggestion, it seems I should be able to use the ordinary Data.Dynamic instead.

/ Emil****

Great! Do you like my plan? Or perhaps know of a better one?

(Relatedly, *does* this have to go through a separate libraries process? Or are we considering Typeable as getting completely replaced, and everything pertaining to it gets discussed here?)****

** **

Your plan certainly seems general enough! But I'm afraid I can't really speak about the implications on libraries etc.

/ Emil****

** **

_______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc

On Thu, Nov 1, 2012 at 8:28 AM, Christian Maeder wrote:

Am 29.10.2012 10:05, schrieb José Pedro Magalhães: [...]

It's been proposed to remove the possibility to derive Typeable or write

...

instances for it. I'm supposing the way that this would be implemented would be:

7.8: Any uses of "deriving Typeable" would give rise to a warning saying that it is no longer necessary. Any instances of Typeable would give rise to a warning saying that this code is being ignored, and replaced by an internal Typeable instance. Packages might break, or change runtime behaviour due to this change.

7.10: Explicit uses of "deriving Typeable" or instances are an error.

I would vote against making "deriving Typeable" an error as this would break a lot of existing code (and is recommended by current deprecation warnings).

Ignoring it (with or without warning) is the right thing to do (IMHO).

Furthermore there's a language flag DerivingTypeable, that should be ignored, too, then.

The flag is actually DeriveDataTypeable, and Data isn't changing, so that flag must stay (or be renamed to DeriveData...) Cheers, Pedro

Cheers Christian