는 크기 벡터

이 같은 고정 된 크기의 벡터를 쓰기 위해 노력하고있어 고정 비교는 크기 벡터

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

컴파일 0

출처

2015-01-22 Alexey Vagarenko

ghcn ~ n'을 에서에서 추론하는 데 문제가 없지만 (아직?) 유형 평등을 추론 할 수 없습니다. 설명하고, 밖으로 가능한 방법에 대한 Append for type-level numbered lists with TypeLits (즉, 두 페 아노 스타일의 원주민이 여전히 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

10 월 '14 ghc에 대한 status report는 말한다 :

Iavor Diatchki가 활용에 노력하고 있습니다 GHC의 구속 솔루션의 기성품 SMT 솔버. 현재이 유형의 주요 초점은 유형 수준의 자연수와 함께 추론에 대한 지원을 개선 한 것입니다. [...]

예를 들어 ghc 7.10 또는 7.12에서 정상적으로 작동 할 수 있습니다!

출처

2015-01-22 23:16:50

는 크기 벡터

답변

관련 문제