Lambda the Ultimate

If you take the Curry-Howard perspective, the types in a total functional programming language form a logic (see e.g. Coq)

I doubt this always holds. Operationally, you can easily have a programming language where the Curry-Howard correspondence does not hold (logically, on the type level, everything can be proven true because, say, it uses the infinite type), but the type system makes perfect sense from an operational perspective.

The Curry-Howard correspondence is a correspondence between certain type systems and terms where terms can be seen as a programming language. It certainly doesn't mean every language satisfies that correspondence.

It is too easy to say that every total functional language would satisfy the correspondence.

Is this any different from simply saying that some of the logics involved are really, really screwy and not much actual use as logics? (I'm sure we can all think of type systems that aren't much use as type systems either, of course)

I just meant to say that Curry-Howard correspondence has little to do with it. Of course you can also give a diagonalization argument in a typed calculus setting, maybe even more easy or readable (I don't know), but introducing that specific setting for this general notion is superfluous.

That there are really screwy type-systems; yeah, I guess I believe that. Heck, Martin-Low even got his first approach wrong.

Also, some type system for programming languages just do not fit nicely with the Curry-Howard correspondence. Or stated better, the type level is logically non-sensical/has no particular meaning. That certainly don't make them screwy type systems.

[Oh, I guess you meant the latter: No. There are really fine type systems where the Curry-Howard correspondence is non-sensical. Just take the lambda-calculus where t = t -> t. You could still use it to encode a calculus where, say, all terms are closed (no free vars in the term.) But the type system would be useless logically, since everything can be proven. But such a type system could also be extended to prove other properties, say safety or multiple application checks, or whatever. You would still have a very usable type system from an operational view, but non-sensical from a Curry-Howard view.)]

My generalization is incorrect indeed. I should have said, "in a Curry-Howard setting", i.e. when you have types and there is an actual correspondence. I'd be interested in actual non-trivial examples of total functional languages not enjoying the correspondence though.

I really like his post too, and I do believe that total functional languages cannot have self-interpreters. But I have some problems reading Connor's post.

First, his post:

I'm sorry about the level of consternation this discussion seems to be
generating, so let me attempt to clarify my previous remarks.

The diagonalization argument which shows that any total language
misses some total programs is the usual one: Godel-code everything in
sight, then make the alleged universal program eat a twisted copy of
itself. It's the Epimenides/Cantor/Russell/Quine/Godel/Turing
argument. And it goes like this...

  Suppose we have a programming language in which all expressions
  compute to a value excluding bottom. For sake of argument, let's
  code expressions and values as natural numbers (an ascii source file
  is just a big number; so is a finite output). In particular, every
  function f from Nat to Nat which lives in the language is quoted by a
  code (quote f) :: Nat, and we know a total function which unquotes,
  executing a coded f at a given argument

    eval :: Nat -> (Nat -> Nat)

  with spec

    eval (quote f) x = f x
    eval _         _ = 0

  Given such a function, I can summon up its evil cousin, with spec:

    evil :: Nat -> Nat

    evil code = 1 + (eval code code)

  Now, if eval is total, so is evil. But if evil lies within our language,
  it will have a number. Without loss of generality, quote evil is a human
  number and that number is 666. So, we get

    evil 666
    = 1 + (eval 666 666)
    = 1 + evil 666

  which is plainly untrue.

  Hence evil is a total function which is not expressible in the language
  (so eval better not be expressible either).

Of course, for any language of total functions, its Halting Problem is
trivial, but that's beside the point.  There is no largest class of
recognizably terminating programs, because no such class can include
its own *evaluation* function, which is by definition terminating.
Given a total language L, we can always construct a strictly larger
language L', also recognizable, which also includes the eval function
for L.

Meanwhile, back in the cafe, why should Haskellers give a monkeys? Two
reasons: one pertinent now, one potential.

Firstly, when we make (or Haskell derives) recursive instance
declarations, we might like to know that

  (1) the compiler will not go into a spin when attempting to compute the
        object code which generates the dictionary for a given instance
  (2) the code so generated will not loop at run-time

You might argue that (1) is not so important, because you can always
ctrl-C, but (2) is more serious, because if it fails, you get the
situation where the compiler approves your program, then breaks it
by inserting bogus code, promising to deliver an instance which does
not actually exist.

