伊德里斯热切的评价 [英] Idris eager evaluation

问题描述

在 Haskell 中，如果像这样，我可以实现：

旋转0 =（）
旋转n =旋转（n - 1）

这表现了我的期望：

 的Haskell>如果'真（旋转1000000）（） - 需要片刻
 haskell>如果'False（spin 1000000）（） -  immediate 
  

---

<

在 Racket 中，如果类似这样，我可以实现一个有缺陷的：

<$ p $ （定义（自旋n）（如果（= n 0）（void）（自旋（ - n 1）））（定义（if2 cond xy）（如果cond xy））
）


这表现了我的期望：

：

  racket> （if2 #t（旋转100000000）（void）） - 需要片刻
 racket> （if2 #f（spin 100000000）（void）） - 需要片刻
  

---

在 Idris 中，如果类似，我可以实现：



  if'：Bool  - > a  - > a  - >如果'True x y = x 
 if'False x y = y 
 spin：Nat  - > （）
 spin Z =（）
 spin（S n）= spin n 
  



< ：

如果'True（spin 1000）（） - 需要片刻
idris>如果'False（spin 1000）（） - immediate


我预计Irdis的行为与Racket类似，两个参数都是
评估的。但事实并非如此！

Idris如何决定何时评估事物？

我们认为Idris有严格的评估，但这是针对其运行时语义的。

作为完全依赖类型的语言，伊德里斯有两个阶段评估事情，编译时间和运行时间。在编译时，它只会评估它知道的全部内容（即终止并覆盖所有可能的输入），以便确保类型检查是可确定的。编译时评估器是Idris内核的一部分，并且在Haskell中使用HOAS（高阶抽象语法）样式表示值来实现。由于这里所有的东西都有一个正常的形式，所以评估策略实际上并不重要，因为无论哪种方式它都会得到相同的答案，并且在实践中，它将执行Haskell运行时系统选择执行的任何操作。

为方便起见，REPL使用编译时评估的概念。所以，你的'旋转1000'实际上从来没有得到评估。如果您使用相同的代码创建可执行文件，我期望看到完全不同的行为。

除了更易于实现（因为我们有评估程序可用）可以非常有用地展示条款如何在类型检查器中进行评估。所以你可以看到两者之间的区别：

  Idris> \\\
，m => （S n）+ m 
 \\\
 => \m => S（加n m）：Nat  - > Nat  - > Nat 
 
 Idris> \\\
，m => n +（S m）
 \\\
 => \m =>加上n（S m）：Nat  - > Nat  - > Nat 
  

如果我们在REPL上使用运行时评估，这将会更困难（虽然不是不可能） ，它不会在lambda下减少。

In Haskell, I might implement if like this:

if' True  x y = x
if' False x y = y
spin 0 = ()
spin n = spin (n - 1)

This behaves how I expect:

haskell> if' True  (spin 1000000) ()  -- takes a moment
haskell> if' False (spin 1000000) ()  -- immediate

---

In Racket, I could implement a flawed if like this:

(define (if2 cond x y) (if cond x y))
(define (spin n) (if (= n 0) (void) (spin (- n 1))))

This behaves how I expect:

racket> (if2 #t (spin 100000000) (void))  -- takes a moment
racket> (if2 #f (spin 100000000) (void))  -- takes a moment

---

In Idris, I might implement if like this:

if' : Bool -> a -> a -> a
if' True  x y = x
if' False x y = y
spin : Nat -> ()
spin Z = ()
spin (S n) = spin n

This behavior surprises me:

idris> if' True  (spin 1000) ()  -- takes a moment
idris> if' False (spin 1000) ()  -- immediate

I expected Irdis to behave like Racket, where both arguments are evaluated. But that's not the case!

How does Idris decide when to evaluate things?

解决方案

We say Idris has strict evaluation, but this is for its run-time semantics.

Being a fully dependently typed language, Idris has two phases where it evaluates things, compile-time and run-time. At compile-time it will only evaluate things which it knows to be total (i.e. terminating and covering all possible inputs) in order to keep type checking decidable. The compile-time evaluator is part of the Idris kernel, and is implemented in Haskell using a HOAS (higher order abstract syntax) style representation of values. Since everything is known to have a normal form here, the evaluation strategy doesn't actually matter because either way it will get the same answer, and in practice it will do whatever the Haskell run-time system chooses to do.

The REPL, for convenience, uses the compile-time notion of evaluation. So, your 'spin 1000' is never actually getting evaluated. If you make an executable with the same code, I would expect to see very different behaviour.

As well as being easier to implement (because we have the evaluator available) this can be very useful to show how terms evaluate in the type checker. So you can see the difference between:

Idris> \n, m => (S n) + m
\n => \m => S (plus n m) : Nat -> Nat -> Nat

Idris> \n, m => n + (S m)
\n => \m => plus n (S m) : Nat -> Nat -> Nat

This would be harder (though not impossible) if we used the run-time evaluation at the REPL, which doesn't reduce under lambdas.

这篇关于伊德里斯热切的评价的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！