новый тип с RankNTypes

Если я хочу объявить newtype таким образом, чтобы тип типа значения был ограничен экземпляром для класса типов, похоже, я могу сделать это с помощью:

{-# LANGUAGE RankNTypes #-}

newtype ShowBox = ShowBox (forall a. Show a => a)

GHC прекрасно компилирует это, но когда я пытаюсь использовать ShowBox с

ShowBox "hello"

Я получаю ошибку компилятора

<interactive>:1:18:
    Could not deduce (a ~ [Char])
    from the context (Show a)
      bound by a type expected by the context: Show a => a
      at <interactive>:1:10-24
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => a at <interactive>:1:10
    In the first argument of `ShowBox', namely `"hello"'
    In the expression: ShowBox "hello"
    In an equation for `a': a = ShowBox "hello"

Есть ли способ заставить это работать?


haskell newtype higher-rank-types
person purefn    schedule 19.03.2012    source источник
comment
Означает ли это количественное определение то, что вы думаете? Я и сам не уверен. Я думаю, что это может означать, что ShowBox можно применять только к значениям точного типа Show a => a. Мне очень интересно узнать, каков ответ на этот вопрос.   -  person Daniel Pratt    schedule 20.03.2012

Ответы (2)


arrow_upward
19
arrow_downward

Вы обещаете компилятору, что значение, которое вы поместите в ShowBox, будет иметь тип forall a. Show a => a. Есть только одно возможное значение с этим типом, и это _|_. Я думаю, вы, вероятно, хотите экзистенциальный тип, который выглядит довольно похоже, но означает что-то совсем другое.

{-# LANGUAGE ExistentialQuantification #-}

data ShowBox = forall a. Show a => ShowBox a

Это нужно сделать с помощью data, а не newtype. Сопоставление с образцом в конструкторе — это то, что в данном случае помещает экземпляр Show в область видимости. Поскольку newtype не имеют представления во время выполнения, у них нет места для хранения полиморфного свидетеля, который подразумевает экзистенциальная квантификация.

person Carl    schedule 19.03.2012
comment
То есть: значения, которые входят в ShowBox пользователя @user1279710, должны быть любым экземпляром Show, но он попытался поместить один конкретный экземпляр Show. (пауза для смены темы) В данном случае единственным значением типа forall a. Show a => a является _|_, потому что класс типов Show не включает никаких методов для создания значений типа экземпляра, а только для их использования. - person Daniel Wagner; 20.03.2012
comment
Было бы неплохо, если бы компилятор выдавал предупреждения типа бесполезного объявления данных: Show a => a: может обитать только _|_ - person Dan Burton; 20.03.2012
comment
Хорошо, это имеет смысл. Я надеялся, что есть какой-то способ сделать это без бокса, но вижу, что на самом деле это невозможно. Спасибо. - person purefn; 20.03.2012
comment
@purefn Бокс важен. В случае экзистенциальных типов с ограничениями класса бокс фактически сохраняет словарь класса во время выполнения. Это то, что необходимо для фактического использования класса, а не просто ограничение во время создания. - person Carl; 21.03.2012
comment
Имейте в виду, что этот ShowBox по сути такой же, как String. Во многих случаях экзистенциальные типы можно свести к более простым, конкретным типам; ищите эти возможности, они могут упростить вашу кодовую базу. - person luqui; 21.03.2012

arrow_upward
7
arrow_downward

Итак, ваш конструктор Show имеет такой тип:

Show :: (forall a. Show a => a) -> ShowBox

Вы пытаетесь применить эту функцию к типу [Char], который не относится к типу forall a. Show a => a, потому что a является "переменной Сколема", которая может быть унифицирована с другим типом только по очень строгим правилам (которые другие смогут объяснить лучше, чем я). могу).

Вы уверены, что следующее не то, что вам нужно (по модулю data против newtype)? Почему вы определили forall внутри конструктора?

-- Show :: Show a => a -> ShowBox
data ShowBox = forall a. Show a => Show a
person Luis Casillas    schedule 19.03.2012