Есть ли способ сделать этот тип семьи инъективным? - PullRequest
Новая
       7

Есть ли способ сделать этот тип семьи инъективным?

0 голосов
/ 10 ноября 2018

Следующее семейство типов 

type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) where  
  ListVariadic (a ': as) b = a -> ListVariadic as b
  ListVariadic '[]       b = b

явно не инъективен, например ListVariadic '[] (a -> a) ~ ListVariadic '[a] a.
Однако очень удобно иметь инъективность, чтобы помочь выводу типа, и я не собираюсь использовать ListVariadic с вторым аргументом, являющимся типом функции.
Я придумала два обходных пути, оба совершенно неудовлетворительные:

Вариант 1: Передача семейств типов, которые являются свидетелями левого обратного к ListVariadic (через классы типов). 

type family Arguments (f :: Type) :: [Type] where
  Arguments (a -> b) = a ': Arguments b
  Arguments b        = '[]
type family Return (f :: Type) :: Type where
  Return (a -> b) = Return b
  Return b        = b

class    ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
instance ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where

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

Вариант 2. Явно перечислите все нефункциональные типы, которые собираетесь использовать, в определении семейства типов переменных: 

type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) | f -> as b where  
  ListVariadic (a ': as) b = a -> ListVariadic as b
  ListVariadic '[] ()     = ()
  ListVariadic '[] Bool   = Bool
  ListVariadic '[] Word   = Word 
  ListVariadic '[] Int    = Int 
  ListVariadic '[] Float  = Float
  ListVariadic '[] Double = Double
  ... ... ...
  ListVariadic '[] (a,b) = (a,b)
  ListVariadic '[] (a,b,c) = (a,b,c)
  ... ... ...
  ListVariadic '[] [a] = [a]
  ... ... ...

Тогда аннотация приемистости возможна и работает как задумано. Очевидно, что он довольно ограничен ... и все же в итоге возникают ограничения вида a ~ ListVariadic '[] a, которые необходимо обойти.

Я надеялся, что найдется способ написать семейство типов ListVariadic (или что-то, выполняющее ту же цель), указывающее, что его второй аргумент не является функцией, и допускает аннотацию инъективности.
Я знаю, что у меня вдвойне неприятности, потому что в приведенном первом определении ListVariadic, второе уравнение имеет переменную голого типа с правой стороны. Обычно это не разрешается при проверке на инъективность ... но, возможно, есть некоторые хитрые приемы, использующие синонимы типов, которые могут обойти эту проблему?

...