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

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

{-# 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, позволяющая это сделать?


haskell partial-application type-synonyms constraint-kinds
person leftaroundabout    schedule 05.04.2015    source источник
comment
Это поведение обеспечивается Синонимы LiberalType. В частности, если он включен, компилятор будет раскрывать все синонимы типов, прежде чем выполнять проверку синонимов частично примененных типов. Я предполагаю, что одно из TypeFamilies или ContraintKinds подразумевает LiberalTypeSynonyms.   -  person user2407038    schedule 06.04.2015
comment
@ user2407038 Как ни странно, они этого не подразумевают.   -  person Ørjan Johansen    schedule 06.04.2015

Ответы (3)


arrow_upward
9
arrow_downward

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

Синоним типа «Baz» должен иметь 1 аргумент, но не задан ни один

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

Добавление -XLiberalTypeSynonyms устраняет ошибку. Следовательно, это ошибка версии 7.8.

person sdcvvc    schedule 05.04.2015

arrow_upward
5
arrow_downward

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

По сути, это откладывает большую часть проверки согласованности синонимов типов до тех пор, пока они не будут расширены, поэтому ваше «встраивание» объяснения, по сути, является правильной идеей.

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

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

person Ørjan Johansen    schedule 05.04.2015

arrow_upward
4
arrow_downward

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

person pigworker    schedule 05.04.2015