Constrained polymorphism of types

4
votes

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.

1
haskell
A list contains elements of the same type. Note that this would not work, since the show for String -> String is a different one then the show for Int -> String. So what would the type for show be at the left side of <$>? – Willem Van Onsem
the type would be forall a. Show a => [a] -> [String], i hoped that maybe with RankNTypes there could be a possibility to make it possible – Nicolas Heimann
You could use an existential type wrapper, but that would lead to [Wrapper] which is a complicated type isomorphic to the simpler [String]. This is a known anti-pattern. – chi

1 Answers

6
votes

[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]