Author here. Besides creating Typo as an exercise in implementing a language, it's also the punchline to a seven-year-old joke[1] about implementing RSA in Haskell's type system, which I did:
Hopefully I'll have the time next week to write a blog post explaining how the encoding of functions work, as well as a cool transformation I employed to make the translation simpler than it otherwise would be.
I've always hoped some language would have a prolog type system. Just today, I was pointed to liquid types [1,2] in haskell-cafe, and they look really promising in that respect. But the idea of having my compiler bail with a nice error message when I try:
fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
fibPlus :: (int LESSTHAN 30) -> (int LESSTHAN 500000)
fibPlus x = fibs !! x + 100
Hindley-Milner style type inference, which is done by MLs and is similar to what is done in Haskell, uses unification, which is a large part of how Prolog reasons, to determine if two types with still unknown subparts can be the same. You can do surprisingly complex things in these type systems.
For a more complex type system that does similar things and allows a lot more reasoning in the type system, you could take a look at Agda. This is a Haskell-like language with a fully dependent type system, i.e., types can contain arbitrary language terms. This has the downside of being not-quite-Turing-complete, as you want to be able to decidably typecheck. However, it is powerful enough that its type system is often used to automate proofs about both programming language theory and more ordinary math.
Don't you think an example where the type system has a visible impact would be appropriate? As it is now, none of the examples show anything that doesn't look like vanilla lisp. I think what makes the Haskell type system nice to use is inference along with type assertions. Do you have type assertions, or is the implementation of types behind the scenes until a type mismatch occurs?
I think maybe you misunderstood what the language does. It is compiled not to Haskell itself, but to the type system. No Haskell code is executed when using the interpreter (well, apart from the interpreter's itself), but it is Haskell's types that are... executed? checked? It's as is you made a program using C++ templates, not C++.
Well, it depends on what you mean by "Haskell's" type system. The standard Haskell type system, as defined by the Haskell 98 spec, is decidable (and hence not Turing complete).
Thus Typo uses a number of GHC-specific type system extensions, one of which has "Undecidable" in its name. They're hidden in Prelude.hs.
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}
It's very common to use some extensions, but AFAIK pretty rare to use UndecidableInstances. I'm not actually sure what it does.
While I was writing the Prelude, I messed up one of the definitions and ghc kept blowing the context stack limit. So I tried it with -fcontext-stack=5000, figuring it wasn't my bug but just a consequence of the inefficient encoding I was using. The type system ended up allocating upwards of 4 gigs before I killed it.
There is nothing inherently bad with turing complete type systems aka allow powerful logic but aren't total (there are ways to avoid proof inconsistency). Other than the risk of non terminating type checking/compilation, the issue is a matter of difficulty (hard to do right) not principle (bad to do).
The problem with C++ templates is not that they are turing complete. Versus Haskell, it is the difference between one day waking up and finding out that layer upon layer of unspeakable ad-hocery have suddenly yielded a deranged spam bot suffering from a severe case of logorrhea that can pass the turing test, given a patient examiner.. And an AI designed from first principles using an elegant theory - even if messy in implementation from unforeseen expectations requiring a patchwork of (still principled) extensions.
A compile-time C++ LISP interpreter I wrote a while ago just for fun: http://pastebin.com/yz4XvYra (scroll to the bottom for an example).
It's a shame that C++ lacks proper support for compile-time strings, but it would be trivial to write a preprocessor turning a string into a list of char literals.
I submitted a pull request, and just now I noticed other three identical requests. So I submitted a Github feature request to warn on overlapping contributions, probably along with a few others...
Until then, enjoy!
[1]: http://article.gmane.org/gmane.comp.lang.haskell.general/132...