У меня есть следующее определение векторов фиксированной длины с использованием расширений ghcs GADTs
, TypeOperators
и DataKinds
:
data Vec n a where
T :: Vec VZero a
(:.) :: a -> Vec n a -> Vec (VSucc n) a
infixr 3 :.
data VNat = VZero | VSucc VNat -- ... promoting Kind VNat
type T1 = VSucc VZero
type T2 = VSucc T1
и следующее определение TypeOperator :+
:
type family (n::VNat) :+ (m::VNat) :: VNat
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)
Для всей моей интеллигентной библиотеки мне нужно применить векторную функцию фиксированной длины типа (Vec n b)->(Vec m b)
к внутренней части более длинного вектора Vec (n:+k) b
. Назовем эту функцию prefixApp
. Он должен иметь тип
prefixApp :: ((Vec n b)->(Vec m b)) -> (Vec (n:+k) b) -> (Vec (m:+k) b)
Здесь пример приложения с фиксированной длиной-вектор-функция change2
определяется следующим образом:
change2 :: Vec T2 a -> Vec T2 a
change2 (x :. y :. T) = (y :. x :. T)
prefixApp
должен иметь возможность применить change2
к префиксу любого вектора длины >= 2, например.
Vector> prefixApp change2 (1 :. 2 :. 3 :. 4:. T)
(2 :. 1 :. 3 :. 4 :. T)
Кто-нибудь знает, как реализовать prefixApp
?
(Проблема в том, что часть типа фиксированной длины-вектор-функции должна использоваться для захвата префикса нужного размера...)
Edit: Решение Daniel Wagners (очень умное!), Похоже, работало с некоторым кандидатом на выпуск ghc 7.6 (а не официальным релизом!). IMHO он не должен работать, однако, по двум причинам:
- Объявление типа для
prefixApp
не имеетVNum m
в контексте (дляprepend (f b)
для правильной проверки типа. - Еще более проблематично: ghc 7.4.2 не предполагает, что TypeOperator
:+
должен быть инъективным в своем первом аргументе (а не во втором, но это не существенно здесь), что приводит к ошибке типа: из декларации типа, мы знаем, чтоvec
должен иметь типVec (n:+k) a
, а тип-checker выводит выражениеsplit vec
в правой части определения типаVec (n:+k0) a
. Но: тип-checker не может сделать вывод, чтоk ~ k0
(поскольку нет уверенности, что:+
является инъективным).
Кто-нибудь знает решение этой второй проблемы? Как я могу объявить :+
инъективным в своем первом аргументе и/или как я могу вообще вообще не сталкиваться с этой проблемой?