To guarantee these properties, we essentially need to ensure that the
instance declaration language is a terminating fragment of Prolog. The
various flags available now are either way too cautious or way too
liberal: what's a suitable middle way? There is no most general choice.

Secondly, might it be desirable to isolate a recognizable sublanguage of
Haskell which contains only total programs?  Pedagogically, Turner argues
that it's useful to have a `safe' language in which to learn.
Rhetorically, making bottom a value is just sophistry to hide the fact
that looping and match failure are pretty bad side-effects available
within an allegedly pure language---preferable to core-dumps or wiping
your hard drive, but still bad. Logically, if you want to show a program
is correct, it helps if you can get its totality for free. Pragmatically,
there are fewer caveats to optimizing bottomless programs.

As we've seen, such a sublanguage (perhaps called `Ask', a part of Haskell
which definitely excludes Hell) cannot contain all the angels, but it
certainly admits plenty of useful ones who can always answer mundane
things you might Ask. It's ironic, but not disastrous that lucifer, the
evaluation function by which Ask's angels bring their light, is himself an
angel, but one who must be cast into Hell.

Yours religiously

Conor

Let's start with his specification of the eval function. The type says that it takes a natural number, and another one, and returns a natural number. However, the function matches on "quote f". Am I supposed to assume that "quote f" is a natural number?

[Hmm, forget it, on second thought, I guess it is short-hand for: quote f is the the function encoded by the natural number which is passed as an argument.]

[Yep, he is right, it is a classic diagonalization argument. Nice proof.]

That is exactly what I was looking for. It's frustratingly nice, I can't argue with it at all, as much as I would like it not to be true.

Intuitively I tend to agree.
After all, a total PL is not obliged to encode all functions from N to N (as there are uncountably many of them).
So it just might be possible to encode eval() while impossible to encode evil().

I would love to see more concrete examples or proofs, though :)

If you're allowed to treat eval as a special form, then it's not very hard to accomplish. For a trivial example, take your favorite language of total functions N->N and add a distinct program special form that evaluates to the eval function. If you try to encode the eval function using general purpose facilities, then you run into the barrier described in this thread. The "using general purpose facilities" is an important distinction, because I think it would be useful to have a strong total language which is capable of implementing implementing variations of itself that are just as powerful as itself (and could in turn re-implement it). I've seen this dismissed as impossible, but I don't think that's right.

I've seen this dismissed as impossible, but I don't think that's right.

The diagonalization argument says that no total language can have eval. It doesn't matter whether it's a user-written program or a gift from God himself. The only requirement is that the language be able to express the evil program in terms of the presumptive eval:

evil :: Nat -> Nat

    evil code = 1 + (eval code code)

I would not expect every program in a total PL to accept just anything, only anything of the corresponding type.
It may be possible that typing saves us from this proof in the similar way it saved from Russel's paradox.
Intuitively, would you expect any program to accept its own typed representation as input?

Then again we will have to deal with the other branch of this discussion (Goedel via Curry-Howard)...

Then again we will have to deal with the other branch of this discussion (Goedel via Curry-Howard)...

I've worked out some of the details for a more sophisticated system than my example in this thread, but I don't go through Curry-Howard. My guess is that it's just a matter of carefully tracking exactly what these propositions being strung together say. The point of my initial post in this thread was that the results in this area are precise and it's easy to go wrong with informal reasoning.

Nobody picked up Andris' idea, which seems to me to be clearly workable.

Consider the following tower of underspecified languages, following The Concept of Truth in Formalized Languages:

• T₀: A PCF-like language with only primitive recursion and with two additional datatypes, Maybe σ as per Haskell, and Sexp of quoted code that include all programs of T₀ plus infinitely many constants eval_n,σ that will later be associated with the type Sexp → Maybe(σ);
• T_n+1: T_n plus eval_n,σ, that accepts Sexp s and yields Nothing, if s is either not a closed program in T_n or not of type σ, or yields Just v, where v is the value of the expression described by s;
• T_ω is the union of all the languages T_n

There are gaps in this, but I'm pretty sure that they can be filled in so that T_ω is a total functional language, where each program in the language has an evaluator. Because there is no evaluator that can evaluate a program containing itself, the diagonalisation argument does not work.

I'm sure I've seen references for the idea of towers of evaluators in the lisp literature; maybe this argument has been made there.

