Of Pseudotypes And Typechecking

Typechecking at runtime is easy, and that's what I presented last time with my post and this library. However as I noted at length, the value of a type system is not in its runtime correctness, it is in the power of such systems to indicate errors before the occur at runtime and thus allow programmers to prevent them through application of functions which are legal for the involved types.

Now, lisp has this awesome feature best known as macros for evaluating code at compile time. These macros are best known for being used to generate code, but why not use them for type checking? Clojure associates metadata with every symbol... typically an :added value to state what library version it was added in and a :doc value which constitutes the symbol's documentation. What if I extend my (deftypedfn) to add a :type to that metadata? Then compile-time typechecking becomes possible by simply comparing :type fields using some definition of equality on types.

Easier said than done

The mechanics are simple, but unfortunately they dirty Clojure's semantics. Either one may employ a macro, say something semantically equivalent to CL's funcall symbol or Clojure's apply which allows for the explicit symbolic invocation of the value. This creates artificial and consequently undesirable separation between typechecked and untyped operations because I must force this artificial funcall invocation upon programmers.

An alternative approach is to change what I bind to the typed function symbol. Rather than give the typechecked function its own name as it were, I could instead bind the function to a known and stored gensym and then provide (foo x .. ) as a macro which typechecks at compile time, errors if appropriate and expands away to (<gensym> x ...). This is great and would work a treat but for one little detail: apply.

Apply is wonderful. Usually I don't have to use apply, but when I do I'm damn glad I have it. However and for very good reasons, apply is not legal on macros! This leaves a programmer who chooses to apply his function(s) rather than simply envoking them directly up a creek as they have no knowlege what the real symbol their function is bound to may be. A partial fix to this would be a standard where for the (deftypedfn foo int ...) the symbol foo is reserved for the typechecking macro and _foo is allocated for the function foo. This would be workable but would burden a programmer with the knowlege that the symbol _foo would be generated silently and is not equivalent to foo as they defined it.

Of Typesystems

As I am proposing a typesystem here, I need to justify its type derivation structure and perhaps even provide additional tools for manipulating type definitions.

The type "formalism" upon which the first generation of pseudotypes operates is disgustingly naive. It uses no algebraic definition of types, rather relies upon the Clojure standard that for a type T there exists a function T? being a predicate which tests for T-ness as it were. So number?, float?, seq? and soforth. As these predicates and the types which they test for provide or prohibit operations it is clear that a definition of type could be derived from these forms, and that working from such a definition I could proceed to develop an arithmetic type system not unlike that which Haskell uses.

I consider such a type system harmful rather than interesting simply because my goal was not to ensure correctness by types, but rather to ensure correctness by pseudotypes which the simple type definition which the existing pseudotypes system supports.