Sound typeable via type families?
Hello, Recently, someone (I forgot who, exactly) mentioned in #haskell this article: http://okmij.org/ftp/Haskell/types.html#unsound-typeable where Oleg demonstrates that Typeable makes the type system unsound, and one can get back unsafeCoerce (which is used in the implementation, I suspect). However, this evening, Ryan Ingram showed how to construct a safe Typeable using GADTs. The problem with that, of course, is that GADTs aren't open, so one can only have a predefined number of Typeables. However, it occurred to me that data families don't have that problem, so I took a shot and came up with the following: {-# LANGUAGE TypeFamilies, ScopedTypeVariables, GADTs , MultiParamTypeClasses, FlexibleInstances, OverlappingInstances #-} class Typeable t where data TypeRep t :: * typeRep :: TypeRep t instance Typeable Int where data TypeRep Int = TInt typeRep = TInt instance Typeable Integer where data TypeRep Integer = TInteger typeRep = TInteger instance Typeable () where data TypeRep () = TUnit typeRep = TUnit data TEq a b where Refl :: TEq a a class (Typeable a, Typeable b) => TEquality a b where teq :: TypeRep a -> TypeRep b -> Maybe (TEq a b) instance (Typeable a) => TEquality a a where teq _ _ = Just Refl instance (Typeable a, Typeable b) => TEquality a b where teq _ _ = Nothing cast :: forall a b. (TEquality a b) => a -> Maybe b cast a = do Refl <- teq ta tb return a where ta :: TypeRep a ta = typeRep tb :: TypeRep b tb = typeRep Which, somewhat to my surprise, actually works. And, of course, if one tries to pull off Oleg's trick: newtype Oleg a = Oleg { unOleg :: a } instance Typeable (Oleg a) where TypeRep (Oleg a) = ... typeRep = ?? Well, it won't work, because TypeRep () ~/~ TypeRep (Oleg a). However, obviously, this depends on overlapping instances (if there's some other way, I'd be happy to know; if type inequality contexts are available, I wasn't able to find them), and I've heard that type families don't play well with overlap. Does that not apply to data families? Will this construction still work in 6.10 and beyond? Also, this doesn't seem to be a suitable basis for Dynamic. Trying to extend the GADT solution presented resulted in errors unless incoherent instances were turned on (clearly not a good sign), and even then, it didn't actually work. Is it possible to do better, and come away with something that will actually work for Dynamic, and be sound? Is there some other trick waiting to pull unsafeCoerce out of this setup (seems doubtful, as it isn't used in the code, and the type families folks have no doubt done plenty of work to ensure soundness)? Comments appreciated. -- Dan
Am Freitag, 28. März 2008 05:21 schrieb Dan Doel:
[…]
However, obviously, this depends on overlapping instances (if there's some other way, I'd be happy to know; if type inequality contexts are available, I wasn't able to find them), and I've heard that type families don't play well with overlap. Does that not apply to data families? Will this construction still work in 6.10 and beyond?
Also, this doesn't seem to be a suitable basis for Dynamic. Trying to extend the GADT solution presented resulted in errors unless incoherent instances were turned on (clearly not a good sign), and even then, it didn't actually work. Is it possible to do better, and come away with something that will actually work for Dynamic, and be sound?
I don’t know exactly whether this helps here but with open type families you will be able to define a type-level type equality decision. See the mail at http://www.haskell.org/pipermail/glasgow-haskell-users/2007-October/013271.h....
[…]
Best wishes, Wolfgang
On 3/27/08, Dan Doel
class Typeable t where data TypeRep t :: * typeRep :: TypeRep t
This is a really interesting idea. Sadly, I can't think of a way to make it work. The biggest problem is the TEquality class; by putting teq in a typeclass, the decision of which teq to call (and thus, whether or not to return Just Refl or Nothing) is made at compile time. The GADT solution puts that decision off until run-time; the case statement in teq allows a decision to be made at that point. What we'd really like to do is something like the following: class Typeable t where data TypeRep t :: * typeRep :: TypeRep t typeEq :: forall t2. TypeRep t2 -> Maybe (TEq t t2) instance Typeable Int where data TypeRep Int = TInt typeRep = TInt typeEq rep = case rep of TInt -> Just Refl _ -> Nothing But you can't case analyze t2 in this way; each TypeRep is an independent data type and there's no way to determine which one you have (aside from some sort of typeable/dynamic constraint, and then we have a circular problem!) Perhaps there is a solution, but I'm not clever enough to find it. -- ryan
On Friday 28 March 2008, Ryan Ingram wrote:
This is a really interesting idea. Sadly, I can't think of a way to make it work.
The biggest problem is the TEquality class; by putting teq in a typeclass, the decision of which teq to call (and thus, whether or not to return Just Refl or Nothing) is made at compile time. The GADT solution puts that decision off until run-time; the case statement in teq allows a decision to be made at that point.
What we'd really like to do is something like the following:
class Typeable t where data TypeRep t :: * typeRep :: TypeRep t typeEq :: forall t2. TypeRep t2 -> Maybe (TEq t t2)
instance Typeable Int where data TypeRep Int = TInt typeRep = TInt typeEq rep = case rep of TInt -> Just Refl _ -> Nothing
But you can't case analyze t2 in this way; each TypeRep is an independent data type and there's no way to determine which one you have (aside from some sort of typeable/dynamic constraint, and then we have a circular problem!)
Perhaps there is a solution, but I'm not clever enough to find it.
Yes, I thought about it a while longer after sending my mail, and I can't see an immediate way of making things work. I imagine one would need some sort of open GADTs to do the job. Currently we have two things that look close; GADTs which can hold the necessary evidence, but are closed, and type families, which are open, but don't allow inspection of values to direct typing. I suppose I was initially fooled by doing things like: cast () :: Maybe () ==> Just () Which looks just like Data.Typeable. However, when one goes to write more generic functions: foo x = case cast x of Just i -> (show :: Int -> String) i Nothing -> "Whatever." The type of foo ends up as '(TEquality a Int) => a -> String', which makes it a bit more clear that we're dealing with compile-time phenomena. I'll probably think on it some more, but I'm not holding out much hope at this point. Thanks for your thoughts, though (and, to Wolfgang, for the pointer to the other discussion, although I don't know if that or any of the new type families stuff coming in 6.10 will be the solution). -- Dan
participants (3)
-
Dan Doel -
Ryan Ingram -
Wolfgang Jeltsch