ImpredicativeTypes & Existentials

#1

Here is the code where ImpredicativeTypes is enabled for a feature I am exploring:

{-# LANGUAGE ImpredicativeTypes #-}

data Fn a b = MkFn a b deriving Show

data AnyFn = forall a b. (Show a, Show b) => MkAnyFn (Fn a b)
instance Show AnyFn where show (MkAnyFn fn) = show fn

data AnyFn' = MkAnyFn' (forall a b. (Show a, Show b) => Fn a b)
-- This doesn't typecheck:
-- instance Show AnyFn' where show (MkAnyFn' fn) = show fn

-- This doesn't typecheck:
-- toAnyFns :: [forall a b. Fn a b] -> [AnyFn]
-- toAnyFns = fmap MkAnyFn

toAnyFns' :: [forall a b. (Show a, Show b) => Fn a b] -> [AnyFn']
toAnyFns' = fmap MkAnyFn'

  1. The AnyFn is a rather standard way of defining existential type (an alternative form is in GADT).

  2. The AnyFn' is rather different, it doesn’t require the ImpredicativeTypes extension, but I don’t know how to call it. And I can’t quite define a show instance for it:

impredicativetypes.hs:10:49: error: [GHC-39999]
    • Ambiguous type variable ‘a0’ arising from a use of ‘show’
      prevents the constraint ‘(Show a0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      Potentially matching instances:
        instance Show Ordering -- Defined in ‘GHC.Show’
        instance Show AnyFn -- Defined at impredicativetypes.hs:6:10
        ...plus 28 others
        ...plus 13 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: show fn
      In an equation for ‘show’: show (MkAnyFn' fn) = show fn
      In the instance declaration for ‘Show AnyFn'’
   |
10 | instance Show AnyFn' where show (MkAnyFn' fn) = show fn
   |                                                 ^^^^
  1. toAnyFns attempts to convert a list of Fn a b with impredicative a and b, but it fails to typecheck:
impredicativetypes.hs:14:12: error: [GHC-83865]
    • Couldn't match type: Fn a0 b0
                     with: forall a b. Fn a b
      Expected: [forall a b. Fn a b] -> [AnyFn]
        Actual: [Fn a0 b0] -> [AnyFn]
    • In the expression: fmap MkAnyFn
      In an equation for ‘toAnyFns’: toAnyFns = fmap MkAnyFn
   |
14 | toAnyFns = fmap MkAnyFn
  1. toAnyFns' though typechecks.

So how can I have toAnyFns' and also the Show instance?

Edit: Though I am ready to accept that maybe it is what impredicative types for, where the type information is simply “gone”. But I don’t have the right words and intuition to describe that yet.

#2

You can make the show instance work like this:

instance Show AnyFn' where 
  show (MkAnyFn' fn) = show (fn @() @())

Similarly, you can fix toAnyFns:

toAnyFns :: [forall a b. Fn a b] -> [AnyFn]
toAnyFns = fmap (\x -> MkAnyFn @() @() x)

(Aside: We need to eta-expand because the compiler needs a place to put the type applications for x, it will infer x @() @() here. With DeepSubsumption GHC will do that eta-expansion automatically, but it is not compatible with ImpredicativeTypes.)

That’s probably not what you expected.

AnyFn and AnyFn' are not very similar at all, they’re pretty much opposites in some sense.

The variables a and b are “hidden inside” MkAnyFn and anyone who matches on MkAnyFn must be prepared to receive an Fn a b for any possible a and b, but they can assume that the Show a and Show b hold.

On the other hand, MkAnyFn' contains a “function” that will create a Fn a b for any a and b you give it (such as () and () in the show instance I wrote above), but the types you give it must have show instances.

Essentially:

Quantification flavour Introduction (e.g. toAnyFns) Elimination (e.g. Show AnyFn)
Existential (e.g. AnyFn) Free Constrained
Universal (e.g. AnyFn’) Constrained Free

Where “Free” means “free to choose a and b (as long as they have show instances)” and “Constrained” means “must be able to deal with any a and b (but can assume show instances exist)”.

3 Likes
#3

Indeed not :slight_smile:

That’s surprising, do you mean MkAnyFn' itself being the function? In which case, isn’t MkAnyFn a function too?

–

But the explanation in type theoretical term makes lot sense now. Those are the right vocabulary I was looking for.

Is it then fair to say it is impossible to have a AnyFn variant works such that:

  • a toAnyFn to construct the list of AnyFn ergonomically from a list of Fn a b with impredicative a and b,
  • and somewhere else (not in the code example) using [AnyFn] can work with the original a b (Show instance is one example).

That left to me with the “vanilla” variant which is fine:

[ MkAnyFn fn1
, MkAnyFn fn2
, MkAnyFn fn3
] :: [AnyFn]

as opposed to an ergonomic version:

toAnyFns [ fn1, fn2, fn3 ] :: [AnyFn]

#4

What you’re looking for are first class existential types:

If Haskell had that, then you could write your desired function as follows:

newtype AnyFn = MkAnyFn (exists a b. (Show a, Show b) /\ Fn a b)
toAnyFns :: [exists a b. (Show a, Show b) /\ Fn a b] -> [AnyFn]

And you might not even need the AnyFn data type at all.

Also, the AnyFn type should be pretty much equivalent to your original AnyFn type that uses ExistentialQuantification, but I saw somewhere in the GHC proposal that these two features are not yet designed to work well together.

2 Likes