Of Pseudotypes And Typechecking
26 Feb 2013Typechecking 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.