Paul William Berg

Ok. for type inference, let me work through this again.

First, lets assume a requirement to return int:

(+ a<int> b<int>)

Now, lets assume we choose the ephemeral constant 1 for a, satisfying the int, and apply (@) for b, with the requirement that the apply return an int:

(+ 1
   (@ c<(-> datum int)>))

The apply must choose a function. All functions are curried to 1 param:

(+ 1
   (@ (lambda (x) d<int>) 
   e<datum>))

Let's now choose for d. we choose if:

(+ 1
   (@ (lambda (x)
        (if f<bool> g<int> h<int))
      e<datum>))

Since we need a bool for the condition, we choose int? and x, since x is a datum and it can be sent to int? Lets also choose e and h (the false arm), since they are simple :

(+ 1
   (@ (lambda (x)
        (if (int? x) g<int> 0))
      (read))) 

That leaves us choosing for g. g must be an int. We would like to be able to let the algorithm choose x here, since x is guaranteed to be an int at run time. We would have to complicate our inferrence rule here though in order to do so, by making our inference rule understand that the run-time typing inferences of the conditional branch are all valid in the truth branch, allowing us to constrain our types further. That seems more solvable than my previous thoughts on the issue, but that severely complicates my inference algorithm (which is already ugly ugly.)

I will probably do this without types for now.