Postscript — I know why this construction seems so familiar: it is not from lisp, but instead is closely analogous to predicative universes in Martin-Löf's type theory, where T_n is type theory with n universes, and the constants eval_n,σ are the recursors over the universes. MLTT has a much richer theory of constructions than what I sketched above, and its rewrite theory satisfies the weak head normal form property, giving a fully worked out, rich formalism along the lines I sketched.

Something very similar to this was discussed lower in this thread here. As you note, Tω does not contain an evaluator for Tω.

I interpreted Andris' comments to be more along the lines of developing a type system to implement the gameplan I've discussed elsewhere in this thread, where you do end up with an actual self-evaluator for your language. In this approach, the type restrictions are not on what you're allowed to pass in to the evaluator, but are on what you're allowed to do with the results.

I'd started writing this up previously, but then got pretty busy. I may try to finish this out soon.

It doesn't matter whether it's a user-written program or a gift from God himself.

My point was that if you can construct 'eval' out of general purpose constructs, then surely any reasonable type system will let you construct 'evil' too. On the other hand if 'eval' is a special form or has a special type, it's very easy to prevent 'evil' from being well formed or typed. Doing this in a way that allows useful modification of the core language requires more care, but isn't impossible.

Also, I gave a counterexample! Did you find something wrong with it? Here it is in more detail:

Take your favorite langauge of (total) functions Nat->Nat, for example all functions that can be proven total in ZFC or constructed in coq. Enumerate the valid programs in this language starting from 1, reserving program 0 for a special program meaning 'self-intepreter'. Let pair :: Nat -> Nat -> Nat be some bijection of pairs of naturals with the naturals, and let simple-eval :: Nat -> (Nat -> Nat) take m to the function defined by the mth program (m > 0) in your original total language. Define:

eval (pair m n) =
    eval n if m = 0
    simple-eval m n otherwise 

This definition is total if n < pair 0 n for all n (basically we want to avoid accidentally encoding an infinite chain of self-interpreter calls). But that's a mild condition on pair. For example, define pair m n by the table:

 n  0  1  2  3  4  5
m +-----------------------
0 | 1  3  5  7  ...
1 | 0  2  6 12 20
2 | 4  8 14 24        
3 |10 16 26 ...
4 |18 28
5 |30
  |... 

So, here we have a language which represents a large class of functions Nat->Nat, with every represented function total, and it includes an encoding of its own self-evaluator.

EDIT: Oops. This was not an appropriate place to attach this message. I agree with Matt M.

There are two assumptions that are made in this proof.
1) eval can be constructed
2) evil can be constructed (from eval).

Your proof shows that we reach a contradiction from these assumptions, which means that they can't both be true. This does not imply that 1) is the false assumption. Your argument is convincing, certainly, but is not a proof. It is not clear that 'any reasonable type system will let you construct evil too'. In fact, any reasonable type system for a total language will reject it (it is, after all, non-total).

The language in question isn't limited to being anything like a conventional language, either. Consider the class of C programs that run in less than 1K of memory (space for code, data, and program counter), augmented with a primitive 'eval' construct. I'm going to refer to the entire contents of memory as the state of the program. We can turn this into a total language by changing the semantics a bit.
- include a value _|_ that means that "eval x" attempted to use more than 1K space, or attempted to enter an infinite loop
- evaluate a program p as follows:
-- initialize an empty "seen" list
-- to execute the "next" command (say, n) of p:
--- if the state is equal to any state on the seen list, return _|_
--- save the state to the seen list
--- if n attempted to allocate more memory than is available, return _|_
--- if n is an eval instruction, instantiate a new interpreter that uses the current seen list as its initial seen list
--- otherwise, execute the instruction normally

So intuitively, this language prevents a program from repeating the same state twice, and produces an abort value (_|_) if this ever happens. A program enters the same state twice if and only if it doesn't halt, so only total functions can be defined in this language.

Of course, we can't write every total computable function in this language (by the space hierarchy theorem) - this is what the really interesting issue is.

It is not clear that 'any reasonable type system will let you construct evil too'

The class of "reasonable type systems" is pretty nebulous, so this claim obviously isn't something I can prove. But it does seem somewhat clear to me that if I can construct a function f :: Nat -> Nat through ordinary arithmetic means, then any type system that prevents me from creating the function \n -> 1 + (f (pair n n)) has some pretty serious limitation. Your space limited C example has the problem that it can't represent large natural numbers.

