idris - 如何在 idris 中对数据类型进行类型约束

Question

在 idris 中，如何约束 Algebraic Data Type 中的参数类型？

在haskell，我会这样做：

data Foo = Bar {x :: Integer, str :: String}

我可以在伊德里斯这样做吗？

Answer 1

有两种选择：数据类型

data Foo = Bar Int String

或记录

record Foo : Type where
  Bar : (x : Int) -> (str : String) -> Foo

两者都有一些限制：对于没有命名访问器的数据类型，对于记录，您只能有一个构造函数。

您可以在Idris 教程的第3.2 节数据类型和3.11 依赖记录中找到有关数据类型和记录的更多信息