idrisの従属レコードのタイプコンストラクタに対するパラメータにインタフェース制約を設定できますか？ 私はインターフェイスShow : Type -> Typeを持っていると言います。今、私は、次の依存のレコードに制約を配置する必要があります。タイプコンストラクタパラメータのインタフェース制約を持つIdris依存レコード
record Source s where
constructor MkSource
initial : s
私はそれが常にShowのインスタンスでなければなりませんようにパラメータsに制約を配置する必要があります。これを達成する方法は？
イドリスは重い開発中であるが、イドリス・グループへのこの最近の電子メールによると、レコードの構文は、現在のインターフェイスを持つ制約タイプをサポートしていません：
https://groups.google.com/forum/#!topic/idris-lang/HMeTylslyFc
あなたが代わりにデータ型の構文を使用する必要があります、例えば
module Main
data Source: Type -> Type where
MkSource: Show s => s -> Source s
x: Source Int
x = MkSource 3
showSource: Source s -> String
showSource (MkSource x) = show $ x
testMe: (showSource $ Main.x = "3")
testMe = Refl
「常に「ショー」のインスタンス」とは、証人の「ss：ショーs」が存在する必要があることを意味しますか？はいの場合、 'Show s'タイプの' Source'に別のフィールドを追加するだけではどうですか？ – Cactus
'show'インターフェースの実際の定義をあなたの質問に含めてください（つまり、キーワード' interface'と 'where'を使用してください）。 –