idris - idris 公设

Question

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

Answer 1

我认为我们打算将 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 之类的东西，但是对于像 machine int 这样的操作在语言之外定义的东西呢？您需要证明 semigroupOpIsAssoc 给出的类型签名是有人居住的，但在语言中缺乏这样做的方法。因此，您可以假设存在这样的事情，作为告诉编译器“请相信我”的一种方式。

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

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

postulate foo : Unit

main : IO ()
main = print foo

仍然编译和运行(打印“()”)； Unit 的值 show 的实现实际上并不需要类型.