По-видимому, немного рассеянно, я написал что-то вроде следующее:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
class Foo f where
type Bar f :: *
retbar :: Bar f -> IO f
type Baz f = (Foo f, Eq f)
-- WithBar :: * -> (*->Constraint) -> * -> Constraint
type WithBar b c f = (c f, Bar f ~ b)
instance Foo () where
type Bar () = ()
retbar = return
naim :: WithBar () Baz u => IO u -- why can I do this?
naim = retbar ()
main = naim :: IO ()
Только после успешной компиляции я понял, что это не должно работать: Baz определяется как синоним типа с одним аргументом, но здесь я использую его без прямого аргумента. Обычно GHC лает на меня Type synonym ‘Baz’ should have 1 argument, but has been given none, когда я пытаюсь что-то вроде этого.
Теперь, не поймите меня неправильно: мне бы очень хотелось, чтобы я мог написать это, и достаточно легко увидеть, как он может работать в этом конкретном примере (просто вложение WithBar даст подпись naim :: (Foo u, Bar u ~ ()) => IO u, что, конечно, прекрасно), но я не понимаю, почему он действительно работает именно так. Возможно ли это только в ghc-7.8.2 ошибке?
Ваш файл компилируется в GHC 7.8, но в GHC 7.10 я получаю сообщение об ошибке:
Синоним типа "Baz должен иметь 1 аргумент, но ему ничего не дано
В сигнатуре типа для naim: naim:: WithBar() Baz u = > IO u
Добавление -XLiberalTypeSynonyms исправляет ошибку. Поэтому это ошибка в 7.8.
Я не знаю, что такое официальные правила, но для такого рода вещей кажется разумным работать на основе стратегии расширения синонимов с самым левым внешним видом. Единственное, что имеет значение, это то, что синонимы типов могут быть удалены в отдельной и завершающей фазе, прежде чем остальная процедура проверки типов произойдет. Я не знаю, предполагало ли это, что вы можете использовать частично применяемый синоним типа F в качестве аргумента для синонима G другого типа, до тех пор, пока G гарантирует, что F получит свои отсутствующие аргументы, но это, безусловно, согласуется с идеей, что синонимы типов являются неглубоким удобством.
Частичное приложение должно быть включено с помощью расширения LiberalTypeSynonyms.
В основном это откладывает проверку целостности синонимов типов до тех пор, пока они не будут расширены, поэтому ваше объяснение "вложения" по сути является правильной идеей.
Странная вещь здесь, однако, заключается в том, что это расширение не подразумевается тем, что в вашем модуле. Я просто тестировал, и частичное приложение вообще не работает с помощью только ConstraintKinds, TypeFamilies и PolyKinds. (Я добавил последнее, потому что виды проверяются перед расширением, а мои типы тестов вывели неверные в противном случае.)
Тем не менее, ваш файл загружается для меня в GHCi 7.8.3. Возможно, это какая-то ошибка, даже если есть расширение, чтобы сделать его должным образом законным.