An ideally typed Lisp would be no different then a dependently typed language semantically. Yes, you would use slightly different syntax but a key feature of m

An ideally typed Lisp would be no different then a dependently typed language semantically. Yes, you would use slightly different syntax but a key feature of most dependently typed languages is that they only have a single class of pseudo-terms that are used for both types and programs. An example Idris program: double : Nat -> Nat double n = 2 * n ourVectorType : Type ourVectorType = Vect (double 1) Int aVector : ourVectorType aVector = [1, 2] If you change everything above to an S-Exp you have a typed Lisp where both types and terms have the same language.