Экзистенциальная квантификация без конструкторов данных

Легко получить экзистенциальную количественную оценку, упаковав словари в конструкторы данных.

{-# LANGUAGE GADTs #-}

data S where
  MkS :: Show a => a -> S

f :: Int -> S
f x = case x of
  0 -> MkS 0
  _ -> MkS "non-zero"

Соответствующий раздел в руководстве GHC прямо говорится о «экзистенциально количественных конструкторах данных». Можно ли написать тот же код, но без введения дополнительных типов данных и конструкторов, т.е. что-то с сигнатурой вида

f :: Int -> (exists a. Show a => a)
f x = case x of
  0 -> 0
  _ -> "non-zero"

Если нет, то есть ли документально подтвержденная причина существования этого ограничения? Избегать добавления нового квантификатора?


haskell existential-type
person typesanitizer    schedule 13.03.2019    source источник
comment
(exists a. Show a => a) всегда можно переписать как что-то вроде forall c. Show b => (forall a. Show a => a -> c) -> b -> c. Это похоже на связь в логике между экзистенциальной квантификацией и универсальной квантификацией.   -  person Colin Barrett    schedule 14.03.2019
comment
@ColinBarrett Вы действительно имели в виду, что там должны быть b, а не только, скажем, forall c. (forall a. Show a => a -> c) -> c?   -  person Daniel Wagner    schedule 14.03.2019

Ответы (1)


arrow_upward
4
arrow_downward

Заимствуя комментарий Колина и глядя на этот ответ, можно написать CPS-версию того же кода без exists квантификатор.

f' :: Int -> ((forall a. Show a => a -> r) -> r)
f' x = case x of
  0 -> \k -> k 0
  _ -> \k -> k "non-zero"

Хотя это и не идеально, но, безусловно, решает проблему без введения дополнительных типов данных.

person typesanitizer    schedule 13.03.2019