다음 코드는 출신 유도 정의 형

Question

(https://stackoverflow.com/a/37461290/2129302)에 대한 구현 (쇼를) 찾기 :

mkStr : (Show a) => tensor shape a -> String 
mkStr x = show x 

하지만 그 대신이 :

tensor : Vect n Nat -> Type -> Type 
tensor []  a = a 
tensor (m :: ms) a = Vect m (tensor ms a) 

나는 다음과 같은 정의하고 싶습니다 다음과 같은 오류가 발생합니다 :

그러나, REPL에서 "show [some tensor value .. .] ". 왜 이것이 문제이며 해결하기 위해 무엇을 할 수 있습니까?

Answer 1

a을 표시하지 않으면 tensor shape a이 표시됩니다. 따라서 다음과 같이 작동해야하며 다음 형식으로 형식을 작성해야합니다.

mkStr : (Show (tensor shape a)) => tensor shape a -> String 
mkStr x = show x