13

postulate是否有关于Idris 中构造的性质和用途的最新信息？教程/手册中没有任何关于该主题的内容，我似乎也无法在 wiki 中找到任何内容。TIA。

4

1 回答 1

15

我认为我们将把 wiki 开发成更多此类事情的参考： https ://github.com/idris-lang/Idris-dev/wiki/Manual

的语法postulate是：

postulate identifier : type

如在

postulate n : Nat

或者

postulate whyNot : 5 = 6

它引入了该类型的未指定值。当您需要一个您不知道如何引入的类型的实例时，这可能很有用。假设您要实现需要证明的东西，例如这个 Semigroup 类型类需要证明该操作是关联的，以便将其视为有效的半群：

class Semigroup a where
  op : a -> a -> a
  semigroupOpIsAssoc : (x, y, z : a) -> op (op x y) z = op x (op y z)

这很容易证明像 Nats 和 Lists 这样的东西，但是对于像机器 int 这样在语言之外定义操作的东西呢？您需要证明 semigroupOpIsAssoc 给出的类型签名是有人居住的，但在语言中缺乏这样做的方法。所以你可以假设这样一个东西的存在，作为告诉编译器“相信我这个”的一种方式。

instance Semigroupz Int where
    op = (+)
    semigroupOpIsAssoc x y z = intAdditionIsAssoc
      where postulate intAdditionIsAssoc : (x + y) + z = x + (y +  z)

具有类似假设的程序仍然可以运行和使用，只要任何假设的“值”都不能从运行时值中获得（它们的值是什么？）。这对于相等术语来说很好，除了类型检查之外不会在任何地方使用，并且在运行时会被删除。一个例外是其值可以被删除的术语，例如单人Unit类型：

postulate foo : Unit

main : IO ()
main = print foo

仍然编译并运行（打印“（）”）；Unit的实现实际上并不需要该类型的值show。

于 2015-01-18T08:39:19.483 回答