Just who was Daedalus? It was the first of many questions the design team had to answer when we started work to find a logo for the digital wallet that will store the Ada cryptocurrency. Daedalus is an unusual name. We were in Riga, on an IOHK working sprint last autumn, when we got the brief to develop the visual identity and brand for the wallet, so the first thing we did was some research online.

It turns out that the name was chosen with good reason for a cryptocurrency wallet. An important figure in Greek mythology, Daedalus was the father of Icarus, a great artist, an innovator… as well as the creator of the labyrinth that kept the minotaur forever captive._

IOHK wants the wallet it is creating to be the best cryptocurrency wallet out there. Not just a place to store, send and receive cryptocurrency (the first of which it will hold is Ada) but a place where you can later access plug-ins and other developer tools/SDKs, anything from managing your mortgage to splitting a bill between people. The vision is that it will become a platform full of applications, and be as important a product as Internet Explorer was for Microsoft._

The creative team needed to find an identity that would connect to that vision, to the meaning behind the name Daedalus and his story, and to what IOHK is as a company and the technology it builds._

We got together to discuss it and an idea came out._

According to the myth, the minotaur never escapes the maze – that’s how good a craftsman Daedalus was._

We argue creatively that the minotaur is your money, or your digital identity. The minotaur is forever held in an infinite prison where only you control your keys. We have a lot of clever cryptography powering the security of the wallet, and like the minotaur in his maze, your money will never be able to escape our wallet, so Daedalus represents our expertise in security, and in building methodically and securely._

Tomas Vrana and Alexander Rukin, both part of the design team, came up with some early concepts. Among many different designs, Tom produced a minotaur; Alexander came up with a contemporary “D” design. They came up with creative sketches and drawings, trying to gauge how best to approach the form and the function of the logo. Some of their early designs are below.

Ribbon variant

Flat maze variant

Ribbon variant

Origami Minotaur variant

Gothic “D” variant

Minotaur variant

Then we threw open the design challenge to a competition, connecting to a community of designers to offer their solutions. This would provide us with a wealth of ideas and give us interesting feedback. We had about 100 entries from graphic designers, ranging from the bad, to the good, to the funny. There were solid corporate identities, also very creative executions. There were lots of designs based on the letter “D”. And lots based on keys (with a nod to public key cryptography). However, that was too obvious. We are a crypto wallet, yes we have keys. A simple key in a logo didn’t covey a strong brand message, it didn’t set us apart. None was quite right._

We were looking for something that would connect to the Daedalus story and have a huge potential for creative story telling in being a brand we could develop._

So we updated the brief and asked the designers to focus on the story of Daedalus. There were about 30 entries this time. A maze in the shape of a key was good, but not excellent. And there were lots of minotaurs. On some, the execution was not great. There was one that looked like a pixelated deer._

The one we finally chose, with the help of IOHK’s two founders, was by a designer called Zahidul Islam. It’s contemporary, it feels modern and fresh yet connects to a very old story. It has the minotaur. It’s a well crafted form, it’s balanced, and yet still has the maze motif in it – it reflects the identity of our brand._

There was one issue, it was quite complex, which meant it didn’t work at smaller sizes. So we worked with the designer to develop a brand hierarchy – which comprises a primary, secondary and tertiary form for the identity to be used in various situations as the rules dictate._Below are the primary, secondary and tertiary images, each with successively less complexity.

The primary logo will be the larger formats, for example to be used on T-shirts, or on main focal areas such as loading screens. (We have a plan to develop the identity, to make it a “living” brand that is dynamic, so you see it moving if you have to wait for the screen to load for instance.)

The secondary logo will be more of a symbol and used at smaller sizes. Some of the complexity has been removed, and it will be used if the requirements are for 64 pixels or smaller. And then we produced a tiny icon, to be used for example as a security feature on paper wallets.

The colours you see might change. The colour palette of the brand has only black and green in it now.

So why did we go to all this effort over five months?

Behind the Daedalus wallet is so much time, money, skill and effort. You wouldn’t want to represent all that hard work with a mark that is unconsidered, or one that lacks capacity to carry the story of Daedalus. You want to bring enigma, some creation to the symbol that represents your quest. This is about more than a platform, it is a brand and about building brand allegiance. It has to stand out, be different and make people think of you. This brand has a lot of runway, a lot of potential for development creatively. The design may change as the brand evolves, but the current identity will scale and develop into something wonderful from this point on._

