Деконструкция GADT: где я теряю контекст?

У меня есть этот тип и эти функции:

data Tag a where
    Tag :: (Show a, Eq a, Ord a, Storable a, Binary a) => a -> BL.ByteString -> Tag a

getVal :: Tag a -> a
getVal (Tag v _) = v

isBigger :: Tag a -> Tag a -> Bool
a `isBigger` b = (getVal a) > (getVal b)

Код не проверяет тип:

No instance for (Ord a)
  arising from a use of `>'
In the expression: (getVal a) > (getVal b)
In an equation for `isBigger':
    a isBigger b = (getVal a) > (getVal b)

 

Но я не могу понять, почему нет. Tag a имеет контекст (Show a, Eq a, Ord a, Storable a, Binary a), и getVal должен сохранить этот контекст. Я делаю это неправильно, или это ограничение расширения GADT?

Это работает:

isBigger :: Tag a -> Tag a -> Bool
(Tag a _) `isBigger` (Tag b _) = a > b

Изменить: я изменил пример на минимальный пример

Редактировать: Хорошо, почему это не проверяет тип?

isBigger :: Tag a -> Tag a -> Bool
isBigger ta tb =
    let (Tag a _) = ta
        (Tag b _) = tb
    in
        a > b

haskell gadt
person masonk    schedule 05.09.2013    source источник

Ответы (1)


arrow_upward
6
arrow_downward

Ваша подпись типа для getVal неверна, вам нужен тип

 getVal (Storable a, Ord a, ...) => Tag a -> a
 getVal (Tag v _) = v

Причина, по которой это не выводится, заключается в том, что вы можете делать такие вещи, как

 doh :: Tag a
 doh = undefined

Теперь, когда a не имеет никаких ограничений. Мы можем сделать что-то вроде

 getVal (doh :: Tag (IO Int)) == getVal (doh :: Tag (IO Int))

если бы у getVal были эти ограничения.

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

Чтобы ответить на новый вопрос

Когда вы деконструируете такие типы

 foo tag = let (Tag a _) = tag
               (Tag b _) = tag
           in a > b

GHC не объединяет их должным образом. Я подозреваю, что это связано с тем, что средство проверки типов уже приняло решение о типе a к тому времени, когда будет достигнуто соответствие шаблону, но при совпадении верхнего уровня оно будет правильно унифицировано.

 foo (Tag a _) (Tag b _) = a > b
person Daniel Gratzer    schedule 05.09.2013
comment
Еще раз спасибо джозе. Я не могу сказать, что понимаю, почему это проблема, потому что не везде проверяется нижний тип? Но пока достаточно знать, что просто нет, это невозможно по какой-то эзотерической причине теории категорий. - person masonk; 05.09.2013
comment
Просто можно создавать экземпляры Tag, у которых есть a, не ограниченный использованием undefined. Думайте о undefined как о секретном конструкторе любого типа, даже такого, который не может существовать без undefined. - person Daniel Gratzer; 05.09.2013
comment
Хорошо, еще одна трудность. Почему эта третья версия isBigger не проверяет тип? Он использует сопоставление с образцом! Здесь нет подлого undefined. - person masonk; 05.09.2013
comment
Изменить: ваше обновление, похоже, подразумевает, что ваша функция foo будет проверять тип. Но это не так. Как и мой выше. Я согласен с тем, что GHC должен знать, что a и b в этом третьем способе сопоставления с шаблоном определенно являются Ord, но это не так. - person masonk; 05.09.2013
comment
Нет, я могу ввести проверку моей функции foo - person Daniel Gratzer; 05.09.2013
comment
на версии GHC 7.6.2 - person Daniel Gratzer; 05.09.2013
comment
Ok. Виноват. foo выполняет проверку типов, а isBigger3 не выполняет проверку типов. Сопоставление с образцом должно быть выполнено на верхнем уровне, чтобы оно работало, по-видимому. - person masonk; 05.09.2013