BTW, some time ago I had a conversation with Giuseppe Costanza, a prominent researcher in semantic type theory, and I posed the question to him: What does A=>B really mean? And he responded, “It means whatever you want it to mean, as long as you are consistent.”
Even if you have an AI that can code, how would you tell that AI what you want? Probably through some kind of programming language?
1 Like
Slides 265 - 274 of https://www.slideshare.net/pjschwarz/understanding-java-8-lambdas-and-streams-part-1-lambda-calculus-lambda-expressions-syntactic-sugar-first-class-functions complement/reinforce @MarkCLewis’ point that A => B compiles to Function1[A, B] (TIL “you can define SAM types using lambda syntax and they won’t be subtypes of FunctionXXX types” - thanks @tarsa)
https://www.slideshare.net/pjschwarz/definitions-of-functional-programming defines FP as the use of functions that are total, deterministic and pure, and so relates to your statement "For example, the following function returns Double on some given elements of type Int" in that your function is not total because it doesn’t return a value for certain inputs and it is impure because it sometimes has the side effect of throwing an exception.
https://www.slideshare.net/pjschwarz/functional-effects-part-1 shows how FP replaces the side effect of failure/exceptions with a functional effect, i.e. an abstraction returning which allows your functions to remain pure. It also links to @jducoeur’s point that “folks are thinking about how to express effects in Scala”.
1 Like
Right, but it doesn’t address the question of what a function is (represents) in terms of its input and output types. And what are the inhabitants of particular function types.
right
kind of related, i.e. may be of interest - From https://en.wikipedia.org/wiki/Curry–Howard_correspondence:
" a proof is a program, and the formula it proves is the type for the program . More informally, this can be seen as an analogy that states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem.
From https://www.youtube.com/watch?v=SknxggwRPzU
“if I want to convince you that if P is true then Q is true, the evidence for this is a function which, whenever I feed it evidence of P, spits out evidence of Q” https://www.youtube.com/watch?v=SknxggwRPzU
I can definitely see them being philosophical, but I think that the actual question is what is needed for “real” software, not what can be proven correct. What fraction of software can you write with for-each style repetition constructs and no infinite collections? (Implicitly you can’t have recursion in that question either.) If you only have finite iterations, the halting problem is solved as everything halts. I haven’t looked into it, but I’m guessing that subset of programs might also be completely provable. The question is whether it is sufficiently powerful to do what we need. That question almost certainly lacks a nice clean answer.
Exactly! Any sufficient specification tends to wind up being equivalent to the program. What interests me isn’t AI that codes, but development languages and tools that aid in proofs of correctness that go beyond standard type safety.
1 Like
Scala tries to guarantee sound type system, i.e. a system where you don’t have ClassCastExceptions unless you explicitly cast. Scala compiler gives warnings or errors about type safety breakage. Errors stops compilation so you can’t even run the program. Warnings still allow you to run your program but without the soundness guarantee.
As to exceptions - throw exception has type Nothing, but there’s no value of type Nothing so there’s nothing that can be returned from throw exception. What happens instead is Expressions | Scala 2.13 :
A throw expression throw 𝑒 evaluates the expression 𝑒. The type of this expression must conform to Throwable. If 𝑒 evaluates to an exception reference, evaluation is aborted with the thrown exception. If 𝑒 evaluates to null, evaluation is instead aborted with a NullPointerException. If there is an active try expression which handles the thrown exception, evaluation resumes with the handler; otherwise the thread executing the throw is aborted. The type of a throw expression is scala.Nothing.
Simplifying things a lot: throw is much closer to goto (with a thread local target) than to return.
3 Likes
The halting problem has much smaller teeth than what’s expressed here. Of course there are plenty of functions that are provably total, which a compiler could prove, and could prove trivially easy for a whole bunch of them.
That you can’t proof of all functions whether they’re total or not is no reason not to care about totality at all anymore.
A=>B in scala unfortunately doesn’t know about totality. Therefore, the best you can do is say that it’s a a construct that accepts values of type A, and if the function returns a value, that value is of type B if the implementation doesn’t use unsound features, but it could also not return any value at all, but instead run forever, exit the program, or throw an exception.
If you do use unsound features like throwing exceptions, or matching a type that’s not a class type in a type pattern, or use asInstanceOf, you’re on your own, and the compiler doesn’t make any promises anymore.
2 Likes
Why using speech, of course! Imagine a rubber duck that doesn’t only debug but also writes the code for you.
Because “what we need” is quite subjective 
To elaborate on that, exceptions can be seen as an alternative pattern for (some of the uses of) goto.
More so, I believe (but not completely sure) that in Scala, return from closures / anonymous functions os implemented via the NonLocalReturnControl exception:
def foo(nums: Seq[Int]): String = {
val evens: Seq[Int] = nums.map(i => if (i % 2 == 0) i else return "odd found")
s"all even sum is: ${evens.sum}"
}
The return type of the anonymous function that is given to map is Int. If an odd number is found, the return throws a NonLocalReturnControl wrapping the string “odd found”, which is then caught, unwrapped and (normally) returned by foo.