Last Monday should have been particularly jarring given the recent excitement. However, it was anything but. Sunlight was flooding the back garden and all the small birds of the neighborhood came together to perform an impromptu concert at maximum volume. I could hear them clearly through the double glazing. Spring had sprung in Dublin. And I’d just come back from Malta talking Ethereum, Cardano, blockchain, crypto, functional languages, goal management and a ton of other cool stuff. Life is good.

It was my first time attending the Financial Cryptography and Data Security conference. The conference is a week-long annual event for cryptography as applied to finance. This year, IOHK's chief scientist Aggelos Kiayias put a great programme of speakers together. Instantly recognizable figures from the crypto community attended – Adam Back, Emin Gün Sirer, Vitalik Buterin and many more. IOHK researchers attended and it was great to see people who may only know each other through twitter feeds and published papers get to speak to each other.

I hope and presume this conference has generated many fine and detailed articles on Coindesk and beyond. This won't be one of them. Particular highlights for me were listening to MIT professor and cryptography pioneer Silvio Micali speak about the Algorand protocol and the conscious decision to keep incentives out of the equation. That instantly generated a little controversy and is going to need a long second look. 

Dmitry Meshkov, IOHK researcher, presented Improving Authenticated Dynamic Dictionaries, with Applications to Cryptocurrencies which is of particular interest to Team Grothendieck as we have wrestled with our implementation of the "Modified Merkle Patricia Trie" as specified in the original yellow paper. In all its forms it’s a clever idea – being able to move forward and back through the state by memorizing a root hash and being able to show tries are equivalent based on the equivalence of their root hashes. Dmitry et al have a scala implementation, and if I heard Vitalik Buterin correctly (he commented after the presentation) he suggested there might be room for improvement on the original implementation, so there are possibilities for enhancements there.

The conference was good, but it had some stiff competition from all the fun I had and everything I learned from mixing with other IOHK employees. IOHK employees usually work remotely but for more than a week almost 40 people gathered in Malta, who had traveled from far flung places like Osaka, St. Petersburg and California, including IOHK founders Jeremy Wood and Charles Hoskinson. While that week was mostly about the conference it was also an opportunity to get some work done. On the top floor of some very nice rented office space, the Serokell and Daedalus teams along with other key personnel on the Cardano project hammered out plans and approaches to give said project a major push forward. There was time for some introspection too and a lot of productive meetings around development methodology.  

A real highlight of working for this company is tripping across experts in many technical fields – functional languages, formal verification, full-time life time cryptographers, language designers and creators, high energy physicists... High energy physicists. Who tell jokes. 

And it gets better. The previous week, the week of the 27th of March, Team Grothendieck arrived in Athens to work on our next and arguably most important milestone – "Transaction Execution" or "tx execution" for short. This was the first time the whole team came together to work, physically together and in same time zone. 

The team reached its first milestone on Friday 24th March. That milestone involved downloading all blocks to the local machine and providing those blocks to other clients, further dispersing the transactions across the peer-to-peer network. The client also supports "fast download", which is the process of downloading the state trie from a point in recent history in order to shorten the time required for a client to get fully up to date with the blockchain. The premise being that downloading the state trie is faster than executing every transaction since block 0. As our first milestone it was very exciting to reach, but also to see the blocks and transactions flying around the network and know that we can successfully synchronize our local database with the rest of the Ethereum Classic network. 

We had a productive few days at the university of Athens, the area is quiet, cool in the shade and conducive to working. The sun shone, the wind blew and the coffee was good. Our hotel was close to the university so we got to walk the streets of Athens in the mornings and see a little of daily life in the city. The subject of our days in Athens (transaction execution) is the process of updating the ledger by applying valid transactions to it block by block. After each block of transactions has been applied to the ledger the ledger exhibits a new state. This state is stored in the form of a state trie and the root of this trie is a hash reflecting precisely the contents of the state trie. The questions we had to answer were – did we understand the goal; did we understand how we measure success; did we have the functionality covered by existing tasks; how long would it take and finally some knowledge swapping as working apart inevitably means small knowledge silos had begun to develop despite our efforts. By Thursday evening we had satisfactorily answered all these questions and we expect to reach the tx execution milestone by the end of April. 

