Is it possible to realize the benefits of dependent typing using macros in Lisp?

Question

This is an honest question, not a a troll. I'm asking for your patience.

When Cedric talks about dependent types, the benefit he states is checking List lengths at compile time:

Having a list with one element would be a type error, so the second line in the snippet above should not compile.

When Ana Bove and Peter Dybjer talk about dependent types, the benefit they state is checking list lengths at compile time:

Dependent types are types that depend on elements of other types. An example is the type An of vectors of length n with components of type A. Another example is the type Amn of m n-matrices. We say that the type An depends on the number n, or that An is a family of types indexed by the number n.

The larger point being we have additional guarantees about the correctness of our program because of additional information and checks at Compile time.

Now my experience is that people (from a Haskell background) sneer at Lisp because it is a 'dynamic language'. Where they're coming from is that it looks unsound because of how it compares to the rich Haskell type system. (I hold nothing against them - I think it is very interesting).

The point is they claim that Haskell (or Agda etc) has additional information at compile time that is not available to a dynamic language like Lisp. (I'm going to use Lisp as the 'family of languages' and assume that Clojure is a Lisp).

Now I can do the following in Clojure to check the length of an array at compile time:

(def my-vec-of-length-2 [0 1])

(defmacro compile-time-vec-length-check [x n] 
  (let [x @(resolve x)] 
    (assert (= n (count x)))))

(compile-time-vec-length-check my-vec-of-length-2 3)

Now this will fail, because I'm expecting a vector of length 3, but the underlying vector is of length 2. I got this information at Compile Time.

user$ lein uberjar

Compiling compile-time-vec-check.core
Exception in thread "main" java.lang.AssertionError: Assert failed: (= n (count x))

Now I seem to be getting the benefits of Dependent Typing in a 'dynamic language'.

My question is Is it possible to realize the benefits of dependent typing using macros in Lisp?

Answer 1

Yes, but not the way you're proposing.

Just checking a vector whose size we know exactly at compile time is not difficult and does not require dependent types. We can do this in a fairly straightforward way in normal typed languages with polymorphic types.

The important insight with dependent types is that they can depend on runtime values. In your example, all the numbers (2 and 3) have to be known at compile time for the assert to work properly. Let's imagine a function zero_vec which takes a number and gives you a vector of that length full of 0s. In a dependently typed pseudocode, this would look something like:

zero_vec : (n : ℕ) → Vec n

Note how the argument's value n appears in the result type! In particular, zero_vec 10 would have the type Vec 10 and zero_vec 42 would have the type zero_vec 42. More importantly, though, you could pass in a value that you don't know at runtime to zero_vec and still typecheck your code. Imagine something like this:

n : ℕ ← readLine
zero_vec n : Vec n

You could still check this against sizes at compile time. For example, the following should work:

checkLength (zero_vec n) n

Or you should even be able to have a type like "vectors of length 3 or greater" and be able to check zero_vec n against that too; this should give you an error since it can't prove the n you read in is ≥ 3.

The point is that typechecking essentially becomes a pretty general form of abstract interpretation where you have to be able to propagate and check against values that you won't know until runtime.

You can't do that with your macro approach.

However, I think you can replicate dependent types with macros. The only problem is that you would essentially have to implement a whole dependent typechecker using your macro system! Which is a bit of an undertaking, but probably not as difficult as you think¹.

In fact, my understanding is that Qi and Shen are two languages implemented as Common Lisp macros with type systems as powerful as dependent types. For various reason, I've never used them (and probably never will) so I'm not sure exactly how they work.

¹ Check out "Simply Easy" for a nice tutorial.