record - 在 Idris 中限制记录类型

Question

我正在尝试在 Idris 中写入一条记录，但它有一个通用参数，需要受接口(interface)约束。对于普通联合类型我可以写:

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