On the Friday the team attended the Smart Contracts conference and spoke with Charles Hoskinson, Prof Aggelos Kiayias, Darryl McAdams and others about the future of smart contracts and the law.

There was tentative agreement on the eventuality of smart contract template libraries, so if for example the author wanted to provide an upgrade path for the contract in the event of some issue being found (ahem!) or have some means of dissolving/locking the contract if the participants lose faith, a tried and trusted set of templates would exist for the contract author to mix and match. Templates of this type could claim regulatory compliance out of the box, which is a great (if not new) way to leverage the usefulness of software in the world of contract law – solve a problem once and reuse the solution ad nauseam. I suspect this is an area most smart contract developers currently enjoy ignoring! 

A final word on Athens, the Acropolis museum  is a wonderful building and worth a visit even if they housed nothing there, but coupled with the treasures of the ancient world and a good restaurant it's a must-see if you find yourself in the area.

Here's hoping the end of April sees us reach another exciting milestone, an even bigger one this time, and we are able to execute every transaction in the blockchain using the Grothendieck client. That would really give the birds something to sing about... 

Experts in law and cryptography are speaking today at a smart contracts day in Athens, organised by IOHK chief scientist Aggelos Kiayias, chair of cyber security and privacy at the University of Edinburgh as well as director of its Blockchain Technology Laboratory. Smart contracts are an emerging technology that run on the same infrastructure that supports Bitcoin: a blockchain. They are digital legal contracts between parties that rely not on the traditional rule of law and institutions such as legal offices and courts, but on cryptography. Professor Aggelos Kiayias says: "To understand the technology it is useful to contrast cryptography and law. Law regulates interactions between persons ensuring fairness and basic rights. In this way, law offers protection from other persons with conflicting interests by relying on rule of law and social institutions. On the other hand, cryptography is the science of redistributing trust in any system that emerges from the interaction of multiple persons. It also protects people from other persons with conflicting interests but its protection is achieved by relying on hard mathematical problems."

So how do smart contracts work? Prof Kiayias again: "A smart contract is a piece of code written in a formal language that records all terms for a certain engagement. It has the power to self execute when certain conditions are triggered and can enforce its outcomes in a cryptographic sense. There is a multitude of smart contract applications in areas such as intellectual property, financial instruments, rental and leasing agreements and others."

Also speaking at the conference are Charles Hoskinson, IOHK CEO and Co-Founder; Burkard Schafer, Professor of Computational Legal Theory and director of the SCRIPT Centre for IT and IP law at the University of Edinburgh; Peter Van Valkenburgh, Director of Research at Coin Center; and Christoph Sorge, holder of the juris professorship of legal informatics, co-director of the Institute for Law and Informatics, and member of the Center for IT Security, Privacy and Accountability at Saarland University.

Darryl McAdams, IOHK's Team Plutus manager is working on a new programming language for smart contracts (Plutus) and is in Athens for the conference. According to Darryl, "A smart contract is a program which can implement an agreement of one form or another between multiple parties. They can be simple transfers of money, contracts in the traditional sense involving rights and obligations of various parties, or things more complex such as a game of chess, a distributed library, or a decentralized DNS system. In all of these cases, the purpose and behaviour of the system needs to be well understood, and in many cases, such as financial contracts with large sums of money involved, the correctness of the program is absolutely vital. In my talk, I will discuss the design of the Plutus language, a new programming language for authoring smart contracts, and demonstrate its use. I'll also discuss the motivation behind its design, especially with a view towards correct implementation of a contract's purpose and behaviour."

The event – "Smart Contracts Day, Cryptography & Law: Information, Privacy and Smart Contracts" – is taking place at the Hotel Divani Caravel, in central Athens. It is highly anticipated and currently sold out with more than 200 participants. Here’s more information: law.bitcoinschool.gr

Prof Kiayias concludes: "In the near future, this technology will give rise to "cryptolegal" frameworks, that, by merging cryptography and law, will be able to regulate interactions of persons at a global scale. In this way, such frameworks will transcend geographic and jurisdictional boundaries and create a dynamic global social institution that belongs to all and can be abused by none."