Of course, we can't write every total computable function in this language (by the space hierarchy theorem) - this is what the really interesting issue is.

I think it's settled that you can't have a total language in which every total computable function can be written.

Well I agree that a type system that accepts f and rejects \n -> 1 + f (pair n n) is odd, I don't know that it is very limiting, because it depends on the choice of f. So \n -> 1 + f (pair n n) could be well-typed for all well-behaved 'f's (the type of f shouldn't be exactly Nat -> Nat... it needs to reflect in some way it's "well-behaved"ness).

You're right that space-limited C can't represent large natural numbers. There's also a finite number of space-limited C programs. So your example has (many) more definable functions than space-limited C. It may be possible to fix these problems, but I don't think it will get us anywhere new.

I would be interested to see a proof that you can't have a total language in which every total computable function can be written*. I've seen the proof that we can't add "basis" functions to the primitive recursive functions, take the closure under composition and primitive recursion, and get the set of all total computable functions - but this isn't the same thing. I suspect that you're right about this, though. Do you have a reference?

* EDIT - and which has a computable interpreter.

Well I agree that a type system that accepts f and rejects \n -> 1 + f (pair n n) is odd, I don't know that it is very limiting, because it depends on the choice of f. So \n -> 1 + f (pair n n) could be well-typed for all well-behaved 'f's (the type of f shouldn't be exactly Nat -> Nat... it needs to reflect in some way it's "well-behaved"ness).

But we're talking about an f constructed from simple arithmetic operations like multiplication, addition, comparisons, and simple loops/branches. How are you going to decide that some additional simple operation makes a function ill behaved? I don't think that's a tenable approach. If you have a function N->N and you compose it with a simple arithmetic operation, you should get out another one.

Do you have a reference?

See the reference Klaus Ostermann provided later in this thread - I think that addresses your question.

The "well-behavedness" has to do with the function's use of eval (I'm assuming that eval is provided as a primitive). The functions that are constructed from simple arithmetic operations are the primitive recursive functions. They are the most well behaved functions (say they have rank 0). Then functions that call eval on rank 0 functions are rank 1 functions. And so on. (These ranks form a type system, which looks a lot like the original type system - Russells). Does this approach actually work? Probably not. But I'm not sure why. And if we can prove that it doesn't work, that doesn't mean that there isn't some type system that fixes our problems.

Klaus Ostermann's reference was the standard recursion theory proof. It assumes that functions definable in our language are closed under composition and primitive recursion, which need not be the case (for instance, using the rank system above, d(x) = eval(x, x) is not well-defined, even though it is defined by composition from eval and the identity function (which is good, because d isn't total)).

The "well-behavedness" has to do with the function's use of eval (I'm assuming that eval is provided as a primitive).

Then we weren't on the same page. Reread what I've written where you've quoted me - I was specifically talking about functions that could be constructed arithmetically (edit: in other words, no calls to a primitive 'eval') in those places.

Your rank scheme will work fine, but at each point you've only ever established an evaluator for the rank below. To have a self evaluator you'll need to do something as you pass to a limit.

It doesn't matter whether it's a user-written program or a gift from God himself.

My point was that if you can construct 'eval' out of general purpose constructs, then surely any reasonable type system will let you construct 'evil' too. On the other hand if 'eval' is a special form or has a special type, it's very easy to prevent 'evil' from being well formed or typed. Doing this in a way that allows useful modification of the core language requires more care, but isn't impossible.

The first post got it right. The diagonalization argument is a proof by contradiction. Reasoning: if eval exists, then so does evil, therefor eval cannot exist.

That's a classical logic argument. You can also try to prove constructively that eval does not exists. That's easy (I think). Just prove that there are an uncountable number of total functions (from N to N). You'll actually end up just giving another diagonalization argument.

Reasoning: if eval exists, then so does evil

Reasoning: flawed

At the very least, additional care is warranted in this statement. Details can be found in this thread. A good start would be to read the paragraph of mine that you just quoted :).

Ok. I didn't really get your posts. But that's ok, I sometimes don't even get my own posts ;-).

My point was that if you can construct 'eval' out of general purpose constructs, then surely any reasonable type system will let you construct 'evil' too.

