Quantified constraints for Show

[Icelandjack]

You can create a show instance for AST sym sig, if you if you say that forall sig. Show (sym sig).

That can be achieved by Show1 or ForallF Show:

instance ForallF Show dom => Show (AST dom sig) where
  showsPrec p = \case
    Sym s -> 
      showParen (p >= 11) (showString "Sym " . showsPrec 11 s) \\
        instF @Show @dom @sig 
    f :$ x -> 
      showParen (p >= 10) (showsPrec 10 f . showString " :$ " . showsPrec 10 x)

Now any symbol domain that has a show instance parametric in its semantic type can be shown, are there any benefits to doing it like this?

data NUM a where
  NUM :: Int 
      -> NUM (Full Int)
  ADD :: NUM (Int :-> Int :-> Full Int)
  MUL :: NUM (Int :-> Int :-> Full Int)
deriving instance Show (NUM a)

>>> Sym ADD
Sym ADD
>>> Sym ADD :$ Sym (NUM 1)
Sym ADD :$ Sym (NUM 1)
>>> Sym ADD :$ Sym (NUM 1) :$ Sym (NUM 2)
(Sym ADD :$ Sym (NUM 1)) :$ Sym (NUM 2)

[emilaxelsson]

Nice! Where is ForallF defined?

[Icelandjack]

It's defined in the constraints package (Data.Constraints.Forall) which is already a dependency of syntactic.

[Icelandjack]

Eq1, Show1, ... just got added to base in the GHC 8 release: to Data.Functor.Classes and they are very similar, compare

class Eq1 f where
    liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool

class Equality e where
    equal :: e a -> e b -> Bool

ForallF Eq would not allow comparing elements of different argument types, so I'm not sure how this all fits together to be honest (obviously Eq1 doesn't have a hash :: e a -> Hash method and Show1 doesn't have renderArgs) but I thought I'd mention it