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…
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…
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 :…
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…
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…
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…
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…
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…
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.
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…
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…
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 :…
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…
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…
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…
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…
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…
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.