Homoiconic type theory

Question

Lisp has the property of being homoiconic, that is, the representation of code used by the language implementation (lists) is also available to, and idiomatically used by, programs that want to represent code for their own purposes.

The other major family of functional programming languages, ML, is based on type theory, which means that the language implementation needs a more complex representation of code, and is also less casual about what you are allowed to do, so typically the internal representation is not available to programs. For example, proof checkers for higher-order logic are often implemented in ML family languages, but normally implement their own type theory system, effectively ignoring the fact that the ML compiler has one already.

Are there any exceptions to this? Any programming languages based on type theory, that expose their code representation for programmatic use?

Answer 1

Take a look at type systems for staged execution (a weak form of metaprogramming), for example, the one used in MetaML language.

Also note that while attractive at first glance, homoiconicity (and metaprogramming by direct AST manipulation in general) turned out to be inconvenient in practice. Take a look at modern systems of macros in Nemerle and an experimental extension of Scala, which both rely on quasi-quotation if I remember correctly.

As for why ML type theory is not reused, here are a few considerations:

• ML type system is not expressive enough (think of dependent types)
• ML type system is polluted with general recursion and mutable references
• There are no consensus on which type system is usable both for proving and writing general-purpose programs. It is an ongoing research. See for example http://www.nii.ac.jp/shonan/seminar007/ . So every prover implements his own theory just because authors fix flaws in previous type theories.

Answer 2

The other major family of functional programming languages ... is based on type theory, which means that the language implementation needs a more complex representation of code

I see no reason why this would be true.

If you haven't seen it already, you may be interested in Liskell, which advertises itself as Haskell semantics + Lisp syntax.

Answer 3

The main profit from Lisp being homoiconic is strong metaprogramming capacity. I guess you might want to take a look at type-safe metaprogramming, particularly Template Haskell.

Answer 4

Shen :

Shen has one of the most powerful type systems within functional programming. Shen runs under a reduced instruction Lisp and is designed for portability.

E.g.:

(define total
  {(list number) --> number}
  [] -> 0
  [X | Y] -> (+ X (total Y)))

---

Typed Racket :

Typed Racket is a family of languages, each of which enforce that programs written in the language obey a type system that ensures the absence of many common errors.

E.g.:

#lang typed/racket
(: sum-list (-> (Listof Number) Number))
(define (sum-list l)
  (cond [(null? l) 0]
        [else (+ (car l) (sum-list (cdr l)))]))

---

Mercury :

Mercury is a logic/functional programming language which combines the clarity and expressiveness of declarative programming with advanced static analysis and error detection features.

E.g.:

:- func sum(list(int)) = int.   
sum([]) = 0.
sum([X|Xs]) = X + sum(Xs).

Answer 5

Are there any exceptions to this? Any programming languages based on type theory, that expose their code representation for programmatic use?

SML does not expose code programmatically but OCaml and F# do. OCaml has a full macro system.