Косвенно ссылайтесь на определенные И неспецифические объекты в Haskell без монад

Я хочу хранить кучу элементов разных «видов» в структуре данных контейнера (список, набор,..) и косвенно ссылаться на них откуда-то еще. Обычно вы, вероятно, использовали бы тип суммы для элементов и, возможно, список в качестве контейнера или что-то подобное:

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

Теперь я хочу использовать (и сохранять) какие-то ссылки на элементы списка (например, используя индекс своей позиции в списке - давайте пока представим, что список не меняется, и что это хорошая идея) . Я хочу иметь возможность ссылаться на элементы, где меня не волнует "сортировка" И вот в чем загвоздка: я также хочу иметь возможность ссылаться на элементы и указывать тип, конкретный сорт. Это исключает приведенное выше решение типа простой суммы (потому что сортировка не в типе!). Я попробовал решение с помощью GADT:

{-#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"

Но это дает мне ошибку: - Недопустимый полиморфный тип: forall t. ElementRef (Element t) — GHC еще не поддерживает импредикативный полиморфизм — В объявлении синонима типа для «UnspecificElementRefs»

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

Как я могу это решить? Я не ищу решение этой конкретной ошибки (я думаю, это тупик?) или конкретно с GADT или даже с использованием индекса int для ссылки или что-то в этом роде, я просто хочу решение, которое:

  • решает основную проблему косвенной ссылки на что-то неспецифическое, а также на что-то конкретное
  • не использует STRef или подобное, поэтому вся моя программа должна быть монадой (поскольку это довольно центральная структура данных)

polymorphism haskell gadt
person Marius Melzer    schedule 11.07.2019    source источник

Ответы (1)


arrow_upward
4
arrow_downward

«Непредикативный полиморфизм» означает, что у вас есть ∀, заключенный в конструктор типа, отличный от ->. В этом случае в []. Как сообщается в сообщении об ошибке, GHC Haskell не поддерживает это (не то чтобы это в принципе неразумно, но, насколько я понимаю, это превращает проверку типов в настоящий кошмар).

Однако это можно решить, заключив ∀ во что-то, что образует «барьер проверки типов»: в новый тип.

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

На самом деле это можно упростить, поскольку ElementRef сама по себе является просто оболочкой нового типа с аргументом фантомного типа:

newtype UnspecificElementRef = UnspecificElementRef Int
person leftaroundabout    schedule 11.07.2019
comment
Хорошо, это решает проблему ссылки на неопределенный элемент, но как мне определить свой ElementList? Я пробовал с newtype ListElement = ListElement (forall t. Element t) и type ElementsList = [ListElement], но это не компилируется - person Marius Melzer; 11.07.2019
comment
Ага, нужен там экзистенциал, а не универсал. data ListElement where ListElement :: Element t -> ListElement. - person leftaroundabout; 11.07.2019