[Haskell-cafe] Sound typeable via type families?
Dan Doel
dan.doel at gmail.com
Fri Mar 28 00:21:11 EDT 2008
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
More information about the Haskell-Cafe
mailing list