Список экзистенциально количественных значений в Haskell - PullRequest
Новая
       33

Список экзистенциально количественных значений в Haskell

4 голосов
/ 30 июня 2010

Мне интересно, почему этот кусок кода не проверяет тип: 

{-# LANGUAGE ScopedTypeVariables, Rank2Types, RankNTypes #-}
{-# OPTIONS -fglasgow-exts #-}

module Main where

foo :: [forall a. a]
foo = [1]

GHC жалуется: 

Could not deduce (Num a) from the context ()
  arising from the literal `1' at exist5.hs:7:7

Учитывая, что: 

Prelude> :t 1
1 :: (Num t) => t
Prelude>

кажется, что контекст (Num t) не может соответствовать контексту () аргумента arg.Я не могу понять, что поскольку () является более общим, чем (Num t), последнее должно включать и включение первого.Это как-то связано с отсутствием поддержки Haskell для подтипа?

Спасибо за любой комментарий по этому поводу.

Ответы [ 3 ]

12 голосов
/ 30 июня 2010

Вы не используете экзистенциальное количественное определение здесь. Вы используете типы ранга N.

Здесь [forall a. a] означает, что каждый элемент должен иметь каждый возможный тип (не любой, каждый). Так что [undefined, undefined] будет действительным списком этого типа, и это в основном все.

Чтобы немного расширить это: если список имеет тип [forall a. a], это означает, что все элементы имеют тип forall a. a. Это означает, что любая функция, которая принимает любой тип аргумента, может принять элемент этого списка в качестве аргумента. Это больше не верно, если вы вставляете элемент, который имеет более конкретный тип, чем forall a. a, поэтому вы не можете.

Чтобы получить список, который может содержать любой тип, вам нужно определить свой собственный тип списка с экзистенциальной квантификацией. Вот так: 

data MyList = Nil | forall a. Cons a MyList
foo :: MyList
foo = Cons 1 Nil

Конечно, если вы не ограничите типы элементов хотя бы экземпляром Show, вы ничего не сможете сделать со списком этого типа.

3 голосов
/ 30 июня 2010

Во-первых, ваш пример даже не зашёл так далеко от меня для текущего GHC, потому что вам также необходимо включить ImpredecativeTypes. Это приводит к предупреждению о том, что ImpredicativeTypes будут упрощены или удалены в следующем GHC. Так что мы не на хорошей территории. Тем не менее, добавление правильного ограничения Num (foo :: [forall a. Num a => a]) позволяет компилировать ваш пример.

Давайте оставим в стороне нецензурные типы и рассмотрим более простой пример: 

data Foo = Foo (forall a. a)
foo = Foo 1

Это также не компилируется с ошибкой Could not deduce (Num a) from the context ().

Почему? Ну, тип обещает, что вы дадите конструктору Foo что-то такое же качество, что для любого типа a, он выдаст a. Единственное, что удовлетворяет этому, это дно. С другой стороны, целочисленный литерал обещает, что для любого типа a класса Num он выдает a. Так что типы явно несовместимы. Тем не менее, мы можем потянуть за собой немного дальше, чтобы получить то, что вы, вероятно, хотите: 

data Foo = forall a. Foo a
foo = Foo 1

Итак, это компилируется. Но что мы можем с этим сделать? Что ж, давайте попробуем определить функцию экстрактора: 

unFoo (Foo x) = x

Oops! Quantified type variable 'a' escapes. Таким образом, мы можем определить это, но мы не можем сделать много интересного с этим. Если бы мы дали контекст класса, то мы могли бы по крайней мере использовать некоторые функции класса в нем.

Есть время и место для экзистенциалов, в том числе без контекста класса, но это довольно редко, особенно когда вы только начинаете. Когда вы в конечном итоге используете их, часто это происходит в контексте GADT, которые являются надмножеством экзистенциальных типов, но способ, которым возникают экзистенциалы, кажется вполне естественным.

2 голосов
/ 01 июля 2010

Поскольку объявление [forall a. a] (в смысле) эквивалентно высказыванию «У меня есть список, и если вы (то есть компьютер) выбираете тип, я гарантирую , что элементы указанногоlist будет такого типа. "

Компилятор, так сказать," вызывает ваш блеф ", говоря:" Я знаю ", что если вы дадите мне 1, то его типв классе Num, но вы сказали, что я могу выбрать для этого списка любой тип, который мне нужен. "

По сути, вы пытаетесь использовать значение универсального типа, как если бы это был типуниверсального значения.Это не одно и то же.

...