Блог

Главная - Вопросы по программированию - forall в подписи вида

forall в подписи вида

#haskell #dependent-type #data-kinds #singleton-type

#haskell #зависимый тип #типы данных #одноэлементный тип

Вопрос:

В singletons-2.6 Sigma определяется как

 data Sigma (s :: Type) :: (s ~> Type) -> Type

и GHC 8.8.4 сообщает, что его вид

 > :k Sigma
Sigma :: forall s -> (s ~> *) -> *

Так что же это forall такое в этой подписи вида?

По-видимому, это отличается от

 data Sigma :: forall s. Type -> (s ~> Type) -> Type

в этом случае его вид, конечно,

 Sigma :: * -> (s ~> *) -> *

Кроме того, это, похоже, отличается от

 data Sigma :: f s -> (s ~> *) -> *

Мне кажется, что расширенный вид переменной s типа в s :: Type унифицирован с переменной вида s в (s ~> Type) -> Type , но происходит ли это? У меня такое чувство, что я упускаю что-то очень простое.

Я пытался найти какие-либо документы, описывающие это, но мне не повезло.

Комментарии:

1. Я не уверен, но я предполагаю, что K :: forall s. F s -> T это означает, что K принимает один аргумент, и это s выводится из этого. Вместо K :: forall s -> F s -> T этого должно означать, что K принимает два аргумента и что значение первого должно совпадать с типом второго, аналогично тому, что происходит для зависимо типизированных функций на других языках.

Ответ №1:

Теперь я получил несколько идей от зависимого haskell в GHC Wiki.

Теперь мы можем передать вид конструктору типа точно так же, как мы можем передать тип конструктору данных (хотя нам все равно нужно передать синглтон вместо самого типа).

В этом объявлении Sigma ,

 data Sigma (s :: Type) :: (s ~> Type) -> Type

s in s :: Type — это переменная вида Type типа kind-kind, и этот вид должен быть передан явно при использовании Sigma . И в виде подписи,

 Sigma :: forall s -> (s ~> *) -> *

forall s означает s видимый вид. Это означает, что вам нужно передать его явно, когда вы говорите, что он виден. Вы можете прочитать это как Sigma конструктор типа, принимающий вид s и тип вида s ~> Type и возвращающий тип вида Type .

Вы не можете написать подпись этого типа непосредственно в GHC 8.8.4, но вы можете написать ее, используя StandaloneKindSignatures GHC 8.10.1.

Обновление (2021/9/30):

Это называется видимой зависимой количественной оценкой. Вы можете найти хорошее объяснение по этому поводу в Visible dependent quantification в Haskell.