Requiring generic instances (for higher-kinded type constructors) in instance context

283 Views Asked by At

I'm trying to create a flexible representation for an inductive datatype (that describes a version of the lambda calculus with datatypes and pattern matching). The flexibility here should mean that it is easy to add extra data on the nodes (free comonad-style) or to do substitution (free monad-style). So here's what I have:

type Tie f φ = φ (f φ)

type Id = String
type Var = Id
type Con = Id

data Pat φ = PVar Var
           | PCon Con [Tie Pat φ]
           | PWildcard

data Expr φ = EVar Var
            | ECon Con
            | EApp (Tie Expr φ)
            | ELam (Tie Pat φ) (Tie Expr φ)

The trouble comes when I want to derive the Show instance. Of course, I can do something like this:

{-# LANGUAGE FlexibleContexts, UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}

deriving instance (Show (φ (Pat φ))) => Show (Pat φ)
deriving instance (Show (φ (Expr φ)), Show (φ (Pat φ))) => Show (Expr φ)

but writing out the context by hand becomes unwieldy when the inductive structure becomes more complex.

Ideally, I'd like to be able to write something like

{-# LANGUAGE RankNTypes #-}
deriving instance (forall a. Show (φ a)) => Show (Expr φ)

to express that the functor φ should be, in some sense, "transparent" to the Show instance.

Is there a way to do something like that?

1

There are 1 best solutions below

0
On

A possible solution would involve

class Show1 f where
  showsPrec1 :: Show a => Int -> f a -> ShowS

This type class is similarly defined in prelude-extras. Unfortunately, Haskell's deriving mechanism would not take advantage of it, and could therefore not be used. A possible replacement may be using the new GHC.Generics and DefaultSignatures to create, though not "derived", at least trivial instances.

instance (Show1 φ) => Show (Pat φ)
instance (Show1 φ) => Show (Expr φ)

Now for the difficult part: actually using GHC.Generics. What could be used is

instance (Show1 f, Show a) => Show (f a) where showsPrec = showsPrec1

However, this has the extreme disadvantage of requiring OverlappingInstances (in addition to other problems). One possible solution is to define a class that is shadows Show.

class Show' a where showsPrec' ...
instance (Show1 f, Show' a) => Show' (f a) where ...

If all the GHC.Generics machinery was in place (GShow, GShow1, default signatures, etc.), then the end result would not look too horrible.

instance (Show1 φ) => Show' (Pat φ)
instance (Show1 φ) => Show (Pat φ) where showsPrec = showsPrec'
instance (Show1 φ) => Show' (Expr φ)
instance (Show1 φ) => Show (Expr φ) where showsPrec = showsPrec'

However, pretending that the amount of work required isn't that bad (it is pretty bad), some types would have to be manually set to forward from showsPrec' to showsPrec (Char, Bool, etc.), and all types used would have to be made instances of Show', which, though trivial if an instance of Generic or Generic1, is certainly not convenient.