atennapel

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?

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.

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.

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

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.

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 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`.

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.

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

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

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))).

Maybe a pure logical programming language such as MiniKanren can be seen as non-linear? There you just read in all the rules you defined and (I think) it does not matter in which order you try to match the rules when you query the system.

Well some of his followers certainly thought that.

Because the all-powered creator will not stop the movie, which I guess shows the weakness of the god. So they have to act for him instead.