Wednesday, 8 May 2013

Monads and Asynchronous Ajax with Javascript


Monads are often seen as a very basic part of the language for haskellers and something completely obscure for programmers which use other, especially non-functional, languages. Even lispers and schemers tend not to use them consciously to any great extent, even though they can help with a number of common problems that occur - perhaps most obviously with functions returning nil in a chain of compositions.

Monads, or Kleisli triples have a formal mathematical meaning which requires satisfaction of a few basic axioms. However, we can understand them fairly simply as a pattern which involves a bind operator which allows us to compose our monad objects, and a unit operator which allows us to lift a value up into one of monad objects.

MonadPlus extends this pattern and allows us a new type of composition +, and a new unit, called mzero that is somewhat like "plus" in the sense that + doesn't do anything when composed mzero.

MonadPlus turns out to be an excellent setting for conveniently dealing with concurrency. So it was that after playing with ajax for a while I found myself irritated with the way in which I had to wrap up continuations in order to get the sequencing behaviour I wanted. It occurred to me that what I really wanted was a MonadPlus.

I started writing one myself and realised that since my knowledge of javascript arcana was somewhat thin (one needs not simply implement them - they also have to be convenient to use!), I'd be better off finding out if someone else had already done it, and hence came to Douglas Crockford's video of javascript monads.

In this video Crockford demonstrates how to roll up a monadPlus object which he calls a vow. In his framework, he has a single composition function when which acts as a combination of bind and +. In order to lift a value into the monad, we use vow.keep(data). Since he doesn't use a strongly typed language, he's able to be a bit more flexible in what actually gets put in his when. In the example functions below, I always return a promise, which can be used by the next function in the chain - this is the standard way that bind works, composing functions (f : a → M b). However, the plumbing written by Crockfort will also automatically lift a function (f: a → b) into the monad, in the event that you have an immediate value and not a promise. Similarly, instead of composition with alternatives, we have our failure function in the right hand side.

This conveniently expresses a combination of "and/or" type asynchronous operators in a single convenient framework. We don't need to worry about when the asynchronous calls return - we are guaranteed that if they do, the next positive function in the chain will be called. If they don't return, we will fall over to our first error handler.

I wrote a quick application that demonstrates how you might use Crockfort's vows:

var iphost = "http://api.hostip.info/get_json.php";
  var countryhost = "http://api.hostip.info/get_json.php?ip=";
  function getIP(){ 
      var vow = VOW.make(); 

      var ajs = { 
          type : 'GET', 
          url : iphost, 
          dataType: 'json', 
          success : function(data){ 
              vow.keep(data.ip);
          }, 
          error: function(x,e){ 
              vow.break([x,e]);
          }
      }
      $.ajax(ajs);
      return vow.promise;
  }
  
  function countryOf(ip){ 
      var vow = VOW.make(); 

      var ajs = { 
          type : 'GET', 
          url : countryhost + ip, 
          dataType: 'json', 
          success : function(data){ 
              vow.keep(data.country_name);
          }, 
          error: function(x,e){ 
              vow.break([x,e]);
          }
      }
      $.ajax(ajs);
      return vow.promise;
  }

  function display(data){ console.log(data);}
  function showError(data){console.log("Error "+data);}

  $(document).ready(function (){
      getIP()
          .when(countryOf)
          .when(display, showError)
      
  });


UPDATE: Much to my surprise, all of this behaviour is already implemented with deferred ajax calls, using "then". It even manages to lift functions which don't return a promise into a promise automatically.

Coauthor Plus with twenty ten on wordpress.

I'm writing this post so that my future self knows how to edit the wordpress Twenty-Ten theme so as to add "coauthors plus" appropriately.

The first task is to install the coauthors plus plugin. Next, edit the functions.php theme file and change the twentyten_posted_on() file to include the following:

