atennapel

4 ms·

1.
by atennapel 2y ago
My guess is that they're setting up the wife being more in to the innie than the outie.
2.
by atennapel 4y ago
Which recursion scheme guarantees tail-recursion?
3.
by atennapel 4y ago
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.
4.
by atennapel 4y ago
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 ma
5.
by atennapel 4y ago
Is the 18506 pages long lambda term the normal form? I wonder how much that can be minimized by not beta reducing everything.
6.
by atennapel 4y ago
The page mentions that the implementation has 32 bit signed integers, plus it uses Scott encodings and not Church.
7.
by atennapel 4y ago
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 t
8.
by atennapel 5y ago
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) * lengt
9.
by atennapel 5y ago
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 y
10.
by atennapel 5y ago
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
11.
by atennapel 6y ago
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 understa
12.
by atennapel 6y ago
There's also effekt for Scala: https://github.com/b-studios/scala-effekt though it does not seem to be maintained.
13.
by atennapel 6y ago
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 yo
14.
by atennapel 6y ago
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))).
15.
by atennapel 6y ago
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.
16.
by atennapel 7y ago
Well some of his followers certainly thought that.
17.
by atennapel 7y ago
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.