在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扩展。