function twentyten_posted_on() {
 if ( function_exists( 'get_coauthors' ) ) {
  $author_string = '';
  $coauthors = get_coauthors();
  $first = true;
  foreach( $coauthors as $coauthor){
   if($first){
    $first = false; 
   }else{
    $author_string .= ', ';
   }
   $user_url = site_url('author/' . $coauthor->user_nicename);
   $author_string .= sprintf( '%3$s',
     get_author_posts_url( $coauthor->ID ),
     esc_attr( sprintf( __( 'View all posts by %s', 'twentyten' ), $coauthor->display_name ) ),
     $coauthor->display_name
     );
  }
 } else {
      $author_string = sprintf( '%3$s',
     get_author_posts_url( get_the_author_meta( 'ID' ) ),
     esc_attr( sprintf( __( 'View all posts by %s', 'twentyten' ), get_the_author() ) ),
     get_the_author()
     );
 }
 
 printf( __( 'Posted on %2$s by %3$s', 'twentyten' ),
  'meta-prep meta-prep-author',
  sprintf( '',
   get_permalink(),
   esc_attr( get_the_time() ),
   get_the_date()
  ),
  $author_string
  //sprintf( '%3$s',
 //  get_author_posts_url( get_the_author_meta( 'ID' ) ),
 //  esc_attr( sprintf( __( 'View all posts by %s', 'twentyten' ), get_the_author() ) ),
 //  get_the_author()
 // )
 );
}
endif;

Next, edit the loop-single.php after the post content where the author entry is, we add the following.

