Когда (если вообще когда-либо) можно вводить синонимы частично?

По-видимому, немного рассеянно, я написал что-то вроде следующее:

{-# 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 ошибке?

Ответ 1

Ваш файл компилируется в GHC 7.8, но в GHC 7.10 я получаю сообщение об ошибке:

Синоним типа "Baz должен иметь 1 аргумент, но ему ничего не дано

В сигнатуре типа для naim: naim:: WithBar() Baz u = > IO u

Добавление -XLiberalTypeSynonyms исправляет ошибку. Поэтому это ошибка в 7.8.

Ответ 2

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

Ответ 3

Частичное приложение должно быть включено с помощью расширения LiberalTypeSynonyms.

В основном это откладывает проверку целостности синонимов типов до тех пор, пока они не будут расширены, поэтому ваше объяснение "вложения" по сути является правильной идеей.

Странная вещь здесь, однако, заключается в том, что это расширение не подразумевается тем, что в вашем модуле. Я просто тестировал, и частичное приложение вообще не работает с помощью только ConstraintKinds, TypeFamilies и PolyKinds. (Я добавил последнее, потому что виды проверяются перед расширением, а мои типы тестов вывели неверные в противном случае.)

Тем не менее, ваш файл загружается для меня в GHCi 7.8.3. Возможно, это какая-то ошибка, даже если есть расширение, чтобы сделать его должным образом законным.