Idrisでレコードタイプを制限する

Question

Idrisにレコードを書き込もうとしていますが、これは汎用のパラメータを持ち、インターフェイスで制約を受ける必要があります。私は書くことができ、通常の労働組合・タイプの場合：

data BSTree : (a : Type) -> Type where 
    Empty : Ord a => BSTree a 
    Node : Ord a => BSTree a -> a -> BSTree a 

が、私はちょうどレコードと、同じことを行うための構文を把握しようとしています。私は次のようなものを試しました：

record Point a where 
    constructor MkPoint : Eq a => a -> a -> Point a 
    x : a 
    y : a 

コンパイルしません。

Idrisでこれを行う方法はありますか？

TIAは

Answer 1

あなたはこのようにそれを行うことができます。

record Point a where 
    constructor MkPoint 
    x : Eq a => a 
    y : Eq a => a 

けれども、実際にあなたがそれをしない必要があります。代わりに、いくつかのスマートコンストラクタを使用する方が良いでしょう。mkPoint : Eq a => a -> a -> MkPoint aのような他の関数です。 実際には、データ型のフィールドのタイプを制約する必要はありません。 -XDataTypeContextsハスケル拡張について読む。