So you actually agree with the proof here? For all settings where eval exists, evil is constructable, thus it cannot exist? And I don't really get your statement (for the proof by contradiction it is not necessary to prove it exists. Actually, this would be impossible since it is a proof that eval cannot exist)

On the other hand if 'eval' is a special form or has a special type, it's very easy to prevent 'evil' from being well formed or typed. Doing this in a way that allows useful modification of the core language requires more care, but isn't impossible.

Yeah well, I don't know about the latter.

Whatever, I guess you're just throwing ideas around. Great throw ;-)

So you actually agree with the proof here? For all settings where eval exists, evil is constructable, thus it cannot exist?

No. I disagree that evil is necessarily well-formed or well-typed. The paragraph of mine you quoted says that if eval is constructible (rather than god-given), then I agree evil ought to be well-formed, and the proof goes through. As I've shown in a trivial counter-example, though, a total language can have a restricted eval construct that lets one write a self-interpreter from within the language. In my example, it can only be used in one circumstance (as the sole construct), but I claim (without evidence presented here) that this can be usefully generalized.

I guess.

A countability argument is irrelevant here. There are (trivially) more partial "functions" than total ones, yet no one says you can't make eval in a Turing-complete language. There are only countably many computable functions, total or not, and eval isn't even required to be able to produce all of those except in the Turing-complete case.

A countability argument is irrelevant here.

Ouch, true and not true. A "classic" diagonalization argument is actually almost always a hidden (un-)countability argument.

There are (trivially) more partial "functions" than total ones,

True [Sorry, not true, depends on the setting. What kind of functions are we talking about?]

yet no one says you can't make eval in a Turing-complete language.

Uh? [???]

There are only countably many computable functions, total or not,

