Using Catlab CCC as an implementation of Lambda Calculus

[jpfairbanks]

@epatters, what would it take to get Catlab to support CCC as a syntax for lambda calculus? I think we need at least:

1. Presentations of FreeCCC as the basis of a lisp like language (done)
2. An instance type for holding programs
3. An interpreter that can run those programs based on their functorial semantics in Set
4. Graphical syntax for displaying ev curry and hom(A,B) in graphviz/tikz/compose
5. @program to recognize ev, curry, hom terms

It looks like the examples/CompAlg is a good place to start. We could extend the Formula type to include lambda abstraction terms λ(A::Type,f::Function{A→B→C}) and then give it a primitive operator call(f,x) for the ev(::Hom(A,B), ::A) terms of CCC

I think the JuliaInterpreter would be a good framework for a runtime for evaluating julia code dynamically, it short circuits the julia compiler and allows you to execute julia code naively in julia. This is used in the Debugger because julia's JIT implementation spends more time JIT-ing than running in the context of a debugger.

I think once we have CCC ⟺ λ-calculus then we can take an instances in Turing.jl programs as an example of PPL programs as models of CCC in Stoch. Darren Wilkinson seems to be exploring PPL and FP ideas and is a serious Theory of Math Bio researcher.

What do you think?

[epatters]

Thanks for starting the discussion. I think that this is a good idea and that we are not too far off from being able to do it. Relevant issues for the wiring diagrams are #94, #12, #25.

The natural way to handle programs is to use Julia's own syntax for anonymous functions (#96). So if f(x,y) represents a morphism Hom(otimes(X,Y),Z), then y -> f(x,y) represents a morphism Hom(X,hom(Y,Z)) where hom is the internal hom. This is the standard way to interpret the typed lambda calculus in a CCC. So, both curry and ev will be implicit in the syntax. It should not be too hard to add this to @program.