如何在 idris 中对数据类型施加类型约束

Question

在 idris 中，如何限制代数数据类型中的参数类型？

在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 从属记录部分中找到有关数据类型和记录的更多信息