Get Idris lazy?

[DAY]

Hi,

It is really nice to see the turn from Set to Type for the type of types.  So following that, how about change idris to use lazy evaluation?  Here are the reasons:

1. If I remember correctly, Martin-Löf's type theory features lazy evaluation.  I did not quite get and now also forget why he did that.  Maybe someone could fill in the reasons.

2. There is no dependently type language using lazy evaluation by default.  It means there is no dependently typed language that faithfully implements Martin-Löf's idea.  What a pity!

3. I know one reason against lazy evaluation maybe efficiency.  But does Haskell suffer from efficiency?  Then why would a dependently typed language do?

Best,

DAY

[Jason Dusek]

2012/12/13 DAY <plm...@gmail.com>:

Laziness is, in practice, a problem for predictability, even
when it is very efficient; and some of the benefits of laziness
are not realizable in total languages.

For example, we can define new "short circuit" operators in
Haskell and rely on undefined or looping terms not being
evaluated in certain contexts when using them; but when a
language is total, we needn't worry about these undefined,
looping terms!

--
Jason Dusek
pgp // solidsnack // C1EBC57DC55144F35460C8DF1FD4C6C1FED18A2B

[Michael Maloney]

The great thing about well-behaved total languages is they have the Church Rosser property. You can reduce the expression however you want, lazily or strictly, but all evaluation strategies converge on the same value.

In other words, as far as the theory goes, there is no need to choose lazy or strict. For all the theory is concerned with, "evaluation by random beta reduction" (full beta reduction) is a viable strategy.

What matters is deciding at what level do we decide evaluation strategy? If we bake it into our code with strictness or laziness annotations, our code becomes rigid and unadaptable. If it is left entirely up to the compiler, we had better have great faith in our compiler.

One possibility I'm personally interested in is evaluation strategy as a JIT optimization. I have dreams of my own language that is based on this principle. The idea is that you can run your code with the evaluation strategy completely unspecified on a special virtual machine. That virtual machine uses a training algorithm to heuristically assign a "pretty optimal" annotation (lazy or strict) to each function in your program. 

Laziness is useful. But laziness as the default..... I'd rather save that for Haskell :)

[Jason Dagit]

Thanks for the great answers. I suspect this question will come up again in the future so I've put your answers on the Unofficial FAQ so that we can point people there in the future: https://github.com/edwinb/Idris-dev/wiki/Unofficial-FAQ

I took some liberty editing your responses. Please review what I wrote and edit it as you see fit.

Jason

[Ben]

de-lurking here --

given that idris is pursuing a partial-evaluation / supercompilation strategy, does this mean that the standard objection to CBV (that is breaks functional modularity [1]) is not an issue? e.g. is

min = head . sort

still going to be O(n)?

best, ben

[1] - see "reuse" in http://augustss.blogspot.com/2011/05/more-points-for-lazy-evaluation-in.html

[Arthur Peters]

From what I understand part of the goal of Idris was the be total in general but still to allow partial functions when appropriate. So it does seem like there is a difference between evaluation strategies because there CAN be partial functions.

-Arthur