Lambda the Ultimate

Here is an outline of a new lisp I plan on creating. Its a fusion of current PLT theories which takes a SchemI am deconstructing lisp and finding what is really meant in lisp and reconstructing it utilizing category theory and logical programming. Scheme is still used for all computation. Its a strongly typed scheme with type inference signature are used to type the language. Categories become your way to create new data types. Your base data type is a topos or basically a type of set from set theory. A set os a collection of things. Lisp is used as the primary syntax so it is a lisp like system. Graphs are also a base data type so the things you do in lisp can be generalized so basically you can code in lisp but it would be weakly typed. The language borries alot from haskell in its design and scheme in its philosophy and design.

By reconstructing I mean actually taking axioms of lisp and retooling them into logic and category theories. Lisp becomes something different and instead a subset of the language. Lisp will be fully expressable as a turing complete language but there will be other paradigms in the language.

Functional programming is still a part of lisp. We also add monads to represent computation. Category theory is based upon morphism and we apply this as morphisms on HOFs. The base data types are graphs and topos. Since all other data types will be defined in this manner we have a interconnection between functional data structures and categorial. Sort of a fusion of scheme and haskell.

The virtual machine is my own design which is also based upon an upcoming arxiv paper. The first step is to get it working on that register machine. The special part of this register machine is that it is intended to work as a hypercomputer although if that fails it still is easy to implement parallelism due to its matrix based design. for more information.

The kali scheme system will be ported to scheme48 1.3 and used for parallelism. It was a abandoned research project at NEC but it was still functional. This would be a subproject of the total project.

Here is how an example program looks


(define-functor (fact-functor sub1) => (fact)
(define (fact n)
(if ( one
(* n (fact (sub1 n))))))
(define-morphism fact-functor N$)
;;N is the set of natural numbers
;;


Join me in #categorizer on freenode.net or zitterbewegung@gmail.com on gtalk/email if you want to discuss ---- Further reading

Category theory from haskell wiki http://www.haskell.org/haskellwiki/Category_theory

A proposal for a Galois Machine See http://arxiv.org/abs/0812.4009 also http://www.reddit.com/r/math/comments/7nh74/ask_mathithelp_this_is_my_first_paper_in/

Charity papers on cat theory ftp://ftp.cpsc.ucalgary.ca/pub/projects/charity/literature/papers_and_reports/dataII.ps

Github source repository for implementation

http://github.com/zitterbewegung/categorizer/tree/master

Kali Scheme Revival

http://community.schemewiki.org/kali-scheme/

From by basic understanding, in System F, a polymorphic function is a single value that can be directly applied to an argument. I want to know: is there a formalism where a "polymorphic function" is really a declaration of a family of monomorphic functions, indexed by the types used for instantiation. Thus, two calls to the same [nominal] polymorphic function with different types would resolve to two calls to different monomorphic functions. Clearly this model is more towards the C++ idea of function templates than the FP idea of polymorphic functions.

For polymorphic functions with these semantics, it seems that there would be a more clear distinction of what can be resolved at compile-time, using the type information available at instantiation, and what needs run-time dispatch. Perhaps, then, this formalism could also be used as a target language of an optimization that specializes true (System F) polymorphic functions.

So, does anyone know any work in this direction?
Thank you!

I don't know if this is the true explanation of the Zune blackout, but if it is it is bloody hilarious.