Experts in law and cryptography are speaking today at a smart contracts day in Athens, organised by IOHK chief scientist Aggelos Kiayias, chair of cyber security and privacy at the University of Edinburgh as well as director of its Blockchain Technology Laboratory. Smart contracts are an emerging technology that run on the same infrastructure that supports Bitcoin: a blockchain. They are digital legal contracts between parties that rely not on the traditional rule of law and institutions such as legal offices and courts, but on cryptography. Professor Aggelos Kiayias says: "To understand the technology it is useful to contrast cryptography and law. Law regulates interactions between persons ensuring fairness and basic rights. In this way, law offers protection from other persons with conflicting interests by relying on rule of law and social institutions. On the other hand, cryptography is the science of redistributing trust in any system that emerges from the interaction of multiple persons. It also protects people from other persons with conflicting interests but its protection is achieved by relying on hard mathematical problems."

So how do smart contracts work? Prof Kiayias again: "A smart contract is a piece of code written in a formal language that records all terms for a certain engagement. It has the power to self execute when certain conditions are triggered and can enforce its outcomes in a cryptographic sense. There is a multitude of smart contract applications in areas such as intellectual property, financial instruments, rental and leasing agreements and others."

Also speaking at the conference are Charles Hoskinson, IOHK CEO and Co-Founder; Burkard Schafer, Professor of Computational Legal Theory and director of the SCRIPT Centre for IT and IP law at the University of Edinburgh; Peter Van Valkenburgh, Director of Research at Coin Center; and Christoph Sorge, holder of the juris professorship of legal informatics, co-director of the Institute for Law and Informatics, and member of the Center for IT Security, Privacy and Accountability at Saarland University.

Darryl McAdams, IOHK's Team Plutus manager is working on a new programming language for smart contracts (Plutus) and is in Athens for the conference. According to Darryl, "A smart contract is a program which can implement an agreement of one form or another between multiple parties. They can be simple transfers of money, contracts in the traditional sense involving rights and obligations of various parties, or things more complex such as a game of chess, a distributed library, or a decentralized DNS system. In all of these cases, the purpose and behaviour of the system needs to be well understood, and in many cases, such as financial contracts with large sums of money involved, the correctness of the program is absolutely vital. In my talk, I will discuss the design of the Plutus language, a new programming language for authoring smart contracts, and demonstrate its use. I'll also discuss the motivation behind its design, especially with a view towards correct implementation of a contract's purpose and behaviour."

The event – "Smart Contracts Day, Cryptography & Law: Information, Privacy and Smart Contracts" – is taking place at the Hotel Divani Caravel, in central Athens. It is highly anticipated and currently sold out with more than 200 participants. Here’s more information: law.bitcoinschool.gr

Prof Kiayias concludes: "In the near future, this technology will give rise to "cryptolegal" frameworks, that, by merging cryptography and law, will be able to regulate interactions of persons at a global scale. In this way, such frameworks will transcend geographic and jurisdictional boundaries and create a dynamic global social institution that belongs to all and can be abused by none."

In my last blog post, we looked at the very basics of proof refinement systems. I noted at the end that there was a big drawback of the systems as shown, namely that information flows only in one direction: from the root of a proof tree to the leaves. In this post, we'll see how to get information to flow in the opposite direction as well. The code for this blog post can be found on GitHub here.

Addition Again

The addition judgment Plus which we defined last time was a three-argument judgment. The judgment Plus L M N was a claim that N is the sum of L and M. But we might want to instead think about specifying only some of the arguments to this judgment. In a language like Prolog, this is implemented by the use of metavariables which get valued in the course of computation. In the proof refinement setting, however, we take a different approach. Instead, we make use of a notion called bidirectionality, where we specify that a judgment's arguments can come in two modes: input and output. This is somewhat related to viewing thing from a functional perspective, but in a more non-deterministic or relational fashion.

Let's start by deciding that the mode of the first two arguments to Plus is that of input, and the third is output. This way we'll think about actually computing the sum of two numbers. Instead of three Nat inputs, we'll instead use only two. We'll use a judgment name that reflects which two:

-- Haskell

data Judgment = Plus12 Nat Nat
  deriving (Show)

// JavaScript

function Plus12(x,y) {
    return { tag: "Plus12", args: [x,y] };
}

The behavior of the decomposer for Plus12 will have to be slightly different now, though, because there are only two arguments. But additionally, we want to not only expand a goal into subgoals, but also somehow synthesize a result from the results of the subgoals. So where before we had only to map from a goal to some new goals, now we must also provide something that maps from some subresults to a result.

