2017-11-26 11 views
2

次のスニペットのための(番組の)実装を(https://stackoverflow.com/a/37461290/2129302)から検索された:帰納的定義型

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

私は次のように定義したいと思います:

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

しかし、その代わりに、この次のエラーが返されます。

Can't find implementation for Show (tensor shape a) 

ただし、REPLでは「show [some tensor value .. 。] "なぜこれがあり、それを修正するために何ができますか?

答えて

2

aが表示されていません。tensor shape aと表示されています。したがって、次のように動作し、次の方法で型を記述する必要があります。

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

これが本当である理由を明確にすることはできますか?確かに 'Show a'の実装があれば' Show(tensor shape a) 'もそうです。 'Vect'自体が' show'を提供します。 –

+0

@RoastedYam 'tensor'は依存型の関数です。 Idrisは、 'Show'制約を満たす' tensor'関数の結果に対して 'a'型の変数に対して' Show'制約があるかどうかを推測しようとしていません。また、 'shape'は型変数であり、特定の型ではないからです。それは 'Vect'ではない。 – Shersh

関連する問題