Changes to Typeable

[Dan Burton]

Whoops, sending this to the whole list. Sorry for the duplication, Simon.

-- Dan Burton


---------- Forwarded message ----------
From: Dan Burton <danburton.email at gmail.com>
Date: Fri, Oct 5, 2012 at 11:57 AM
Subject: Re: Changes to Typeable
To: Simon Peyton-Jones <simonpj at microsoft.com>


I was alluding to what Brent Yorgey and others already said. If I annotate
a function with the type signature (a -> Int) then that function should
*not* have access to typeable operations on its input (because then we
would lose our precious free theorems).

If a function is not annotated, but uses typeable operations, then type
inference should indicate the corresponding Typeable constraints in the
inferred type. To steal Brent's example:

foo x = case typeOf x of
          Int  -> (3 :: Int)

          Char -> 4
          _    -> 5

This function (ignoring the monomorphism restriction) should be inferred to
have the type Typeable a => a -> Int

In short, from the language user's perspective, Typeable should still be a
regular old typeclass, that just happens to come with a distinct instance
for every type.

Another way to model the "danger" of accessing Typeable information is to
use a monad, and consider access to Typeable information to be an
"effect".[1] For backwards compatibility, I think it would be easier to
just stick with the typeclass.

[1] http://hpaste.org/75824

-- Dan Burton

Another, simpler alternative (if we don't want to use the Typeable
typeclass or the Monad idea) is to simply prefix "unsafe" to all of the
Typeable methods, and then quarentine them to a "contaminated" module as we
have done with unsafePerformIO.


On Fri, Oct 5, 2012 at 10:12 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

>  To take advantage of Typeable, though, the user should still have to
> annotate the necessary Typeable constraints.****
>
> ** **
>
> Can you say what you mean by this?  Perhaps with an example.****
>
> ** **
>
> Simon****
>
> ****
>
> *From:* Dan Burton [mailto:danburton.email at gmail.com]
> *Sent:* 05 October 2012 17:05
>
> *To:* Simon Peyton-Jones
> *Cc:* libraries at haskell.org
> *Subject:* Re: Changes to Typeable****
>
>  ** **
>
> 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-unsafe/
> ****
>
> ** **
>
> -- Dan Burton****
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20121005/8d9bc72e/attachment-0001.htm>