Haskell's static type system is extremely flexible, but there are some limitations. For example, lists must hold exactly one type of element. Of course, you can get around this by creating a sum type to hold multiple types, but if you're writing a library, your sum type can't be extended by users. Another option in modern Haskell is to use a GADT to carry a type class dictionary and type around, but, again, this doesn't allow library users to define new type classes and instances.
Enter closed-world. Closed world is an extremely mischievous library that lets
you wrap up instance declarations into a Universe, a collection of instance
dictionaries and instance dictionary constructors. Then, as long as you have a
type with a Typeable instance, you can ask your Universe to see if it
contains a particular instance of that type, and, if so, to use that
constraint in an expression.
For example, Data.ClosedWorld defines the following type
data MyDynamic where
MyDynamic :: Typeable a => a -> MyDynamicNow, a list of type [MyDynamic] can contain any value, so long as it has a
Typeable instance. However, since I don't know the actual type of any of the
a, you can't do anything interesting with the values (other than call typeOf
on them)...
myList :: [MyDynamic]
myList = [ MyDynamic (1 :: Int)
, MyDynamic ("hello world" :: String)
, MyDynamic (("hello", 3) :: (String, Int))
, MyDynamic (("hello", "world") :: (String, String))
, MyDynamic (Nothing :: Maybe Int)
, MyDynamic (Just 34 :: Maybe Int)
, MyDynamic (Just ("hello, world", 4) :: Maybe (String, Int))
, MyDynamic ([1,2,3,4,5] :: [Int])
, MyDynamic (["hello", "world"] :: [String]) ]Now, suppose I wanted to show all the values in myList. I can't do this
normally, unless I add Show to the constraints of the MyDynamic constructor.
Actually, with closed-world you can! First, let's define a Universe, a
collection of Show instances. You'll need -XScopedTypeVariables and
-XTemplateHaskell.
import Data.ClosedWorld
showIntInstance :: Universe
showIntInstance = $(mkUniverse [d| instance Show Int |])This uses the template haskell mkUniverse function to generate the Universe
for us. This is your best bet, as the actual definition of the Universe value
makes heavy use of unsafeCoerce.
Now, we can fmap over the list, and convert each value to a string, if we know
how. You'll need -XTypeApplications
showMyDynamic :: Universe -> [MyDynamic] -> [Maybe String]
showMyDynamic u = fmap (\(MyDynamic (x :: a)) -> withHead @(Show a) u Nothing (Just $ show x))Now, if we run showMyDynamic showIntInstance myList in GHCi, we get
[Just "1",Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing]Awesome! Our Show Int instance was recovered at run-time! Let's add more show
instances. Let's do the one for Show String.
Er.. hold on. String ~ [Char] and Show [Char] isn't a valid Haskell 98
instance. The Show [Char] instance comes from a combinator of the Show Char
instance and the Show a => Show [a] instance.
We know how to do the Show Char instance.
showCharInstance :: Universe
showCharInstance = $(mkUniverse [d| instance Show Char |])Universes combine monoidally. Let's see what showMyDynamic says now.
*Data.ClosedWorld.TH Data.ClosedWorld Data.ClosedWorld.Base Data.ClosedWorld.TH> showMyDynamic (showIntInstance <> showCharInstance) myList
[Just "1",Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing]
Hmm... We need to add the instance for Show a => Show [a] to our universe too. Let's try that.
showListInstance :: Universe
showListInstance = $(mkUniverse [d| instance Show a => Show [a] |])Now, let's try combining all three.
*Data.ClosedWorld.TH Data.ClosedWorld Data.ClosedWorld.Base Data.ClosedWorld.TH> showMyDynamic (showIntInstance <> showCharInstance <> showListInstance) myList
[Just "1",Just "\"hello world\"",Nothing,Nothing,Nothing,Nothing,Nothing,Just "[1,2,3,4,5]",Just "[\"hello\",\"world\"]"]
Great! We recovered the Show String instance for "hello world". But hold on!
Notice that the Show instance for Show [Int] and Show [[Char]] was
recovered as well! Indeed, Universes can hold both explicit instance
dictionaries, as well as instructions on how to make those dictionaries.
There's still a few instances we don't have. Let's define Show (a, b) and
Show (Maybe a).
miscShowInstances :: Universe
miscShowInstances = $(mkUniverse [d|instance (Show a, Show b) => Show (a, b); instance Show a => Show (Maybe a) |])Now, everything can be shown.
*Data.ClosedWorld.TH Data.ClosedWorld Data.ClosedWorld.Base Data.ClosedWorld.TH> showMyDynamic (showIntInstance <> showCharInstance <> showListInstance) myList
[Just "1",Just "\"hello world\"",Nothing,Nothing,Nothing,Nothing,Nothing,Just "[1,2,3,4,5]",Just "[\"hello\",\"world\"]"]
*Data.ClosedWorld.Types Data.ClosedWorld Data.ClosedWorld.Base Data.ClosedWorld.TH Data.ClosedWorld.Types> map fromJust (showMyDynamic (showIntInstance <> showCharInstance <> showListInstance <> miscShowInstances ) myList)
["1","\"hello world\"","(\"hello\",3)","(\"hello\",\"world\")","Nothing","Just 34","Just (\"hello, world\",4)","[1,2,3,4,5]","[\"hello\",\"world\"]"]
Okay, one more trick! Let's find Ints in containers in myList. More
specifically, we want to use the Foldable f instance (if any) of our
MyDynamic types of form f Int, to recover all Ints in myList. Intuitively we want
foldMap (\(MyDynamic x) -> superMagicToListIfFoldable x) myList Let's write superMagicToListIfFoldable! Of course, our magic isn't really that
magical, so we'll have to compromise and parameterize our real function by a Universe.
import Data.Foldable
superMagicToListIfFoldable :: forall a r. (Typeable a, Typeable r) => Universe -> a -> [r]
superMagicToListIfFoldable u a = withHead1 (Proxy @Foldable) u a [] toListFirst, let's verify that the empty universe has no idea how to fold over
containers containing Ints.
*Data.ClosedWorld.TH Data.ClosedWorld Data.ClosedWorld.Base Data.ClosedWorld.TH Data.Typeable Data.Foldable> concatMap (\(MyDynamic x) -> superMagicToListIfFoldable mempty x) myList :: [Int]
[]
The Show Universe we defined also doesn't know what to do.
*Data.ClosedWorld.TH Data.ClosedWorld Data.ClosedWorld.Base Data.ClosedWorld.TH Data.Typeable Data.Foldable> concatMap (\(MyDynamic x) -> superMagicToListIfFoldable (showIntInstance <> showCharInstance <> showListInstance) x) myList :: [Int]
[]
Now, let's define some Foldable instances for our universe.
foldableInstances :: Universe
foldableInstances = $(mkUniverse [d| instance Foldable Maybe; instance Foldable []; instance Foldable ((,) a) |])These know what to do!
*Data.ClosedWorld.TH Data.ClosedWorld Data.ClosedWorld.Base Data.ClosedWorld.TH Data.Typeable Data.Foldable> concatMap (\(MyDynamic x) -> superMagicToListIfFoldable foldableInstances x) myList :: [Int]
[3,34,1,2,3,4,5]
We can also restrict ourselves only to lists.
foldableListInstance :: Universe
foldableListInstance = $(mkUniverse [d| instance Foldable [] |])Now, only the Ints in a list are returned.
*Data.ClosedWorld.TH Data.ClosedWorld Data.ClosedWorld.Base Data.ClosedWorld.TH Data.Typeable Data.Foldable> concatMap (\(MyDynamic x) -> superMagicToListIfFoldable foldableListInstance x) myList :: [Int]
[1,2,3,4,5]
Alright, that's it!
A lot of unsafeCoerce to make the constraint solver happy. I think it's mostly
type safe.
Currently, mkUniverse can't deal with instances whose instance heads contain
higher-kinded free variables. For example,
$(mkUniverse [d| instance Monad m => Monad (StateT s m) |])will likely not work.
The library can handle them internally, but you need to give explicit kind annotations and it's really messy. Pull requests welcome if you figure this one out!
No. This was mostly an exercise in using unsafeCoerce without segfaulting.
Honestly, I have no idea. I wrote it to see if I could, and it turns out I can. I'm not even sure this is type-safe, caveat emptor.