DISCLAIMER: In this post I explore an interesting but ill-advised use of Shen’s type system. Nothing in it should be taken as an indication of how to write good Shen.

Historically, a lauded feature of Lisp is its extensive support for runtime introspection. Common Lisp makes it easy to tease out properties of programs as first class values, which is especially useful when customizing the behavior of the language to a particular problem domain. The venerable Common Lisp Object System (CLOS) is renown in PL circles for its flexibility and dynamism — its first implementation was written entirely in the core Common Lisp language.

From the perspective of a language designer, the downside of extensive introspection support is that makes it much harder to introduce ways of expressing constraints on code into the language. In this post I want to show how we can enable a fast, type-driven, mostly reliable single dispatch mechanism in Shen.

Property lists and effectful programming in the type checker

One feature Shen exhibits from its Lisp heritage is the property list, or plist. A plist is a way of annotating data onto a symbol, which can be associatively read and modified at that symbol, stored as a list of key/value pairs. In chapter 24 of Practical Common Lisp, Seibel uses plists to control the expansion of a family of macros at compile time. Shen’s property lists can be annotated onto any Shen value, and are documented here.

We’ll begin by providing a typed version of Common Lisp’s type-of function. To do this we’ll exploit the fact that we have at our disposal most (all?) of the Shen language from within the sequent rules written in any datatype clause.

Since Shen is a Lisp, we also have the home advantage of homoiconicity. This means we can intercept any datum put out by the type checker — itself a Shen value — and do whatever we like with it in the course of checking that a value inhabits a type.

So, while verifying that a value X inhabits a type A, we’ll annotate X’s property list with a representation of its type A at the key type-rep. We’ll reference the value of type-rep when we add dynamic dispatch, but first we need to decide on a mode of representation. For type-reps, we’ll use Shen strings.

(define type->string
  { A --> string }  
  Str -> (make-string "~A" Str))

make-string writes a value to a string using the Fortran formatting notation for strings.

The type theory for type-reps is as follows.

(datatype type-reps
  ______________________________________________
  X : (type-rep A) >> (get X type-rep) : string;

  let Tag (put (eval X) type-rep (type->string A))
  ________________________________________________
  (tag-value-with-rep X A);

  X : A; (tag-value-with-rep X A);
  ________________________________
  X : (mode (type-rep A) -);)

We’ll run down the rules from the top. We consider that any value X of type A represents the type of A; the type (type-rep A) is nothing other than the type A.

The first rule says that if the value X represents A, it is annotated with the representation of A at the key type-rep in its plist, a string.

The second rule does the work of annotating the plist with the string representation of A at the key type-rep. Shen values get mangled slightly in the type checker, but the mangling can be undone using the eval function.

The third and final rule checks that X is of type A before firing the clause that annotates the plist of X appropriately. The mode ... - wrapper is there to prevent the type checker from entering an infinite loop upon encountering some of the more complicated (ie. polymorphic) types native to Shen.

We are finally ready to give the definition of type-of.

(define type-of
  { (type-rep A) --> string }
  X -> (get X type-rep))

And that’s it. All the heavy lifting is done in the type checker. We can test the operation of type-of on values of various types.

(36+) (type-of 3)
"number" : string

(37+) (type-of "a string")
"string" : string

(38+) (type-of false)
"boolean" : string

(39+) (type-of (@p 3 false [1 2 3] (@v (@v symbols are present <>) <>)))
"(number * (boolean * ((list number) * (vector (vector symbol)))))" : string

(40+) (type-of str)
"(Var17 --> string)" : string

The function str has the polymorphic type (A --> string), but here a skolemized variable Var17 is leaked out of the type checker. Obviously this poses a serious caveat to dynamic dispatch on polymorphic types. We should be more careful in defining type->string after deciding on a format for polymorphic type representation. This seems a job for the (Shen and human) reader and Shen Prolog.

Generic type verification

What we’ve developed is a semi-elegant way of implementing generic verified types. In the definition of a Shen function, the expression making up a where clause is automatically given the type ’verified’, something a Shen programmer can exploit to inject more information into the type theory on a case-driven basis.

If we lean heavily on the use of verified types, we may soon find we’ve overburdened the type checker with many ad hoc rules. Fortunately, we can leverage type-of to avoid that, at least when dealing with non-polymorphic types.

(define has-type?
  { (type-rep A) --> string --> boolean }
  X Type -> (= (type-of X) Type))

(datatype generic-verification
  if (= (type->string A) Str)
  ______________________________________
  (has-type? X Str) : verified >> X : A;)

has-type? checks that X has the type described in the string, by extracting its type representation from type-of. The rule in generic-verification proves that X has type A by appealing to the truth of has-type? on X and its purported representation Str.

Now we have type verification “for free”, at least on arbitrary concrete types, as demonstrated in the stupid and useless function arbitrary-messages.

(define arbitrary-messages
  { (type-rep A) --> string }
  X -> (let Y (+ X X) (str Y)) where (has-type? X "number")
  X -> (let Y (@s X X X) Y) where (has-type? X "string")
  X -> (@s "passed a " (type-of X)))

Note that X is being typed as a number, as a string, etc. in each of the adjoining clauses, and is treated accordingly. What we’ve created is essentially a limited but type safe version of Common Lisp’s typecase macro, without delving into macrology.

Opportunities and Shortcomings

We’ve mentioned the difficulty in dealing with polymorphic types, but another major shortcoming is that Shen’s type system is simply too powerful for this mechanism to work well across all applications. Shen places no restrictions on the number of types or the relations among types that any value may belong to.

On the bright side, a technique like this could serve as the basis for some form of automatic type-driven single dispatch; think Haskell’s typeclasses.

EDIT: Thanks to Mark Tarver for his comments on the code and corrections.

Source code

… is available here.