Rather than giving two separate functions, we'll give a single function that returns both the new subgoals, and the function that composes a value from the values synthesized for those subgoals.

-- Haskell
decomposePlus12 :: Nat -> Nat -> Maybe ([Judgment], [Nat] -> Nat)
decomposePlus12 Zero y = Just ([], \zs -> y)
decomposePlus12 (Suc x) y = Just ([Plus12 x y], \[z] -> Suc z)

decompose :: Judgment -> Maybe ([Judgment], [Nat] -> Nat)
decompose (Plus12 x y) = decomposePlus12 x y

// JavaScript

function decomposePlus12(x,y) {
    if (x.tag === "Zero") {
        return Just([[], zs => y]);
    } else if (x.tag === "Suc") {
        return Just([[Plus12(x.arg,y)], zs => Suc(zs[0])]);
    }
}

function decompose(j) {
    if (j.tag === "Plus12") {
        return decomposePlus12(j.args[0], j.args[1]);
    }
}

The decompose function is somewhat redundant in this example, but the shape of the problem is preserved by having this redundancy. The same is true of the Maybe in the types. We can always decompose now, so the Nothing option is never used, but I'm keeping it here to maintain parallelism with the general framework.

Building a proof tree in this setting proceeds very similarly to how it did before, except now we need to make use of the synthesis functions in parallel with building a proof tree:

-- Haskell

findProof :: Judgment -> Maybe (ProofTree, Nat)
findProof j =
  case decompose j of
    Nothing -> Nothing
    Just (js, f) -> case sequence (map findProof js) of
      Nothing -> Nothing
      Just tns -> let (ts, ns) = unzip tns
                  in Just (ProofTree j ts, f ns)

// JavaScript

function unzip(xys) {
    var xs = [];
    var ys = [];

    for (var i = 0; i < xys.length; i++) {
        xs.push(xys[i][0]);
        ys.push(xys[i][1]);
    }

    return [xs,ys]
}

function findProof(j) {
    var mjs = decompose(j);

    if (mjs.tag === "Nothing") {
        return Nothing;
    } else if (mjs.tag === "Just") {
        var js = mjs.arg[0]
        var f = mjs.arg[1]
        var mtns = sequence(js.map(j => findProof(j)));

        if (mtns.tag === "Nothing") {
            return Nothing;
        } else if (mtns.tag === "Just") {
            var tsns = unzip(mtns.arg);
            return Just([ProofTree(j, tsns[0]), f(tsns[1])]);
        }
    }
}

Now when we run this on some inputs, we get back not only a proof tree, but also the resulting value, which is the Nat that would have been the third argument of Plus in the previous version of the system.

Let's now add another judgment, Plus13, which will synthesize the second argument of the original Plus judgment from the other two. Therefore, the judgment Plus13 L N means L subtracted from N. We'll add this judgment to the existing Judgment declarations.

-- Haskell

data Judgment = Plus12 Nat Nat | Plus13 Nat Nat
  deriving (Show)

// JavaScript

function Plus13(x,z) {
    return { tag: "Plus13", args: [x,z] };
}

We can now define a decomposition function for this judgment. Notice that this one is partial, in that, for some inputs, there's no decomposition because the first argument is larger than the second. We'll also extend the decompose function appropriately.

-- Haskell

decomposePlus13 :: Nat -> Nat -> Maybe ([Judgment], [Nat] -> Nat)
decomposePlus13 Zero z = Just ([], \xs -> z)
decomposePlus13 (Suc x) (Suc z) = Just ([Plus13 x z], \[x] -> x)
decomposePlus13 _ _ = Nothing

decompose :: Judgment -> Maybe ([Judgment], [Nat] -> Nat)
decompose (Plus12 x y) = decomposePlus12 x y
decompose (Plus13 x z) = decomposePlus13 x z

// JavaScript

function decomposePlus13(x,z) {
    if (x.tag === "Zero") {
        return Just([[], xs => z]);
    } else if (x.tag === "Suc" && z.tag === "Suc") {
        return Just([[Plus13(x.arg, z.arg)], xs => xs[0]]);
    } else {
        return Nothing;
    }
}

function decompose(j) {
    if (j.tag === "Plus12") {
        return decomposePlus12(j.args[0], j.args[1]);
    } else if (j.tag === "Plus13") {
        return decomposePlus13(j.args[0], j.args[1]);
    }
}

