在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 Haskell擴展。