How to 'show' unshowable types?

Question

I am using data-reify and graphviz to transform an eDSL into a nice graphical representation, for introspection purposes.

As simple, contrived example, consider:

{-# LANGUAGE GADTs #-}

data Expr a where
  Constant :: a -> Expr a
  Map :: (other -> a) -> Expr a -> Expr a
  Apply :: Expr (other -> a) -> Expr a -> Expr a

instance Functor Expr where
  fmap fun val = Map fun val

instance Applicative Expr where
  fun_expr <*> data_expr = Apply fun_expr data_expr
  pure val = Constant val

-- And then some functions to optimize an Expr AST, evaluate Exprs, etc.

To make introspection nicer, I would like to print the values which are stored inside certain AST nodes of the DSL datatype. However, in general any a might be stored in Constant, even those that do not implement Show. This is not necessarily a problem since we can constrain the instance of Expr like so:

instance Show a => Show (Expr a) where
  ...

This is not what I want however: I would still like to be able to print Expr even if a is not Show-able, by printing some placeholder value (such as just its type and a message that it is unprintable) instead.

So we want to do one thing if we have an a implementing Show, and another if a particular a does not.

Furthermore, the DSL also has the constructors Map and Apply which are even more problematic. The constructor is existential in other, and thus we cannot assume anything about other, a or (other -> a). Adding constraints to the type of other to the Map resp. Apply constructors would break the implementation of Functor resp. Applicative which forwards to them.

But here also I'd like to print for the functions:

• a unique reference. This is always possible (even though it is not pretty as it requires unsafePerformIO) using System.Mem.StableName.
• Its type, if possible (one technique is to use show (typeOf fun), but it requires that fun is Typeable).

Again we reach the issue where we want to do one thing if we have an f implementing Typeable and another if f does not.

How to do this?

---

Extra disclaimer: The goal here is not to create 'correct' Show instances for types that do not support it. There is no aspiration to be able to Read them later, or that print a != print b implies a != b.

The goal is to print any datastructure in a 'nice for human introspection' way.

The part I am stuck at, is that I want to use one implementation if extra constraints are holding for a resp. (other -> a), but a 'default' one if these do not exist. Maybe type classes with FlexibleInstances, or maybe type families are needed here? I have not been able to figure it out (and maybe I am on the wrong track all together).

Answer 1

Great timing! Well-typed recently released a library which allows you to recover runtime information. They specifically have an example of showing arbitrary values. It's on github at https://github.com/well-typed/recover-rtti.

Answer 2

Not all problems have solutions. Not all constraint systems have a satisfying assignment.

So... relax the constraints. Store the data you need to make a sensible introspective function in your data structure, and use functions with type signatures like show, fmap, pure, and (<*>), but not exactly equal to them. If you need IO, use IO in your type signature. In short: free yourself from the expectation that your exceptional needs fit into the standard library.

To deal with things where you may either have an instance or not, store data saying whether you have an instance or not:

data InstanceOrNot c where
    Instance :: c => InstanceOrNot c
    Not :: InstanceOrNot c

(Perhaps a Constraint-kinded Either-alike, rather than Maybe-alike, would be more appropriate. I suspect as you start coding this you will discover what's needed.) Demand that clients that call notFmap and friends supply these as appropriate.

In the comments, I propose parameterizing your type by the constraints you demand, and giving a Functor instance for the no-constraints version. Here's a short example showing how that might look:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}

import Data.Kind

type family All cs a :: Constraint where
    All '[] a = ()
    All (c:cs) a = (c a, All cs a)

data Lol cs a where
    Leaf :: a -> Lol cs a
    Fmap :: All cs b => (a -> b) -> Lol cs a -> Lol cs b

instance Functor (Lol '[]) where
    fmap f (Leaf a) = Leaf (f a)
    fmap f (Fmap g garg) = Fmap (f . g) garg