이드리스은 - 다음 I가 이드리스에서 N 차원 벡터를 정의

Question

막내 차원 벡터에 대해 작업을 매핑 :

import Data.Vect 

NDVect : (Num t) => (rank : Nat) -> (shape : Vect rank Nat) -> (t : Type) -> Type 
NDVect Z  []  t = t 
NDVect (S n) (x::xs) t = Vect x (NDVect n xs t) 

그러면 I는 텐서 모든 항목 f는 함수 매핑은 다음 함수를 정의.

iterateT : (f : t -> t') -> (v : NDVect r s t) -> NDVect r s t' 
iterateT {r = Z} {s = []} f v = f v 
iterateT {r = S n} {s = x::xs} f v = map (iterateT f) v 

그러나 나는 다음과 같은 기능에 iteratorT를 호출 할 때 :

scale : Num t => (c : t) -> (v : NDVect rank shape t) -> NDVect rank shape t 
scale c v = iterateT (*c) v 

내가 나를

When checking right hand side of scale with expected type 
     NDVect rank shape t 

When checking argument v to function Main.iterateT: 
     Type mismatch between 
       NDVect rank shape t (Type of v) 
     and 
       NDVect r s t (Expected type) 

     Specifically: 
       Type mismatch between 
         NDVect rank shape t 
       and 
         NDVect r s t    
     Specifically: 
       Type mismatch between 
         NDVect rank shape t 
       and 
         NDVect r s t 

에 꽤 좋은 것 같다 일치하지 않는 유형이,이 말을 다음과 같은 오류 메시지가

Answer 1

저는 또한 Idris에서 n 차원 벡터 (즉, 텐서)를 표현하는 방법을 궁금해했습니다. 다음과 같이

data NDVect : (rank : Nat) -> (shape : Vect rank Nat) -> Type -> Type where 
    NDVZ : (value : t) -> NDVect Z [] t 
    NDV : (values : Vect n (NDVect r s t)) -> NDVect (S r) (n::s) t 

그리고지도를 구현 : 다음

nmap : (t -> u) -> (NDVect r s t) -> NDVect r s u 
nmap f (NDVZ value) = NDVZ (f value) 
nmap f (NDV values) = NDV (map (nmap f) values) 

나는 문제의 유형 정의와 연극을했지만, 여러 가지 문제가 발생, 그래서 데이터 유형으로 NDVect 기능을 표현 이제 작동합니다 :

*Main> NDVZ 5 
NDVZ 5 : NDVect 0 [] Integer 
*Main> nmap (+4) (NDVZ 5) 
NDVZ 9 : NDVect 0 [] Integer 
*Main> NDV [NDVZ 1, NDVZ 2, NDVZ 3] 
NDV [NDVZ 1, NDVZ 2, NDVZ 3] : NDVect 1 [3] Integer 
*Main> nmap (+4) (NDV [NDVZ 1, NDVZ 2, NDVZ 3]) 
NDV [NDVZ 5, NDVZ 6, NDVZ 7] : NDVect 1 [3] Integer 

불행히도 모든 유형 생성자를 사용하면 상황이 다소 엉망이됩니다. 이 문제를 해결할 더 깨끗한 방법이 있는지 알고 싶습니다.

편집 : 여기

의 명시 적 유형의 텐서 순위를 인코딩하지 않는 약간 짧은 유형 서명 :

data NDVect : (shape : List Nat) -> Type -> Type where 
    NDVZ : (value : t) -> NDVect [] t 
    NDV : (values : Vect n (NDVect s t)) -> NDVect (n::s) t 

nmap : (t -> u) -> (NDVect s t) -> NDVect s u 
nmap f (NDVZ value) = NDVZ (f value) 
nmap f (NDV values) = NDV (map (nmap f) values)