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'
The AnyFn is a rather standard way of defining existential type (an alternative form is in GADT).
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
| ^^^^
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
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.
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)â.
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.