Changes to Typeable

[Simon Peyton-Jones]

Crumbs, let's lay this ghost.  There is absolutely no danger (for GHC anyway) of making all types be Typeable without a visible constraint.  "seq" is bad enough (and arguably a mistake anyway).

My efficiency remark was solely about the type inference engine itself.  It has to answer the question "Is (Maybe (Tree Int)) a instance of Typeable?"  So it looks up in a big table to see, and finds an instance for (Typeable (a b)).  So now it needs (Typeable Maybe) and (Typeable (Tree Int)).  Off we go to the table to look for (Typeable Maybe).  But if *every* type constructor is in table, it'll be a big table, and we know the answer: yes, Maybe is an instance of Typeable, and its dictionary is called $dfTypeableMaybe.

That's all. I just hate looking things up when I know the answer.  But I only know the answer if *every* type is an instance.

So back to the Plan A vs Plan B discussion.

Simon

| -----Original Message-----
| From: libraries-bounces at haskell.org [mailto:libraries-
| bounces at haskell.org] On Behalf Of Brent Yorgey
| Sent: 03 October 2012 22:04
| To: libraries at haskell.org
| Subject: Re: Changes to Typeable
| 
| 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
| 
| _______________________________________________
| Libraries mailing list
| Libraries at haskell.org
| http://www.haskell.org/mailman/listinfo/libraries