Constrained polymorphism of types

user_2072459 0
Viewed 102

I try to define list of constrained polymorphic values, e.g.

myList = ["foo", 5] :: [Show a => a]

which yields the following error (GHCi, version 8.6.5)

GHC doesn't yet support impredicative polymorphism

Anyways, is it possible to specify a type such that, for example, functions of the form f :: Show a => [a] -> [String] could consume a constrained value like above?

In other words, is there a way to verify the following code by the compiler?

(++ "fork") . show <$> ["foo", 5]

I currently try to test a Show type class instance of a GADT by defining a dataset of values and expected results [(value, "expectedResult")]. But, due to the fact that GADTs constructors specify the values type, it is not possible to do this naively.

haskell
1 Answers

[Show a => a] does not mean what you think it does. It's a shorthand for [∀ a . Show a => a], i.e. a list of values each of which are polymorphic, not a polymorphic list containing concrete (but unknown) types. That would be an existential, [∃ a . Show a => a].

While Haskell doesn't come with anonymous existentials in type expressions, it is possible to obtain them as a declared type:

{-# LANGUAGE GADTs #-}

data Showable where
  Showable :: Show a => a -> Showable

myList :: [Showable]
myList = [Showable "foo", Showable 5]

Main*> map (\(Showable x) -> show x ++ "fork") myList 
["\"foo\"fork","5fork"]

however as chi already commented, there's no point to doing that: all you can possibly do with a Show-constrained existential is to, well, show it. I.e., all its information can be captured in a string. Well, then just store the string right away!

myList :: [String]
myList = [show "foo", show 5]
user_7459030
Related