У меня такое чувство, что я спрашиваю о невозможном, но здесь все идет.
Я хочу связать конструкторы типов с полностью примененной версией, которая нумерует параметры на уровне типа натуральными числами.Вот пример сеанса ghci с его желаемым использованием:
ghci> :kind! MKNumbered Maybe
MKNumbered Maybe :: *
= Maybe (Proxy Nat 1)
ghci> :kind! MKNumbered Either
MKNumbered Either :: *
= Either (Proxy Nat 1) (Proxy Nat 2)
Чтобы немного уменьшить шум вышеупомянутого, по сути, я получаю что-то вроде
Maybe >----> Maybe 1
Either >----> Either 1 2
Оказывается,Я могу быть достаточно близко со следующими типами семей.Они фактически используют дополнительный параметр, определяющий общее количество аргументов, но это нормально.
type MkNumbered f n = UnU (MkNumbered_ (U f) 1 n)
type family MkNumbered_ (f :: k) (i::Nat) (n::Nat) :: j where
MkNumbered_ (U f) i i = U (f (Proxy i))
MkNumbered_ (U f) i n = MkNumbered_ (U (f (Proxy i))) (i+1) n
data U (a::k)
type family UnU f :: * where
UnU (U f) = f
Тип U - это еще один прокси, который, по-видимому, необходим для получения желаемого поведения.Если у меня есть полностью примененный U, то есть U (a :: *), я могу развернуть его с помощью UnU.
Недостатком вышеизложенного является то, что, поскольку Proxy i :: *, MkNumbered может обрабатывать только конструкторы с * переменными.Нумерация
data A (f :: * -> *) a = ...
отсутствует, A (Proxy 1) (Proxy 2) не будет работать в аргументе Proxy 1.Я должен быть в состоянии улучшить MkNumbered, введя ряд конкретных прокси нумерации:
data NPxy1 (n :: Nat)
data NPxy2 (n :: Nat) (a :: i)
data NPxy3 (n :: Nat) (a :: i) (b :: j)
...
Это должно оставить меня с таким поведением:
ghci> :kind! MKNumbered A
MKNumbered A :: *
= A (NPxy2 Nat 1) (NPxy1 Nat 2)
Это очень помогает,только эти три определения NPxy, вероятно, охватывают большинство случаев более высокого порядка.Но мне было интересно, есть ли способ улучшить это, чтобы я мог охватить все k -> j -> ... -> * случаев?
Между прочим, я серьезно не надеюсь работать с такими типами, как
data B (b::Bool) = ...
Мне нужно что-то вроде этого незаконного определения:
data NPxyBool (n :: Nat) :: Bool
В любомВ этом случае все типы Bool уже заняты.Идя дальше, я был бы рад узнать, что есть способ создать некоторые данные
data UndefinedN (n :: Nat) :: forall k . k
, которые я назвал UndefinedN, поскольку на добром уровне это кажется дном.
Редактировать: Использование по назначению
Суть моего предполагаемого использования - запросить тип для параметра прокси.
type family GetN s (a :: k) :: k
GetN (Either Int Char) (Proxy 1) ~ Int
Однако мне также требуется, чтобыесли индекс прокси - это какой-то другой конкретный тип, кроме Proxy n, то этот тип просто возвращается.
GetN (Either Int Char) Maybe ~ Maybe
Однако любое решение семейства типов для Proxy n позволяет записывать экземпляры семейства для GetN с помощью Proxy n на лхс незаконно.Я открыт для решений на основе классов классов, где у нас может быть:
instance (Proxy n ~ pxy, GetNat s n ~ a) => GetN s pxy a where...
, но мое требование также разрешать конкретные значения для себя вызывает противоречивые определения экземпляров, которые у меня тоже возникают проблемы.
Остальное это просто для информации, но, имея вышеизложенное, я должен иметь возможность получать субданные из моих типов параметров прокси.Например, заполнив мое определение A, выше:
data A f a = A { unA :: f (Maybe a) }
субданных в unA, так как пронумерованные параметры выглядят так:
type UnANums = (Proxy 1) (Maybe (Proxy 2))
Я бы хотелполучить семейство типов (или некоторый другой метод), который создает конкретные суб-данные на основе примера супер-данных.
type family GetNs s (ns :: k) :: k
GetNs (A [] Int) UnANums ~ [Maybe Int]
GetNs (A (Either String) Char) UnANums ~ Either String (Maybe Char)
В конечном итоге это приводит к генерации сигнатур обхода в общем.Учитывая исходный и целевой контексты, например, A f a и A g b, в общем представлении я буду иметь в K1 типы узлов, такие как UnANums, из которых я могу получить источник и цель, к которой необходимо перейти.