λ Tony’s blog λ

Functional Java 3.0 is released. As usual, requires any Java 1.5 (or above) runtime and the source can be compiled with any Java 1.5 compiler.

Support for Java 7 BGGA closures is dropped, since the function interfaces are now classes with abstract methods. Other useful additions abound. Have fun!

Below are three exercises using Scala. The instructions for each are in the comments. Exercises 1 and 2 must be completed before Exercise 3 (which is just a thinking exercise — no code).

A follow-on to these exercises will be coming.

Hope this helps!

// A typical data type with a single abstract method
case class Inter[A](f: Int => A) {
  // which is a functor
  def map[B](g: A => B): Inter[B] =
    Inter(n => g(f(n)))
 
  // and a monad (see unital below)
  def flatMap[B](g: A => Inter[B]): Inter[B] = 
    Inter(n => g(f(n)).f(n))
}
 
// unital: A => F[A]
// Implementations for F=Option and F=Inter
object Unitals {
  def unitalOption[A](a: A): Option[A] =
    Some(a)
 
  def unitalInter[A](a: A): Inter[A] =
    Inter(_ => a)
}
 
// Exercises
// 
// It is recommended to use only map, flatMap and unital* for
// Option or Inter when implementing the exercises below.
// Any other libraries are acceptable (e.g. List functions).
object Sequencing {
  import Unitals._
 
  // Exercise 1 of 3
  // ===============
  // Implement a function that returns None if the given list
  // contains any None values, otherwise, all the Some values.
  def sequenceOption[A](x: List[Option[A]]): Option[List[A]] =     
    error("todo")
 
    // SOLUTIONx2 (ROT-13)
    /*
    1)
    k.sbyqEvtug(havgnyBcgvba(Avy: Yvfg[N]))((n, o) => n syngZnc (k => o znc (k :: _)))
 
    2)
    k zngpu {
      pnfr Avy  => havgnyBcgvba(Avy)
      pnfr u::g => u syngZnc (k => frdhraprBcgvba(g) znc (k :: _))
    }
    */
 
  // Exercise 2 of 3
  // ===============
  // Implement a function that returns an Inter that applies an Int
  // to all the Inter implementations in the List of Inters and returns
  // all the results.
  def sequenceInter[A](x: List[Inter[A]]): Inter[List[A]] =     
    error("todo")
 
    // SOLUTIONx2 (ROT-13)
    /*
    1)
    k.sbyqEvtug(havgnyVagre(Avy: Yvfg[N]))((n, o) => n syngZnc (k => o znc (k :: _)))
 
    2)
    k zngpu {
      pnfr Avy  => havgnyVagre(Avy)
      pnfr u::g => u syngZnc (k => frdhraprVagre(g) znc (k :: _))
    }
    */
 
  // Exercise 3 of 3
  // ===============
  // There is repetition in the above exercises.
  // How might we be rid of it?
  // That is for Part 2.
 
  def main(args: Array[String]) {
    def assertEquals[A](a1: A, a2: A) {
      if(a1 != a2)
        error("Assertion error. Expected: " + a1 + " Actual: " + a2)
    }
 
    def assertInterEquals[A](a1: Inter[A], a2: Inter[A]) {
      val testInts = List(1, 2, 0, -7, -9, 113, -2048)
      assertEquals(testInts.map(a1.f(_)), testInts.map(a2.f(_)))
    }
 
    // sequenceOption
    assertEquals(sequenceOption(List(Some(7),
        Some(8), Some(9))), Some(List(7, 8, 9)))
    assertEquals(sequenceOption(List(Some(7), None, Some(9))),
        None)
    assertEquals(sequenceOption(List()),
      Some(List()))
 
    // sequenceInter
    assertInterEquals(sequenceInter(List()),
      Inter(_ => List()))
    assertInterEquals(sequenceInter(List(Inter(1+),
        Inter(2*))), Inter(n => List(1+n, 2*n)))    
  } 
}

A loose follow-on from Java Trivia.

I run a weekly Haskell session at my place of employment. We are just beginning. The intention is not so much to learn Haskell, but to learn deeper programming concepts so that we can apply them regardless of language — though to the extent that various languages permit.

Recently, we were discussing algebraic data types and we invented our own:

data Optional a = Full a | Empty deriving (Eq, Show)

This is equivalent to:

• fj.data.Option for Java
• Data.Maybe for Haskell
• scala.Option for Scala
• option for F#
• module Option for OCaml
• Option for SML
• option for Coq

We were writing a function with this type

Optional a -> a -> a

when a member of the audience said, “Why not just use Optional a -> a?” to which I responded, “That’s not possible to do in a consistent way.” That is, not only we shouldn’t, but we cannot do it, no matter what! By consistent here, I mean a total, terminating function. Telling programmers that something is not possible is often a little hasty, even if it is true, so I side-stepped any further discussion on this matter and carried on, promising further explanation, which follows.

Here I will prove it is not possible by exploiting the Curry-Howard Isomorphism. It is not intended to be deep or technical, only to display some of the possibilities of using “types as propositions, programs as proof” — to paraphrase the intention of C-H Isomorphism.

The essence of C-H is quite simple. If you write a type signature, you have also written a logical proposition. If you find at least one function that satisfies this signature, you have proven that proposition. Conversely, if you have a program, its existence proves its type (whether the programming language explicitly supplies that type or not). This program for a type is called an inhabitant of the type. Some types are uninhabited, for example: a -> b. That’s because this proposition is not true.

To state it logically, forall a b. a implies b is a false statement. You can determine this by a simple truth table:

a b a->b
0 0 1
0 1 1
1 0 0 <-- inconsistency
1 1 1

In a previous post, I demonstrated a function that was once-inhabited using (a subset of — see the rules) Java. I knew it was once-inhabited before I gave the puzzle, meaning that every answer given should be the same (extensionally equivalent). Once-inhabited functions are very interesting, but not here — since we are looking for either:

• At least one inhabitant (proof which I have claimed does not exist)
• The absence of an inhabitant (proof negative)

So how can we prove or disprove Optional a -> a?

My claim is that it is uninhabited. You can disprove this claim by finding an inhabitant. However, the inability to find an inhabitant does not disprove the proposition — after all, we might just be having an unimaginative day! I am assuring you for now, that you will find no such inhabitant. Now I will prove that you won’t.

We first ask the question, what exactly is Optional a? We can provide a data structure of equivalence by exploiting the catamorphism for the data type:

type Optional a = forall x. (a -> x) -> x -> x

This data type is isomorphic (of the same one form) to our previous one and you can determine this by passing in the two constructors of the earlier data type to this isomorphic data type to produce an identity function:

let cata :: (a -> x) -> x -> x
cata Full Empty == id

Side note: if you’re interested in doing the same for a Haskell list, see the foldr function denoting the list catamorphism (foldr (:) [] == id).

Therefore, our proposition to prove/disprove is now rewritten (remember that -> is right-associative):

forall a x. ((a -> x) -> x -> x) -> a)

Using this, and the truth table for logical implication, we can find an answer by another truth table. Let us first assign some of the parts of this proposition to values for brevity (s being the proposition under investigation):

p = a -> x
q = x -> x
r = p -> q
s = r -> a

Let us now draw the truth table:

a x p q r s
0 0 1 1 1 0 <-- inconsistency
0 1 1 1 1 0 <-- inconsistency
1 0 0 1 1 1
1 1 1 1 1 1

We have now disproven the proposition Optional a -> a. It is not possible to inhabit this type signature consistently.

Further Reading:

• The Curry-Howard Correspondence
• The Curry-Howard Isomorphism with a crash course in formal logic

As always, I hope this helps!