平等のタイプを比較するには？

Question

StringとStringを比較しようとしました.Trueと予想しています。

Idris> String == String 
Can't find implementation for Eq Type 

BoolにStringを比較する際それから私はFalseを期待。

Idris> String /= Bool 
Can't find implementation for Eq Type 

私にはimportがありませんか？

Answer 1

私たちがIdrisに持っているparametricityを壊すことはできません。タイプのパターンマッチングはできません。しかし、これは例えば、Eq実装を作成する必要がある。また

{- Doesn't work! 
eqNat : Type -> Bool 
eqNat Nat = True 
eqNat _ = False -} 

、一つは種類のパターンマッチ、それらが実行時に必要とされるであろうことができれば。現在、コンパイル時に型が消去されます。