My guess is that they're setting up the wife being more in to the innie than the outie.

Which recursion scheme guarantees tail-recursion?

`cata` with a cps'd argument

Is the 18506 pages long lambda term the normal form? I wonder how much that can be minimized by not beta reducing everything.

No; the term has no normal form. It contains a lot of applications of the fix-point combinator Y. As a simpler example, here's a lambda term for reversing input:

    λ 1 ((λ 1 1) (λ λ λ λ 2 (4 4) (λ 1 4 2))) (λ λ 1)

which similarly has no normal form.

Ah yes, that makes sense. But is that PDF really the most minimal form? I can imagine if we write a program using lets:

  let nil = \n c. n;
  let cons = \hd tl n c. c hd tl;
  let map = ...;
  body

And compile it as:

  (\nil cons map. body) (\n c. n) (\hd tl n c. c hd tl) (...)

That we would get a more minimal form. But I cannot verify in what form the lambda expression in the PDF is. It just seems unbelievably large to me.

Yes, let bindings would get translated like that, but there would be some straightforward optimizations done, such as size-reducing beta-reductions, which strip out unused let bindings, and inline the single-use ones, as well as the multi-use ones whose definition is smaller than the unary encoded de-Bruijn index.

Yes, I wonder if these optimizations are done in the PDF. I found the BLC encoding of the lambda expressions which is 407171813 bits, about 5 mb.

I expect so, as the author is familiar with my tools [1] for doing these optimizations.

[1] https://github.com/tromp/AIT

Indeed he uses it here [1], which also gets used in lambda-8cc.

[1] https://github.com/woodrush/lambda-calculus-devkit

The page mentions that the implementation has 32 bit signed integers, plus it uses Scott encodings and not Church.

I'm not sure what you mean with totally expanded type space. But it sounds like Dhall has an issue with unfolding/normalisation.

Totality shouldn't have any special impact on memory usage as far as I know. It just restricts the kind of recursive functions and data types you can write.

If you have a sum type `< a : A | b : B | c : C >.a`, then A, B, and C need to be unfolded. If A itself is of type `< j : J | k : K | l : L >`, and J is also a sum type, etc., then unfolding everything can result in exponential memory usage and exhaust the amount of available memory. Of course there are ridiculously high-memory systems available, but then it's no longer economical.

I haven't written enough dependently typed programs to know what's best, but just an argument in favour of the OP version :): I agree that your version is easier to understand. But with the other version the types at least guide you in the implementation of the compress/uncompress. In your version you can return any `List t`.

For the sake of discussion I'm going to say something stronger than I believe, but which I don't think gets enough airtime so I want to expose its most extreme version. Having sufficient type direction such that there is only one possible implementation of a function is a bad thing. It represents a tightly constrained data type that will be painful to make even the smallest changes to down the road and duplicates code for no real benefit.

The definition of `RuntimeLength` does not do away with the need to define `uncompress`, all it does is move it into the definition of `RuntimeLength`. In fact my version of `RuntimeEncodedList` and `uncompress` is less overall code than `RuntimeLength` and `uncompress`. Indeed the only reason the compiler can synthesize `uncompress` is because it duplicates `RuntimeLength`! So really the compiler hasn't reduced the amount of work that needs to be done. Just like I could've messed up my definition of `uncompress`, its equivalent in `RuntimeLength` could also have been written incorrectly. We haven't reduced the amount of code that needs to be checked by a human for correctness (in the absence of other invariants), only moved it from a function definition to a data type definition.

By moving it into a function, however, we can then selectively add as many additional properties as we want (such as the `uncompress(compress xs) == xs` invariant), without having to worry about privileging one over any other.

Thank you for your comment, I haven't thought about it from this point of view before. What do you think about simpler datatypes like Vector? This can also be seen as a `List` with the constraint that `Vector n A = (l : List A) * length l = n`.

I personally balk even against sized vectors. It's too easy to accidentally find yourself writing out long proofs for arithmetic theorems that could easily be verified some other way (e.g. using a SAT solver). Although Idris 2 makes great strides here with zero multiplicity annotations on the vector lengths which makes bailing out a more feasible option.

Instead of

  append : Vector n a -> Vector m a -> Vector (n + m) a

I'd prefer just

  append : List a -> List a -> List a

and a separate theorem

  appendSumsLength : (xs : List a) -> (ys : List a) -> length (append xs ys) = length xs + length ys

Sure it's wordier in the short-term, but I think it pays dividends in longer term maintenance.

To be clear though this is a minority position. Other programmers will argue that putting the size parameter in the data type itself makes a lot of proofs essentially trivial and that at least in the case of sized vectors, the issue of "privileging a single invariant" is less of an issue, because the only defining feature of a polymorphic list is its length. I personally disagree with the merits of this trade-off for most production code, but that's starting to get into the weeds.

Your `Sum` is actually a `Pair` as well :). Should be: ``` Sum A B = (C : *) -> (A -> C) -> (B -> C) -> C ```

Note that in the calculus of constructions you can do these Church encodings of datatypes but you cannot derive an induction principle for these (only non-dependent folds). For example you cannot write a `snd` for the `Sigma` above.

As you allude to, you need a more expressive type system to derive induction principles (for example "Self types") for lambda encodings.

There's also effekt for Scala: https://github.com/b-studios/scala-effekt though it does not seem to be maintained.

Yes - I think we can conclude that these techniques are both too complicated and not ergonomic enough as of now. If that does not work in Scala, it will work even less in Kotlin (where many people go when they find Scala too complex).

I think something like algebraic effects can definitely be ergonomic and understandable, but a language definitely has to be designed for it. Algebraic effects are like exceptions in a lot of ways, so I think people will be able to understand them. See Effekt [1] and Koka [2] for languages that are designed with them in mind.

[1] https://effekt-lang.org/ [2] https://koka-lang.github.io/koka/doc/kokaspec.html

If your language has equality proofs, for example `a = Int` then, if your language is non-total I can prove anything by divergence. So I can prove `Int = String`. This is still type-safe as long as you don't erase the proof, because you can never use the invalid proof because your program will diverge.

So if you want to be type-safe but you still want to be able to erase proofs, your proofs have to be total.

Note that one combinator is enough: X = \x. x S K is turing complete! K = X (X (X X)) and S = X (X (X (X X))).