Yeah. That's actually one way to undermine the argument/shift to a language where a self-interpreter can exist. Is the set of total functions from N to N, the set-theoretic set of total functions, or is it the set of expressible total functions from N to N [in a certain language]? That's a big difference. [Hmm, I got something wrong here, whatever, don't feel like thinking too much about it. I guess in the general case not all total functions from N to N are expressible, and neither is eval, and some languages might exist where the set of [expressible] total functions from N to N is sufficiently small to have a self interpreter.]

and eval isn't even required to be able to produce all of those except in the Turing-complete case.

Not true, a self interpreter must be able to interpret all functions in the language. How can it otherwise be a self interpreter? [Me bad, misread the definition of eval as the definition of a self-interpreter, which is wrong. You're right, it only needs to be able to interpret itself for the argument.]

Too much bullshit in the above post. Somebody who teaches this might want to respond.

I haven't taught this stuff in years, but anyhow:

A countability argument is irrelevant here.

Ouch, true and not true. A "classic" diagonalization argument is actually almost always a hidden (un-)countability argument.

No. Turing's Entscheidungsproblem refutation shows nonrepresentability of the halting problem. In fact, if you consider turing degrees (where you allow progressive expansions of the class of recursive functions by "jumps" allowing solvability of the halting problem for lower degrees), you get a tower of sets of non-recursive functions, all of which have halting problems, and all of which are countable in size.

There are (trivially) more partial "functions" than total ones,

True [Sorry, not true, depends on the setting. What kind of functions are we talking about?

The set of partial and total functions have the same cardinality, whether we consider the uncountable space Nat=>Nat, or restrict to any particular Turing degree.

and eval isn't even required to be able to produce all of those except in the Turing-complete case.

Not true, a self interpreter must be able to interpret all functions in the language. How can it otherwise be a self interpreter?

I think you misunderstood Derek here.

Yeah, I misunderstood a lot of stuff, so it's great it is clarified. (This really isn't my turf: I like logics, PLs, automata theory and type-theory but usually stay away from Turing arguments)

[Scrapped some nonsense]

Still, just a hunch. Are all total languages with self-interpreters finite in size? [Ah forget it, got it wrong again. Grmbl ;-)]

Indeed, my use of the incompleteness theorem should be restricted to the case of a total functional language having an associated proof theory through Curry-Howard. I was also assuming the system to be sufficiently expressive. The ones of Dan Willard do seem to fit an interesting spot. I'm a bit sceptic though, as it seems in these systems you don't actually prove consistency inside the system but you just add it as an axiom and prove relative consistency of the whole in a larger system (or is that in the same system?). I must be missing something here.

There's two notions of consistency going on here: internal consistency, which is given by the proof of the consistency sentence within the self-verifying system, and external consistency, which is given by a relative consistency proof within primitive recursive arithmetic showing that consistency of some system of regular arithmetic entails consistency of the self-verifying system. There are a family of self-verifying systems, of arbitrarily strong consistency strength, because it is possible to add any valid pi-0-1 sentence of arithmetic to Willard's systems; consistency sentences themselves being pi-0-1.

The proof of the consistency sentence is trivial in Willard's systems, because they are indeed just added as axioms. But the intuition for the way Willard formalised consistency comes from an intuition about how provability of consistency is the same thing as saying that certain tableaux searches terminate.

There might be a function algebra corresponding to these systems, but it could not be based on the simply-typed lambda calculus. If I were to go looking for one, some system of light linear logic would be the place I would start.

If this is meant to refute the point I made above, that the existence of self-verifying theories shows a gap in the argument showing the impossibility of self-interpreters in total languages, then it doesn't work. Diagonalisation is the algorithmic core of Goedel's argument, and Willard's systems avoid representing the diagonal construction by not being able to prove the totality of the necessary functions because multiplication is not provably total. If we had a function algebra corresponding to Willard's system, this standard result would not go through for it.

As I say, I doubt the existence of such a system. But it's clear the argument has a rather messy hole in it.

You cannot make a total functional language that includes an evaluator for the whole language, ...

So which of these words excludes the counterexample I presented in this thread? "functional"? "includes"?

Explicit stratification is IMO the wrong way to go about things. Imagine you want to put out a language that can evaluate itself (or maybe variations on itself), and so you cook up this stratification scheme and put the first language at level 1e24. Every time someone nests deeper into eval, they lose a level. With such a high starting number, you can spin recursing deeper into eval until the sun burns out and (barring compiler optimization) never reach bottom. But the choice of 1e24 (or any choice) feels like a hack, and we can do better.

To start off, note that each of your eval functions is just the restriction of some external eval function that can evaluate any language term. So instead of thinking of this as a hierarchy of evals, think of it a single typed eval that requires its argument to belong to some level of the stratification. Next, instead of requiring explicit annotation of the stratification level of each term, do inference to establish that some valid assignment of levels is possible (similar to how universes are inferred in Coq). You may want something more fancy that allows level-polymorphism, but that's a separable issue.

With this change we don't need to pick some ad hoc number of levels to our stratification, and in fact our eval function is now a proper self-evaluator since adding one more level of eval will not ever add a cycle to our graph. In fact, one might describe what we've constructed as "a total functional language that includes an evaluator for the whole language".

If you say "eval" is a "special" form, then it really isn't having "eval" as part of the language. Similarly, if you add consistency as an axiom, you can't say that you can prove consistency in the system, because you just extended it. If you resort to universes/stratification, even with clever tricks like universe inference that almost make you to think you work with Type:Type, you're still missing the next level. E.g., consistency of Coq with n universes can only be proven in Coq with at least n+1 levels, at least that's what I learned.
Can we settle that it's not possible in a sufficiently expressive total functional programming language to have its own evaluator as a regular, explicitely constructible term?

Which example?

Well, now I've outlined two - in the post you just replied to and here. In both cases, eval is a special form or has a special type. Neither of these examples provide a compelling language design, due to the extreme restrictions they place on the use of eval. Their purpose is to serve as counterexamples, but I still claim useful variants are possible.

If you say "eval" is a "special" form, then it really isn't having "eval" as part of the language ...

And why not? Are you going to define "part of the language" now?

I find your analogy to Coq flawed in the respect that in Coq, even with the universe inference trick, you can't prove the consistency of Coq. Whereas, the trick does allow a self-evaluator for a language.

Just to be clear, here's the informal definitions I'm using:
- Functional: Function terms define pure functions
- Total: Every well formed function term defines a function that terminates (and is even computable) on every input
- Self-evaluator: A function capable of evaluating every legal (well-formed) program that produces the result of evaluating that program

Can we settle that it's not possible in a sufficiently expressive total functional programming language to have its own evaluator as a regular, explicitly constructible term?

Sure. As I've said elsewhere in the thread, I consider that settled.

In GHC, this type is inhabited only by bottom:

data Void


In total languages, this type must be uninhabited, I believe.