Частично прикладное семейство типов

Это дополнительный вопрос к этому вопросу, где ответ, частично применяющий оператор типа (~), допустимый.

Рассмотрим следующее (глупое) семейство типов:

type family SillyT a b :: Constraint

data D (c :: * -> Constraint) where
  D :: Proxy c -> D c

Тогда что-то вроде этого недействительно:

D (Proxy :: (Proxy (SillyT Int)))

Но если я оберну SillyT в такой класс:

class SillyT a b => SillyC a b
instance SillyT a b => SillyC a b

Тогда я могу сделать это:

D (Proxy :: (Proxy (SillyC Int)))

И все работает нормально. Однако обертывание в классе кажется немного глупым и повторяющимся, но единственный ли это способ частично применить семейство типов?


type-constraints haskell type-families
person Clinton    schedule 01.03.2017    source источник
comment
Может быть, я ошибаюсь, но, возможно, проблема в том, что вы выбираете вид ограничения для возвращения вашей семьи. Ограничения могут отображаться только в левой части =>.   -  person Rodrigo Ribeiro    schedule 01.03.2017
comment
Что еще может быть, кроме Constraint, если все экземпляры типа являются ограничениями? Например, сказать type instance SillyT Int a = Num a, чтобы привести глупый пример.   -  person Clinton    schedule 01.03.2017
comment
Извините за неправильное понимание вашего другого вопроса. Я думаю, что в этом более общем случае перенос классов, который вы делаете, является адекватным, и действительно, я довольно часто использовал один и тот же подход, чтобы иметь возможность обманом заставить GHC принять частично примененные ограничения. В некоторых случаях вы можете полностью обойтись без семейства типов, если у вас есть класс. Но не всегда.   -  person kosmikus    schedule 01.03.2017
comment
Следует отметить, что на самом деле это не позволяет вам «частично применить» ваше семейство типов — если у вас было instance SillyT Int a = Num a, то SillyC Int не сводится к Num. В этом операционное различие между семействами и конструкторами инъективных типов (т. е. data, newtype и class) — первые уменьшаются сразу, но не могут быть частично применены, а вторые уменьшаются только при полном применении, но «частичные применения» допустимы, но только в том смысле, что частичное приложение является синтаксически допустимым типом.   -  person user2407038    schedule 01.03.2017
comment
@ user2407038 Не совсем понимаю, почему вы говорите, что это не частичное приложение. Частично примененные функции также (в общем случае) не сокращаются, если вы не передадите достаточно много аргументов.   -  person kosmikus    schedule 02.03.2017

Ответы (1)


arrow_upward
-1
arrow_downward

Эти два определения, которые вы упомянули: type family SillyT a b :: Constraint и class ... => SillyC a b очень, очень отличаются с точки зрения средства проверки типов Haskell.

Если вы видите первое, единственное, что вы знаете, это то, что вы получаете Constraint после применения двух переменных типа, но вы не сообщаете GHC, что происходит после применения только одной. Вы должны быть в состоянии определить SillyT как type family SillyT a :: * -> Constraint, и тогда это скажет GHC гораздо больше.

Думайте об этом как о переменных конструктора. Если вы сообщаете GHC, что что-то является Functor, GHC знает, что его «форма» — это f a, где a — последний параметр некоторого f. Вы должны сказать GHC, что он может анализировать результат SillyT таким же образом, чтобы GHC мог быть уверен, что он всегда может получить доступ к последнему параметру, глядя на тип результата.

С другой стороны, классы типов здесь немного более выразительны. Они ЯВЛЯЮТСЯ типом, а не преобразованием типа (как семейства типов), и GHC может «сопоставлять шаблоны» для своих переменных, поэтому здесь вы не сталкиваетесь с вышеуказанным ограничением. Кроме того, классы типов позволяют определять перекрывающиеся экземпляры, что невозможно при использовании семейств типов. Однако функциональные зависимости менее гибки, чем семейства типов, потому что, если GHC не поддерживает непредикативные контексты, очень сложно избавиться от ненужных переменных свободного типа с помощью отложений типов.

Я надеюсь, что это проясняет некоторые вещи :)

person Wojciech Danilo    schedule 01.03.2017
comment
Я думаю, что да, но просто чтобы подтвердить, разумен ли мой подход или есть лучший способ? - person Clinton; 01.03.2017
comment
Вам не нужно создавать семейства типов и оборачивать их в классы таким образом, потому что это, как правило, не имеет смысла. Я мог бы рассказать вам больше, если бы вы рассказали о реальном сценарии использования. Иногда это может быть выгодно, но скорее как хак, чем правильное решение. Все зависит от варианта использования. - person Wojciech Danilo; 01.03.2017
comment
Я проголосовал против. Здесь много текста, но даже как эксперту по Haskell мне трудно понять, в чем разница, которую вы пытаетесь выделить, и почему это важно/было сделано именно так. Для некоторых конкретных примеров: единственное, что вы знаете [с семейством типов], это то, что вы получаете Constraint после применения двух переменных типа; что еще вы знаете о классе типов? Что вы пытаетесь проиллюстрировать своей Functor аналогией? Что такое сопоставление с образцом для переменных, почему это полезно для GHC, и от чего вы отказываетесь, разрешая это? - person Daniel Wagner; 01.03.2017
comment
Этот ответ неверен для нескольких учетных записей. 1. Классы типов НЕ ЯВЛЯЮТСЯ типами, это классы типов, как следует из названия. 2. Классы перекрывающихся типов эквивалентны семействам неинъективных типов: в классе перекрывающихся типов тип может совпадать с заголовками двух отдельных экземпляров класса типов одного и того же класса типов. 3. Под сопоставлением с образцом, я думаю, вы подразумеваете, что система типов пытается найти наиболее конкретный экземпляр класса типов в соответствии с алгоритмами, изложенными в спецификации и GHC, для перекрывающихся экземпляров. - person justinpc; 28.12.2019