CODEWITHSUNDEEP
haskellpolymorphismgadt
Marius Melzer
Marius Melzer

Reputation: 1064

Indirectly reference specific AND unspecific objects in Haskell without monads

I want to store a bunch of elements of different "sorts" in a container datastructure (list, set,..) and indirectly reference them from somewhere else. Normally, you would probably use a sum type for the elements and probably a list as container or similar:

data Element = Sort1 | Sort2 String | ...
type ElementList = List Element

Now I want to use (and save) some sort of references to the elements of the list (e.g. using an index to its position in the list - let's imagine for now that the list does not change and that this is thus a good idea). I want to to be able to reference elements where I don't care about the "sort" AND here's the catch: I also want to be able to reference elements and tell in the type that it's from some specific sort. This rules out the simple sum type solution above (because the sort is not in the type!). I tried a solution with GADTs:

{-#LANGUAGE GADTs, EmptyDataDecls, RankNTypes, ScopedTypeVariables #-}
data Sort1
data Sort2

data Element t where
  Sort1Element :: Element Sort1
  Sort2Element :: String -> Element Sort2

newtype ElementRef a = ElementRef Int

type UnspecificElementRefs = [forall t. ElementRef (Element t)]
type OneSpecificSort1ElementRef = ElementRef (Element Sort1)

main = do
  let unspecificElementRefs :: UnspecificElementRefs = [ElementRef 1, ElementRef 2]
  let oneSpecificElementRef :: OneSpecificSort1ElementRef = ElementRef 1
  putStrLn "hello"

But this gives me the error: - Illegal polymorphic type: forall t. ElementRef (Element t) - GHC doesn't yet support impredicative polymorphism - In the type synonym declaration for ‘UnspecificElementRefs’

   |
11 | type UnspecificElementRefs = [forall t. ElementRef (Element t)]
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

How can I solve this? I'm not looking for a solution to this specific error (I guess this is a dead end?) or specifically with GADTs or even using an int index for referencing or so, I simply want a solution which:

Upvotes: 2

Views: 81

Answers (1)

leftaroundabout
leftaroundabout

Reputation: 120711

“Impredicative polymorphism” means you have a ∀ that is wrapped in a type constructor other than ->. In this case, in []. As the error message tell you, GHC Haskell does not support this (it's not that it isn't in principle sensible, but as far as I understand it makes type checking quite a nightmare).

This can be solved though by wrapping the ∀ in something that forms a “type checker barrier”: in a newtype.

newtype UnspecificElementRef = UnspecificElementRef (∀ t. ElementRef (Element t))
type UnspecificElementRefs = [UnspecificElementRef]

In fact, this can be simplified seeing as ElementRef is itself just a newtype wrapper with a phantom type argument:

newtype UnspecificElementRef = UnspecificElementRef Int

Upvotes: 4

Related Questions