If we now try to find a proof for Plus13 (Suc Zero) (Suc (Suc (Suc Zero))), we get back Suc (Suc Zero), as expected, because 1 subtracted from 3 is 2. Similarly, if we try to find a proof for Plus13 (Suc (Suc Zero)) (Suc Zero), we find that we get no proof, because we can't subtract a number from something smaller than it.

Type Checking Again

We'll aim to do the same thing with the type checker as we did with addition. We'll split the HasType judgment into two judgments, Check and Synth. The Check judgment will be used precisely in those cases where a type must be provided for the proof to go through, while the Synth judgment will be used for cases where the structure of the program is enough to tell us its type.

-- Haskell

data Judgment = Check [(String,Type)] Program Type
              | Synth [(String,Type)] Program
  deriving (Show)

// JavaScript

function Check(g,m,a) {
    return { tag: "Check", args: [g,m,a] };
}

function Synth(g,m) {
    return { tag: "Synth", args: [g,m] };
}

Additionally, because of these changes in information flow, we'll remove some type annotations from the various program forms, and instead introduce a general type annotation form that will be used to shift between judgments explicitly.

-- Haskell

data Program = Var String | Ann Program Type
             | Pair Program Program | Fst Program | Snd Program
             | Lam String Program | App Program Program
  deriving (Show)

// JavaScript

function Var(x) {
    return { tag: "Var", arg: x };
}

function Ann(m,a) {
    return { tag: "Ann", args: [m,a] };
}

function Pair(m,n) {
    return { tag: "Pair", args: [m,n] };
}

function Fst(m) {
    return { tag: "Fst", arg: m };
}

function Snd(m) {
    return { tag: "Snd", arg: m };
}

function Lam(x,m) {
    return { tag: "Lam", args: [x,m] };
}

function App(m,n) {
    return { tag: "App", args: [m,n] };
}

The last change that we'll make will be to change the notion of synthesis a little bit from what we had before. In the addition section, we said merely that we needed a function that synthesized a new value from some subvalues. More generally, though, we need that process to be able to fail, because we wish to place constraints on the synthesized values. To capture this, we'll wrap the return type in Maybe.

-- Haskell

decomposeCheck
  :: [(String,Type)]
  -> Program
  -> Type
  -> Maybe ([Judgment], [Type] -> Maybe Type)
decomposeCheck g (Pair m n) (Prod a b) =
  Just ([Check g m a, Check g n b], \as -> Just undefined)
decomposeCheck g (Lam x m) (Arr a b) =
  Just ([Check ((x,a):g) m b], \as -> Just undefined)
decomposeCheck g m a =
  Just ( [Synth g m]
       , \[a2] -> if a == a2 then Just undefined else Nothing
       )

decomposeSynth
  :: [(String,Type)]
  -> Program
  -> Maybe ([Judgment], [Type] -> Maybe Type)
decomposeSynth g (Var x) =
  case lookup x g of
    Nothing -> Nothing
    Just a -> Just ([], \as -> Just a)
decomposeSynth g (Ann m a) =
  Just ([Check g m a], \as -> Just a)
decomposeSynth g (Fst p) =
  Just ( [Synth g p]
       , \[t] -> case t of
                   Prod a b -> Just a
                   _ -> Nothing
       )
decomposeSynth g (Snd p) =
  Just ( [Synth g p]
       , \[t] -> case t of
                   Prod a b -> Just b
                   _ -> Nothing
       )
decomposeSynth g (App f x) =
  Just ( [Synth g f, Synth g x]
       , \[s,t] -> case s of
                     Arr a b | a == t -> Just b
                     _ -> Nothing)
decomposeSynth _ _ = Nothing

decompose :: Judgment -> Maybe ([Judgment], [Type] -> Maybe Type)
decompose (Check g m a) = decomposeCheck g m a
decompose (Synth g m) = decomposeSynth g m

// JavaScript

function eq(x,y) {
  if (x instanceof Array && y instanceof Array) {
    if (x.length != y.length) { return false; }

    for (var i = 0; i < x.length; i++) {
      if (!eq(x[i], y[i])) { return false; }
    }

    return true;
  } else if (x.tag === y.tag) {
    if (x.args && y.args) {
      return eq(x.args,y.args);
    } else if (x.arg && y.arg) {
      return eq(x.arg,y.arg);
    } else if (!x.arg && !y.arg) {
      return true;
    } else {
      return false;
    }
  }
}

