Lambda the Ultimate

I suspect that when you ask 'what is good / bad about this?', you're effectively asking 'what's good / bad about dependent types', and their pros and cons have, I think, been well-discussed in other threads here.

I say this because I suspect a full-on turing-complete theorem-proving type system with some kind of dependent types would be necessary to handle this sort of thing. But I may be wrong. Perhaps a weaker type system could still infer these sorts of types in very limited circumstances?

I spent the morning reading up on dependent types, thanks for having brought this to my attention.

So AFAIU C++ templates act as a limited form of dependent types within the context of a weak type system. For example the work of Tood Veldhuizen ( http://osl.iu.edu/~tveldhui/papers/Template-Metaprograms/meta-art.html ) has apparently made good use of them.

For example, to type-check a function

f : Int -> Singleton(0)

would require proving that f returns zero for every single input. For general f, this would be undecideable - see Rice's theorem.

For example, say we write the function f above so it returns 1 if its argument is an even number greater than two which doesn't exist as a sum of two primes, or 0 otherwise. If the type-checker terminates then it looks like we've settled Goldbach's conjecture!

Really I'm wondering what the proposed use-case is for types like these. What kind of properties of programs would you hope to be able to check at compile-time with these types, that can't be checked using simpler type systems? I can only see them being inferred for trivially constant functions, the sort of thing which I expect pure functional compilers can optimize away already without needing to involve the type system. But quite likely I'm missing something.

For example, say we write the function f above so it returns 1 if its argument is an even number greater than two which doesn't exist as a sum of two primes, or 0 otherwise. If the type-checker terminates then it looks like we've settled Goldbach's conjecture!

I would approach this problem by having the type-checker reject any program which even suggests the possibility of returning 1.

I can only see them being inferred for trivially constant functions, the sort of thing which I expect pure functional compilers can optimize away already without needing to involve the type system. But

If I can formalize this within the type system, then I can write more interesting metaprograms.

Of course you can't always infer that a function returns a singleton value, but in these cases, you can simply infer that it returns an int. Inference is not the goal however, I simply view it as a tool.

Such a type system is generally undecidable, but it can typecheck all programs that typecheck in simpler decidable type systems, plus lots of additional programs written using more powerful and expressive constructs (but not all of them!)

I'm certainly an advocate of gaining more expressive type systems at the expense of decidability.

After all, what you really care about is the following: If your compiler accepts a program successfully, then the program is type-safe. If it's not type-safe, then you might get an error message, or a stack overflow, or a core dump, or whatever -- but in no case will you see the compiler accept a program that's not type-safe.

Yes adding extra expressiveness sounds like a good idea, even if it's not decideable in the general case. I guess my issue is this (in a pure functional language, at least):

In what situation would it be useful to declare a singleton type in a function signature? If I already know when writing the program which exact value the function argument must always be, or which value the function will always return, then why bother having it as an argument or return value in the first place? It would make the type system more expressive, I just can't immediately see where that extra expressiveness would come in useful.

On the other hand, if the system can infer these types in some situations, then that could help the compiler optimize away constant functions. But like I said, I don't see the need to get the type system involved here, unless there's a practical use for the extra expressiveness. Which perhaps there is - I'm just curious if you had anything particular in mind.

I can see these being useful in the context of an even-richer type system. Perhaps that's where you're coming from.

Thanks Tim, I like this approach a lot. It helps me frame my ideas with more standard nomenclature.

In general what you describe is very much like what I was planning to do with Cat. I am designing the Cat type system to be dynamic by default (everything is a variant), with types as first class values. If the language is compiled then the the compiler infers where values are constants (or a small set of possibilities) and precomputes as much code as possible.

This precomputation phase effectively performs static type-checking. by pre-evaluating expressions involving types at compile-time.

This way the type-system is as expressive as the programming language itself.