Viewing profile — 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 =…

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 memor…

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…

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…

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 enc…

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 …

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 typ…

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 o…

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.