function decomposeCheck(g,m,a) {
    if (m.tag === "Pair" && a.tag === "Prod") {
        return Just([ [Check(g, m.args[0], a.args[0]),
                       Check(g, m.args[1], a.args[1])],
                      as => Just(undefined)]);
    } else if (m.tag === "Lam" && a.tag === "Arr") {
        return Just([ [Check([[m.args[0], a.args[0]]].concat(g),
                             m.args[1],
                             a.args[1])],
                      as => Just(undefined)]);
    } else {
        return Just([ [Synth(g,m,a)],
                      as => eq(a,as[0]) ? Just(undefined) : Nothing ])
    }
}

function decomposeSynth(g,m) {
    if (m.tag === "Var") {
        var ma = lookup(m.arg, g);

        if (ma.tag === "Nothing") {
            return Nothing;
        } else if (ma.tag === "Just") {
            return Just([[], as => Just(ma.arg)]);
        }
    } else if (m.tag === "Ann") {
        return Just([ [Check(g, m.args[0], m.args[1])],
                      as => Just(m.args[1]) ]);
    } else if (m.tag === "Fst") {
        return Just([ [Synth(g, m.arg)],
                      as => as[0].tag === "Prod" ?
                              Just(as[0].args[0]) :
                              Nothing ]);
    } else if (m.tag === "Snd") {
        return Just([ [Synth(g, m.arg)],
                      as => as[0].tag === "Prod" ?
                              Just(as[0].args[1]) :
                              Nothing ]);
    } else if (m.tag === "App") {
        return Just([ [Synth(g, m.args[0]), Synth(g, m.args[1])],
                      as => as[0].tag === "Arr" &&
                              eq(as[0].args[0], as[1]) ?
                                Just(as[0].args[1]) :
                                Nothing ]);
    } else {
        return Nothing;
    }
}

function decompose(j) {
    if (j.tag === "Check") {
        return decomposeCheck(j.args[0], j.args[1], j.args[2]);
    } else if (j.tag === "Synth") {
        return decomposeSynth(j.args[0], j.args[1]);
    }
}

Finally, the findProof function has to be augmented slightly to deal with the new Maybe in the return type of the synthesizing function:

-- Haskell

findProof :: Judgment -> Maybe (ProofTree, Type)
findProof j =
  case decompose j of
    Nothing -> Nothing
    Just (js,f) -> case sequence (map findProof js) of
      Nothing -> Nothing
      Just tsas ->
        let (ts,as) = unzip tsas
        in case f as of
             Nothing -> Nothing
             Just a -> Just (ProofTree j ts, a)

// JavaScript

function findProof(j) {
    var mjs = decompose(j);

    if (mjs.tag === "Nothing") {
        return Nothing;
    } else if (mjs.tag === "Just") {
        var js = mjs.arg[0]
        var f = mjs.arg[1]
        var mtns = sequence(js.map(j => findProof(j)));

        if (mtns.tag === "Nothing") {
            return Nothing;
        } else if (mtns.tag === "Just") {
            var tsns = unzip(mtns.arg);
            var mn = f(tsns[1]);

            if (mn.tag === "Nothing") {
                return Nothing;
            } else if (mn.tag === "Just") {
                return Just([ProofTree(j, tsns[0]), mn.arg]);
            }
        }
    }
}

If we now try to find proofs for some typical synthesis and checking examples, we find what we expect:

findProof (Check [] (Lam "p" (Fst (Var "p"))) (Arr (Prod Nat Nat) Nat))

findProof (Check [] (Lam "p" (Fst (Var "p"))) (Arr Nat Nat))

findProof (Synth [("p",Prod Nat Nat)] (Fst (Var "p")))

Conclusion

The bidirectional style in this post has some interesting limitations and drawbacks. Consider the case of the rule for App: it has to synthesize the type of both the function and the argument and then compare them appropriately. This means that certain programs require additional type annotations to be written. But this is somewhat unnecessary, because once we synthesize the type of the function, we can use that information to check the argument. In the next blog post, I'll try to explain how to do this in a more elegant way, the combines both the upward and downward flows of information.

If you have comments or questions, get in touch. I'm @psygnisfive on Twitter, augur on freenode (in #haskell).

This post is the second part of a three part series, the first part is here, and the third part is here.