DEV Community

Types as propositions, programs as proofs

DrBearhands on November 15, 2018

This post is part of a series called functional fundamentals. See the introduction and index. That's also where you can request specific topics No...
Collapse
 
rrampage profile image
Raunak Ramakrishnan

Great article. I have a doubt. You mentioned that the type checker for imperative programs can only give a guess as to whether the function will indeed return the correct type due to side effects in code. Is that also valid for languages with exceptions like Java and C#? Java for e.g also has product types and can have sum-types if you are willing to jump through some hoops (using inheritance). Java's Exceptions make the effective return into a sum type of (return or thrown exception). Won't similar inference laws apply except with the type changed to reflect possibility of exceptions?

For example:
f = p -> (q or e) where e is thrown exception simply becomes f = (p or e) -> (q or e)
and another function g = (q or e) -> (r or e) thus arguments for each function have a sum type of original arguments or error
"Composing" (altered to check for error and short-circuit) these will become:
g o f = (p or e) -> (q or e) -> (r or e)
In Java code we cannot ignore a checked exception, we have to handle it by catching or throw it and exit.

Is there something I am missing here?

Collapse
 
drbearhands profile image
DrBearhands

I'd like to first clarify a few things for other readers, you seem to be quite ahead of what I expected for my intended audience :-)

Sum-types are essentially disjunctions / enum types. If you have two types A and B, which can have respectively a and b number of values, their sum-type (disjunction / enum type / union) C can have a + b values, hence the name.

Similarly, product types (conjunction / tuples) can have a * b values because any combination of an A and a B is valid.


I am not intimately familiar with Java and C#, so they might have a "declarative mode" I just don't know about, in which case please do correct me. In my memories of Java, it was rather simple to cause an unhandled exception, e.g. ArrayOutOfBounds. But I will assume there is a 'safe mode' where you must handle all exceptions.

In this case, you are right in saying that exceptions are part of the type system and shouldn't be considered a side effect. If exceptions would have been the only side effect, that would make the language declarative! (You can look at SAC for an imperative looking but declarative language)

However, we still have hidden state in the form of static variables
and non-const, non-unique, references. That's essentially the p ∧ r → q example.

f = p -> (q or e) where e is thrown exception simply becomes f = (p or e) -> (q or e)

Now you're thinking with Monads :-)

Collapse
 
rrampage profile image
Raunak Ramakrishnan

In Java, there are checked exceptions and unchecked exceptions. Checked ones can be caught in the code, unchecked ones like the ArrayOutOfBounds result in a Runtime exception. Runtime exceptions do not have to be caught i.e code will compile fine if you ignore them. OTOH, checked exceptions have to be caught.

You are right in that I had not considered global variables. I was thinking that they can also be added to the type signature
f = ((p and s) or e) -> ((q and s) or e) where s is all state variables. But I can see that there is too much pollution occurring with these additions.

Regarding functional languages like Haskell, how do they handle fatal errors like machine getting out of memory or being sent a kill -9 signal? Is that also built into the type system?

Finally, is there any book you can recommend for getting better at Functional programming? I tried Learn You a Haskell but after 5 chapters I kind of never got back into it.

Now you're thinking with Monads :-)

I'll need to learn FP to understand what that means :)

Thread Thread
 
drbearhands profile image
DrBearhands

I was thinking that they can also be added to the type signature [...]

Sure! That's what you would do in declarative languages.

Regarding functional languages like Haskell, how do they handle fatal errors like machine getting out of memory or being sent a kill -9 signal? Is that also built into the type system?

The functional part of a program is just declarations, so it doesn't really 'run'. Because of this it can't run out of memory or be interrupted either. That all happens in the runtime, IO Monad, or similar imperative structure, which can indeed crash in the ways you mentioned.

If the entire system were purely functional it'd be a different story, but I'm not aware of such systems existing in reality.

I'll need to learn FP to understand what that means :)

You seem to have the right mindset to apply FP in practice. Learning the formal definition of a Monad can wait a bit. I have a post planned for it in the future.

is there any book you can recommend for getting better at Functional programming?

Unfortunately no, I personally don't learn well from books at all. Most of my uni books were left unopened.

Learning Elm can be a good starting point, see the guide and the beginners' slack channel

Haskell and Idris certainly have more features, but those very same features can get in the way of understanding the basics. Their type systems for instance use more than just propositional logic (another subject for the future).

Collapse
 
gypsydave5 profile image
David Wickes

interesting fact: humans get a lot better at logic when you formulate it as a cheater-detection problem

I laughed hard!

The compiler will check that your proof is correct (you have no compiler errors).

Do you need a compiler to do this, or can it be done with a separate program where no compiler exists for the language?

Collapse
 
drbearhands profile image
DrBearhands

There are proof checkers. I'm not familiar with them though. I believe Coq does something similar.

Could you do this for an interpreted language? Sure, but strongly typed, functionally pure languages are generally compiled. (if I'm not mistaken, you'd be losing out on a virtually free speedup by not compiling).

Collapse
 
8uurg profile image
8uurg

Agda and Coq are both languages that also forbid infinite loops and thus have type systems that allow you to prove logical statements (via the Curry-Howard correspondence) about your programs.

It is cool to know your program has certain properties for all inputs by proving it, but also very time consuming :)