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