What is the relationship between static typing and lazy functional languages?

Question

I am curious about the relationship between static typing and lazy functional languages. For example, is it possible to have a dynamic lazy functional language? It seems that all the lazy functional languages ​​there are statically typed (Haskell, Miranda, etc.), and all dynamic functional languages ​​use strict evaluation (Clojure, Scheme, etc.).

In particular, a Wikipedia article on lazy pricing states:

However, lazy evaluation is difficult to combine with imperative functions, such as exception handling and I / O, because the order of operations becomes uncertain. Lazy appreciation can introduce cosmic leaks.

What is the role that static typing plays in preventing space leaks?

Answer 1

I do not think that static types play a role. For example, consider an untyped lazy language, Lazy Racket . I have not heard any indication that it is skipping space the way Haskell does (for example).

Side effects, on the other hand, are a problem because people find that the order of evaluation of a strict assessment is (relatively) natural, and the callsign is much more difficult to predict.

Answer 2

What is the role that static typing plays in preventing space leaks?

Types can be used to track the lifetime of objects, statically ensuring no leaks.

An example would be the types of regions and other types of effects.

Answer 3

Lazy evaluation and static typing are independent concepts.

• Untyped
  • lazy evaluation An untyped lambda calculus with a normal order reduction strategy (or a challenge if necessary). The leftmost redex is always handled first.
  • Expected (strict) assessment Calculus non-gaming lambda with a strategy to reduce the application order . Lambda terms are always abbreviated until they are replaced with other terms.
• typed
  • Haskell's lazy assessment is an example.
  • Simple Assessment Example OCaml.

---

Roughly speaking, evaluation is what happens when a program is launched. Text input is what happens when compiling a program.

But, of course, there is an important correspondence between the recruitment system and the evaluation strategy:

If the term M reduces to N and M: σ (M has type σ), then N: σ.

This means that when you start a program that has some type of σ, then the value will have the same type. Without this property, an input system is really useless (at least for programming). It also means that as soon as we typed during compilation, we don’t need to remember information about typing when evaluating, because we know that the result will be of the correct type.

---

Regarding the Wikipedia article you are citing. There are two different things:

• Imperative functions. This is not related to the typing system. The problem is that if evaluating some expressions has side effects (like I / O in most languages) in lazy settings, it is very difficult to predict when (if at all) a side effect occurs. Therefore, if you have a lazy assessment, it is hardly possible to have an unclean language.

  The one exception is Clean language . It uses a special type system to handle side effects in a lazy setting. Thus, there is some connection between the assessment strategy and the input system by processing side effects: the type system allows you to process side effects in such a way that we can conduct a lazy assessment.

• Leakage of space. This is a known disadvantage of lazy appreciation. See Creating Unvalued Expressions or Ch. 25 Profiling and optimization at Real World Haskell. But again, this has nothing to do with type systems - you get the same behavior in an untyped language.

Answer 4

I think that if you look at things from a more general level, you can observe the natural connection between static typing and lazy functional languages. The main point of static types is to inform and promote the compiler; exploring the static-dynamic separation between languages, it usually tracks the split between compiled and interpreted code.

And what is the meaning of lazy assessment?

The notorious retrospective article by Payton-Jones et al. Describes a lazy rating as a “hair shirt” that keeps the tongue purely functional. His metaphor aptly conveys the Haskell community to the deep-rooted idealism of denotational semantics. A non-standard assessment of the fundamental benefit lies in the fact that it transforms the possibilities of structuring code in ways that facilitate this denotational paradigm. In the notorious lazy debate assessment by Bob Harper and the Haskell community, Professor Harper demonstrates the problems that lazy assessments pose for practical programs - and among Lennart Augssson - protection against laziness, this best illustrates the point:

"I have kept my biggest problem of strict evaluation in recent times. A strict evaluation is fundamentally wrong for reusing a function. [...] With a strict evaluation, you can no longer tell people with a straight face: do not use recursion, reusing recursion patterns on a map, filter, foldr, etc. It just doesn’t work (in general). [...] a strict assessment really, fundamentally stops you from reusing functions as you can with laziness. "

And for an example of reusing a function using a lazy evaluation, Augustson suggests: "It is natural to express the function any by reusing the map and or functions." Such a lazy appraisal arises from this picture as a rather expensive linguistic function, encompassed in serving a more natural coding style.

What else do we need to maintain an abstract, denotational coding style? A powerful optimizing compiler can come in handy! Thus, even if there is no technical or necessary connection between static types and lazy evaluation, the two functions are oriented towards the same goal. Not surprisingly, they often appear together.