伊德里斯的假设

Question

是否有关于postulate伊德里斯构造的性质和用途的最新信息？教程/手册中没有任何内容,我似乎也无法在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这样的东西,但是对于像机器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.