Сравнить фиксированный размер векторов

Question

Я пытаюсь написать вектор фиксированного размера, как это:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators #-} 
import GHC.TypeLits 

data NVector (n :: Nat) a where 
    Nil :: NVector 0 a 
    Cons :: a -> NVector n a -> NVector (n + 1) a 

instance Eq a => Eq (NVector n a) where 
    Nil == Nil = True 
    (Cons x xs) == (Cons y ys) = x == y && xs == ys 

, но он не компилировать с этим сообщением:

Could not deduce (n2 ~ n1) 
from the context (Eq a) 
    bound by the instance declaration at prog.hs:8:10-33 
or from (n ~ (n1 + 1)) 
    bound by a pattern with constructor 
      Cons :: forall a (n :: Nat). a -> NVector n a -> NVector (n + 1) a, 
      in an equation for `==' 
    at prog.hs:10:6-14 
or from (n ~ (n2 + 1)) 
    bound by a pattern with constructor 
      Cons :: forall a (n :: Nat). a -> NVector n a -> NVector (n + 1) a, 
      in an equation for `==' 
    at prog.hs:10:21-29 

но если я представлю типа уровня натуралы вручную, он успешно компилируется

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies #-} 
data Nat = Z | S Nat 

infixl 6 :+ 

type family (n :: Nat) :+ (m :: Nat) :: Nat 
type instance Z  :+ m = m 
type instance (S n) :+ m = S (n :+ m) 

data NVector (n :: Nat) a where 
    Nil :: NVector Z a 
    Cons :: a -> NVector n a -> NVector (S n) a 

instance (Eq a) => Eq (NVector n a) where 
    Nil == Nil = True 
    (Cons x xs) == (Cons y ys) = x == y && xs == ys 

GHC версия 7.8.3

Answer 1

ghc не может (еще не?) Вывести тип равенства n ~ n' от (n+1) ~ (n'+1) , хотя он не имеет проблем с выводом его из S n ~ S n' См., Например, Append for type-level numbered lists with TypeLits для объяснения, и возможного выхода (т.е. иметь как Naturals Пеано стиль и все еще быть в состоянии использовать литералы как 5)

Но, если вы измените свое определение Nvector в

data NVector (n :: Nat) a where 
    Nil :: NVector 0 a 
    Cons :: a -> NVector (n -1) a -> NVector n a 

он должен будет вывести n-1 ~ n'-1 от n ~ n', намного проще вывести! Это компилирует и все еще дает правильный тип, например. Cons() Nil:

*Main> :t Cons() Nil 
Cons() Nil :: NVector 1() 

Обратите внимание, что это довольно бесполезно, так как мы не можем определить

append :: NVector n a -> NVector m a -> NVector (n + m) a -- won't work 

октября '14 status report для ghc говорит:

Явор Diatchki работает над использованием встроенный SMT-решатель в решателе ограничений GHC. В настоящее время основное внимание в этой области уделяется улучшенной поддержке рассуждений с натуральными номерами типового уровня [...]

, так что ваш пример может работать нормально с ghc 7.10 или 7.12!