What's the deal with Deno? We talk with a major contributor to find out. Listen now.

# Tag Info

4

The point of stacks is that they are in a sense the dual concept to computations. A computation does not run in a vacuum. It is always "surrounded" by some sort of an environment, or evaluation context, telling us what the current "state of progress" is, or is recording "where we are, and where we're going". Often this sort of information has stack-like ...

3

Since Andrej has somewhat covered the operational side, I'll take the more semantic/category theoretic perspective of why we care about stacks, that is especially relevant in EEC. The general philosophy of categorical logic is that all types should be defined by a universal property. In CBPV without stacks, you cannot give a universal property to the $F$ ...

2

Using Free, you can have a HOAS embedding of the untyped lambda calculus. And then write a structurally recursive function firing the top-level redex again and again. Good luck trying to normalise reduce omega. {-# NO_POSITIVITY_CHECK #-} data Free (f : Set → Set) (a : Set) : Set where Pure : a → Free f a Roll : f (Free f a) → Free f a data LAMF (T : ...

Only top voted, non community-wiki answers of a minimum length are eligible