$coauthors = get_coauthors(); 
foreach($coauthors as $coauthor){
$userdata = get_userdata( $coauthor->ID );
if ( $userdata->description )


etc... filling in the $coauthor->foo or $userdata->bar as needed. Mostly everything is in $coauthor (i.e. display_name, user_email etc excepting for description, which is in $userdata->description.

Friday, 19 October 2012

Formalisation of Tables in a Dependent Language




I've had an idea kicking about in my head for a while of making query plans explicit in SQL in such a way that one can be assured that the query plan corresponds to the SQL statement desired. The idea is something like a Curry-Howard in a relational setting. One could infer the plan from the SQL, the SQL from the plan, or do a sort of "type-checking" to make sure that the plan corresponds to the SQL.

The devil is always in the details however. When I started looking at the primitives that I would need, it turns out that the low level table joining operations are actually not that far from primitive SQL statement themselves. I decided to go ahead and formalise some of what would be necessary in Agda in order get a better feel for the types of objects I would need and the laws which would be required to demonstrate that a plan corresponded with a statement.

Dependent types are very powerful and give you plenty of rope to hang yourself. It's always something of a struggle for me to figure out what I want to live in the type world as opposed to what I want to live in the term world.

First things first. We're going to need rows if we want tables. In dynamically typed languages (a.k.a. languages with a [potentially open] universal type) you can easily make a heterogeneous collection of objects (numbers, strings etc). Modelling a row in lisp or python is very straight forward. However, in a strongly typed setting heterogeneous lists are more complicated. The solution I have written in Agda below uses a vector (really just a list with a guaranteed size) of types which lives in the type universe, and which is constructed as we push things into our row. This is basically just a heterogeneous list where the type advertises what kind of row it is.

module RowList where

open import Level renaming (suc to lsuc; zero to lzero)
open import Data.Nat hiding (__)
open import Data.Vec renaming (__ to __; _++_ to _++_; [] to []; [_] to [_])
open import Data.List 
open import Data.Fin renaming (_+_ to _+f_)
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality as PropEq
  using (__; refl; sym; subst; trans; cong; cong₂; inspect)
open import Data.Bool

infixr 4 _,_
infixr 5 __

data Row {α : Level} : (n : )  Vec (Set α) n  Set (lsuc α) where 
  · : Row zero []
  _,_ :  {j} {A : Set α} {Aⱼ : Vec (Set α) j}  A  Row j Aⱼ -> Row (suc j) (A  Aⱼ)

In the data definition above we use (·) to terminate a row, and return a row which has an empty-vector in the rows type signature. In the
(,) case, we extend the row by giving an element of some type A and stick its type in our row signature vector. This will allow us to ensure that tables are constructed of homogeneous row types, and will allows us to present a lookup function for rows which knows what its return type will be.

You may notice all the bits about (Set α) etc. The α is just book keeping to avoid Russell-type paradoxes creeping in. They are otherwise not particularly enlightening and the above table definition might be more easily read if you ignore them.

example : Row 2 (  (  []))
example = (1 , 2 , ·)

pick :  {α i j A}  (v : Vec (Fin j) i)  Vec {α} A j  Vec A i
pick [] ys = []
pick (x  xs) ys = lookup x ys  pick xs ys 

__ :  {α j Aⱼ}  (r : Row {α} j Aⱼ)  (i : Fin j)  lookup i Aⱼ 
·  ()
(y , ys)  zero = y
(y , ys)  suc i = ys  i 

We call our row selection operation (r i) for a row (r) and index i. Notice that the return type is dependent on the type signature vector which is carried around in the type of the row. This selector will be useful for writing predicates over columns which will have to know what their input type is. We use a finite type (Fin j) to describe our index, since we need to make sure we don't index outside of the row. The finite type ensures us that whatever the index is, it's no greater than the size of the vector. These operations are now guaranteed to be type safe and can not lead to run-time out-of-range errors.

_++r_ :  {α i j Aᵢ Bⱼ}  Row {α} i Aᵢ  Row j Bⱼ  Row (i + j) (Aᵢ ++ Bⱼ)
· ++r r = r
(x , xs) ++r r = x , (xs ++r r)

We of course need to be able to combine rows from different tables in joins, and so we'll need a row concatenation operator, which we call (++r).

pickr :  {α i j Aⱼ}  (v : Vec (Fin j) i)  Row {α} j Aⱼ  Row i (pick v Aⱼ)
pickr [] r = · 
pickr (x  xs) r = r  x , pickr xs r

Additionally, it's useful if we can specify a list of indices we want to pick out of a row to construct a new row. This will allow us to make a "select" like statement where we can duplicate or ignore indices in order to create a new row, which when done over a list of rows will become more like the familiar table select.

Table :  {α} (m : ) (Aⱼ : Vec (Set α) m)  Set (lsuc α)
Table {α} m Aⱼ = List (Row m Aⱼ)

We define tables as simply a list of rows, and keep the indices and types as parameters to the type. The table header is now correct by construction and exists only as a type index.

{-
Example table: The header is specified as the type
-}
exampleTable : Table 3 (  (  (  [])))
exampleTable = (1 , 2 , 3 , ·)
             ((3 , 4 , 5 , ·)
             ((5 , 6 , 7 , ·)
             []))


__ :  {α i j Aᵢ Bⱼ}  Table {α} i Aᵢ  Table j Bⱼ  Table (i + j) (Aᵢ ++ Bⱼ)
[]  [] = []
[]  _  = []
_   [] = []
(x  xs)  (x'  xs') = x ++r x'  [ x ]  xs' ++ xs  (x'  xs') 
-- concatenate row, union row with the rest of the table

The familiar join operation. As you can see here, our primitive join operation does not take a restriction. In practice the primitive join would have to use the restriction in order to reduce the amount of row consing. In order to have a pragmatic optimiser, I'll have to change this later.

{-
Example join
-}
result : Table 6 (  (  (  (  (  (  []))))))
result = exampleTable  exampleTable
 

-- Restriction 
__ :  {α j Aⱼ}  Table {α} j Aⱼ   (Row j Aⱼ  Bool)  Table j Aⱼ
[]  p = []
(x  xs)  p = if p x then x  xs  p else xs  p 

Restrictions are just row predicates. They simply take a row and specify which rows to keep and which to throw away. This allows for most of the usual SQL WHERE clause shenanigans (minus aggregation of course) and gives us a fairly complete method of doing joins subject to restrictions [we don't deal with nulls at all].

{- 
Example restriction
-}
_b_ :  (n m : )  Bool
zero b m = true
suc n b zero = false
suc n b suc n' = n b n'

restrict : Table 6 (  (  (  (  (  (  []))))))
restrict = result  (λ v  (v  (# 1)) b 1)
Finally we have restriction, which allows us to pick and choose columns by specifying their index. It would of course be more natural to have names for columns and allow that as a means of addressing the columns of interest and I may in fact add that to rows in order to simplify the debugging, but it's not of much interest logically speaking.
-- Selection 
__ :  {α i j Aⱼ}  (v : Vec (Fin j) i)  Table {α} j Aⱼ  Table i (pick v Aⱼ)
xs  [] = []
xs  (y  ys) = (pickr xs y)  xs  ys

{- 
Example selection 
-}
-- Syntax of a query: (selector ∥ t1 ∪ t2 ∪ t3 ▹ restriction)


selection : Table 2 (  (  []))
selection = ((# 1)  ((# 3)  []))  result  (λ v  (v  (# 1)) b 4)

From this point we will need some form of relation which allows us to establish query equivalence. We will then want a way to compute whether two tables are equivalent up to this relation and we can continue on with the more pragmatic concerns of pushing the restrictions into the actual table joins.

Friday, 2 March 2012

Decidable Equality in Agda

So I've been playing with typing various things in System-F which previously I had left with auxiliary well-formedness conditions. This includes substitutions and contexts, both of which are interesting to have well typed versions of. Since I've been learning Agda, it seemed sensible to carry out this work in that language, as there is nothing like a problem to help you learn a language.

In the course of proving properties, I ran into the age old problem of showing that equivalence is decidable between two objects. In this particular case, I need to be able to show the decidability of equality over types in System F in order to have formation rules for variable contexts. We'd like a context Γ to have (x:A) only if (x:B) does not occur in Γ when (A ≠ B). For us to have statements about whether two types are equal or not, we're going to need to be able to decide if that's true using a terminating procedure.

And so we arrive at our story. In Coq, equality is something of a nightmare. In Agda, by contrast, often times this nightmare is avoided with clever structuring of the rules for elimination in pattern matching. However, Agda's lack of a system of tactics brings the nightmare home to roost in a different nest. This proof was 1 line in Coq, and amounts to evocation of the tactic decide equality. decide equality..

(Thanks to Saizan for showing me how to do this: Eq.agda)

First of course, we need to set up our modules etc...


module SystemFPlus where 

open import Function
open import Data.Fin using (Fin)
open import Data.Nat hiding (_*_) 
open import Data.Bool renaming (__ to __Bool) 
open import Data.List 
open import Data.Unit using ()
open import Relation.Nullary.Core
open import Data.Sum 
open import Data.Product 
--open import Relation.Binary.EqReasoning
open import Relation.Binary hiding (__)
open import Relation.Binary.PropositionalEquality as PropEq
  using (__; refl)

Next we write down an inductive definition for System-F style types.

data Ty : Set where
   : Ty                -- unit type
  ι :   Ty           -- universal abstraction vars
  η :   Ty           -- μ vars 
  __ : Ty  Ty  Ty  -- implication
  __ : Ty  Ty  Ty  -- conjunction
  __ : Ty  Ty  Ty  -- disjunction
  μ : Ty  Ty          -- inductive types
  Π : Ty  Ty          -- universal quantification

Next we have to do the business which is relatively usual in Agda, when proving negative goals under a constructor, that is, define explicit inversion principles. It turns out that you don't generally have to do this if you're not under a constructor and inside a λ but I haven't found a way to avoid it when you are, and you almost always are when you're proving false for something decidable.

invι :  {n m}  (ι n  ι m)  n  m
invι refl = refl 

invη :  {n m}  (η n  η m)  n  m
invη refl = refl 

invμ :  {α β}  (μ α  μ β)  α  β
invμ refl = refl 

invΠ :  {α β}  (Π α  Π β)  α  β
invΠ refl = refl 

invL :  {α β δ γ}  (α  β  δ  γ)  α  δ
invL {.α} {β} {α} {.β} refl = refl

invR :  {α β δ γ}  (α  β  δ  γ)  β  γ
invR {.α} {β} {α} {.β} refl = refl

invL :  {α β δ γ}  (α  β  δ  γ)  α  δ
invL {.α} {β} {α} {.β} refl = refl

invR :  {α β δ γ}  (α  β  δ  γ)  β  γ
invR {.α} {β} {α} {.β} refl = refl

invL :  {α β δ γ}  (α  β  δ  γ)  α  δ
invL {.α} {β} {α} {.β} refl = refl

invR :  {α β δ γ}  (α  β  δ  γ)  β  γ
invR {.α} {β} {α} {.β} refl = refl

Now comes the epic annoyance. This function could have been written by a program. It's absolutely vanilla, and yet I'm forced to write out the full cross-product of possibilities almost all of which lead to the conclusion: (λ ()), which is essentially, "no, and you should know why". Since it knows why, it seems unnecessarily arduous for me to have to write out every case!

__ty : Decidable {A = Ty} __
         ty      = yes refl
        (ι m) ty   = no (λ ())
        (η m) ty   = no (λ ())
        (δ  γ) ty = no (λ ())  
        (δ  γ) ty = no (λ ()) 
        (δ  γ) ty = no (λ ()) 
        (μ β) ty   = no (λ ()) 
        (Π β) ty   = no (λ ()) 
(ι n)     ty       = no (λ ())
(ι n)    (ι m) ty   with n  m 
(ι .n)   (ι n) ty   | yes refl = yes refl
(ι n)    (ι m) ty   | no p  = no (p  invι)
(ι n)    (η m) ty   = no (λ ())
(ι n)    (δ  γ) ty = no (λ ())  
(ι n)    (δ  γ) ty = no (λ ()) 
(ι n)    (δ  γ) ty = no (λ ()) 
(ι n)    (μ β) ty   = no (λ ()) 
(ι n)    (Π β) ty   = no (λ ()) 
(η n)     ty       = no (λ ())
(η n)    (ι m) ty   = no (λ ())
(η n)    (η m) ty   with n  m 
(η .n)   (η n) ty   | yes refl = yes refl
(η n)    (η m) ty   | no p  = no (p  invη)
(η n)    (δ  γ) ty = no (λ ())  
(η n)    (δ  γ) ty = no (λ ()) 
(η n)    (δ  γ) ty = no (λ ()) 
(η n)    (μ β) ty   = no (λ ()) 
(η n)    (Π β) ty   = no (λ ()) 
(μ α)     ty       = no (λ ())
(μ α)    (ι m) ty   = no (λ ())
(μ α)    (η m) ty   = no (λ ())
(μ α)    (δ  γ) ty = no (λ ())  
(μ α)    (δ  γ) ty = no (λ ()) 
(μ α)    (δ  γ) ty = no (λ ()) 
(μ α)    (μ β) ty   with α  β ty 
(μ .β)   (μ β) ty   | yes refl = yes refl 
(μ α)    (μ β) ty   | no p  = no (p  invμ)
(μ α)    (Π β) ty   = no (λ ())
(Π α)     ty       = no (λ ())
(Π α)    (ι m) ty   = no (λ ()) 
(Π α)    (η m) ty   = no (λ ())
(Π α)    (δ  γ) ty = no (λ ())
(Π α)    (δ  γ) ty = no (λ ())
(Π α)    (δ  γ) ty = no (λ ()) 
(Π α)    (Π β) ty   with α  β ty 
(Π .α)   (Π α) ty   | yes refl = yes refl 
(Π α)    (Π β) ty   | no p  = no (p  invΠ)
(Π α)    (μ β) ty   = no (λ ()) 
(α  β)   ty      = no (λ ())
(α  β)  (ι m) ty   = no (λ ())
(α  β)  (η m) ty   = no (λ ())
(α  β)  (δ  γ) ty   with α  δ ty  
(.α  β)  (α  γ) ty  | yes refl with β  γ ty 
(.α  .β)  (α  β) ty | yes refl | yes refl = yes refl
(.α  δ)  (α  γ) ty  | yes refl | no p = no (p  invR)
(α  β)  (δ  γ) ty   | no p = no (p  invL)
(α  β)  (δ  γ) ty = no (λ ()) 
(α  β)  (δ  γ) ty = no (λ ()) 
(α  β)  (μ δ) ty   = no (λ ()) 
(α  β)  (Π δ) ty   = no (λ ()) 
(α  β)   ty      = no (λ ())
(α  β)  (ι m) ty   = no (λ ())
(α  β)  (η m) ty   = no (λ ())
(α  β)  (δ  γ) ty   with α  δ ty  
(.α  β)  (α  γ) ty  | yes refl with β  γ ty 
(.α  .β)  (α  β) ty | yes refl | yes refl = yes refl
(.α  δ)  (α  γ) ty  | yes refl | no p = no (p  invR)
(α  β)  (δ  γ) ty   | no p = no (p  invL)
(α  β)  (δ  γ) ty = no (λ ()) 
(α  β)  (δ  γ) ty = no (λ ()) 
(α  β)  (μ δ) ty   = no (λ ()) 
(α  β)  (Π δ) ty   = no (λ ()) 
(α  β)   ty      = no (λ ())
(α  β)  (ι m) ty   = no (λ ())
(α  β)  (η m) ty   = no (λ ())
(α  β)  (δ  γ) ty   with α  δ ty  
(.α  β)  (α  γ) ty  | yes refl with β  γ ty 
(.α  .β)  (α  β) ty | yes refl | yes refl = yes refl
(.α  δ)  (α  γ) ty  | yes refl | no p = no (p  invR)
(α  β)  (δ  γ) ty   | no p = no (p  invL)
(α  β)  (δ  γ) ty = no (λ ()) 
(α  β)  (δ  γ) ty = no (λ ()) 
(α  β)  (μ δ) ty   = no (λ ()) 
(α  β)  (Π δ) ty   = no (λ ()) 

Well there has to be a better way right? So I thought I'd try to cook one up. It turns out that you can solve a decidable equality problem by injection into a domain with a decidable equality. So I went about thinking about what kind of decidable equality might have a domain with a similar enough shape that we could do the incoding without to much difficulty. I came up with the following program. It hardly saves any time at all unfortunately, but it does make me wonder if there isn't a more efficient way of doing it, perhaps using vectors, modules with decidable equalities for the carried data and with a single data constructor. Perhaps containers are the solution? I'm not sure. Anyhow, if you have a big inductive data type (such as a rich programming term language) this approach might save you trouble.

The trick is essentially to create an isomorphism with something like a Gödel coding. Since numbers are a hassle, and we need to have an isomorphism, it's more natural to do it into a space of trees where the trees have the same basic shape. We encode each operator as a number up to a finite size, whose limited nature is dictated by Fin n. This ensures that we don't have to worry about what to do with numbers bigger than the number of operators we have. The rest should be fairly self explanatory. Hopefully this gives someone ideas of a better way...

module TyDec where 

open import Function using (__)
open import Data.Nat hiding (_*_) 
open import Data.Fin renaming (zero to fzero ; suc to fsuc)
open import Data.Fin.Props renaming (__ to __fin)
open import Data.Product using (Σ; _,_; proj₁; proj₂)
open import Relation.Nullary.Core
open import Relation.Binary hiding (__)
open import Relation.Binary.PropositionalEquality as PropEq
     using (__; refl; trans; sym; cong)


data Ty : Set where
   : Ty
  ι :   Ty
  η :   Ty
  μ : Ty  Ty
  Π : Ty  Ty
  __ : Ty  Ty  Ty
  __ : Ty  Ty  Ty 
  __ : Ty  Ty  Ty

data Tree : Set where 
  Nullary : Tree
  NullaryNat : Fin 2    Tree
  Unary : Fin 2  Tree  Tree
  Binary : Fin 3  Tree  Tree  Tree

invNullaryNat1 :  {op1 op2 n1 n2}  NullaryNat op1 n1  NullaryNat op2 n2  op1  op2
invNullaryNat1 refl = refl

invNullaryNat2 :  {op1 op2 n1 n2}  NullaryNat op1 n1  NullaryNat op2 n2  n1  n2
invNullaryNat2 refl = refl

invUnary1 :  {op1 op2 t1 t2}  Unary op1 t1  Unary op2 t2  op1  op2
invUnary1 refl = refl

invUnary2 :  {op1 op2 t1 t2}  Unary op1 t1  Unary op2 t2  t1  t2
invUnary2 refl = refl

invBinary1 :  {op1 op2 l1 l2 r1 r2}  Binary op1 l1 r1  Binary op2 l2 r2  op1  op2
invBinary1 refl = refl

invBinary2 :  {op1 op2 l1 l2 r1 r2}  Binary op1 l1 r1  Binary op2 l2 r2  l1  l2
invBinary2 refl = refl

invBinary3 :  {op1 op2 l1 l2 r1 r2}  Binary op1 l1 r1  Binary op2 l2 r2  r1  r2
invBinary3 refl = refl

__tree : Decidable {A = Tree} __
Nullary                Nullary               tree = yes refl  
Nullary                (NullaryNat op n)     tree = no (λ())
Nullary                (Unary op t)          tree = no (λ())
Nullary                (Binary op l r)       tree = no (λ())
(NullaryNat op n)      Nullary               tree = no (λ ())
(NullaryNat op1 n1)    (NullaryNat op2 n2)   tree with op1  op2 fin
(NullaryNat .op1 n1)   (NullaryNat op1 n2)   tree | yes refl with n1  n2
(NullaryNat .op1 .n1)  (NullaryNat op1 n1)   tree | yes refl | yes refl = yes refl
(NullaryNat .op1 n1)   (NullaryNat op1 n2)   tree | yes refl | no p = no (p  invNullaryNat2)
(NullaryNat op1 n1)    (NullaryNat op2 n2)   tree | no p  = no (p  invNullaryNat1) 
(NullaryNat op1 n1)    (Unary op t)          tree = no (λ())
(NullaryNat op1 n1)    (Binary op l r)       tree = no (λ())
(Unary op1 t1)         Nullary               tree = no (λ())
(Unary op1 t1)         (NullaryNat op n)     tree = no (λ())
(Unary op1 t1)         (Unary op2 t2)        tree with op1  op2 fin
(Unary .op1 t1)        (Unary op1 t2)        tree | yes refl with t1  t2 tree
(Unary .op1 .t1)       (Unary op1 t1)        tree | yes refl | yes refl = yes refl
(Unary .op1 t1)        (Unary op1 t2)        tree | yes refl | no p = no (p  invUnary2) 
(Unary op1 t1)         (Unary op2 t2)        tree | no p = no (p  invUnary1) 
(Unary op1 t1)         (Binary op2 l r)      tree = no (λ())
(Binary op l r)        Nullary               tree = no (λ())
(Binary op1 l r)       (NullaryNat op2 n)    tree = no (λ())
(Binary op1 l r)       (Unary op2 t)         tree = no (λ())
(Binary op1 l1 r1)     (Binary op2 l2 r2)    tree with op1  op2 fin
(Binary .op1 l1 r1)    (Binary op1 l2 r2)    tree | yes refl with l1  l2 tree
(Binary .op1 .l1 r1)   (Binary op1 l1 r2)    tree | yes refl | yes refl with r1  r2 tree
(Binary .op1 .l1 .r1)  (Binary op1 l1 r1)    tree | yes refl | yes refl | yes refl = yes refl
(Binary .op1 .l1 r1)   (Binary op1 l1 r2)    tree | yes refl | yes refl | no p = no (p  invBinary3)
(Binary .op1 l1 r1)    (Binary op1 l2 r2)    tree | yes refl | no p = no (p  invBinary2)
(Binary op1 l1 r1)     (Binary op2 l2 r2)    tree | no p = no (p  invBinary1)

{- 
Op codes 

Nullary
ι = 0
η = 1

Unary
μ = 0 
Π = 1

Binary
⇒ = 0
⊗ = 1
⊕ = 2
-} 

jni : Tree  Ty 
jni Nullary                              =  
jni (NullaryNat fzero n)                 = ι n
jni (NullaryNat (fsuc fzero) n)          = η n
jni (NullaryNat (fsuc (fsuc ())) n)   
jni (Unary fzero t)                      = μ (jni t)
jni (Unary (fsuc fzero) t)               = Π (jni t)
jni (Unary (fsuc (fsuc ())) t)
jni (Binary fzero l r)                   = (jni l)  (jni r)
jni (Binary (fsuc fzero) l r)            = (jni l)  (jni r)
jni (Binary (fsuc (fsuc fzero)) l r)     = (jni l)  (jni r)
jni (Binary (fsuc (fsuc (fsuc ()))) l r) 

injEx : (x : Ty) -> Σ Tree \ t -> jni t  x
injEx                          = Nullary , refl 
injEx (ι n)                     = NullaryNat fzero n , refl
injEx (η n)                     = NullaryNat (fsuc fzero) n , refl
injEx (μ t)                     with injEx t
injEx (μ .(jni tree))           | tree , refl = (Unary fzero tree) , refl
injEx (Π t)                     with injEx t
injEx (Π .(jni tree))           | tree , refl = (Unary (fsuc fzero) tree) , refl
injEx (t  s)                   with injEx t
injEx (.(jni tr1)  s)          | tr1 , refl with injEx s
injEx (.(jni tr1)  .(jni tr2)) | tr1 , refl | tr2 , refl = (Binary fzero tr1 tr2) , refl 
injEx (t  s)                   with injEx t
injEx (.(jni tr1)  s)          | tr1 , refl with injEx s
injEx (.(jni tr1)  .(jni tr2)) | tr1 , refl | tr2 , refl = (Binary (fsuc fzero) tr1 tr2) , refl 
injEx (t  s)                   with injEx t
injEx (.(jni tr1)  s)          | tr1 , refl with injEx s
injEx (.(jni tr1)  .(jni tr2)) | tr1 , refl | tr2 , refl = (Binary (fsuc (fsuc fzero)) tr1 tr2) , refl 

inj : Ty  Tree
inj = proj₁  injEx -- strip off the existential proof

injeq :  {x y} -> inj x  inj y -> x  y
injeq {x} {y} p = trans (sym (proj₂ (injEx _))) (trans (cong jni p) (proj₂ (injEx _)))

__ty : (x y : Ty) -> Dec (x  y)
x  y ty with (inj x)  (inj y) tree
x  y ty | yes p = yes (injeq p)
x  y ty | no p = no (p  (cong inj))