Lambda the Ultimate

In a language that enforces a separation between data and codata, it seems like (with a Haskell-esque syntax):

data Silly = Very Silly

should be statically disallowed, since the resulting type Silly is uninhabited.

First, is this intuition correct? Or does defining types of this kind have some utility?

Second, what's the dual concept for codata? I think that if we are ruling out Silly as uninhabited, we should probably also rule out both of:

codata CoSilly = Quite CoSilly
codata CoSilly2 = Just Int | Quite2 CoSilly2

for a related reason.

I'm thinking that the rule is something like this: A data definition must contain at least one alternative which is not recursive. A codata definition must not contain any alternative which is "only recursive" (meaning that it is a product of only recursive references to the codata type being defined).

Am I even close? I am unaware of the correct terminology here, because searching is getting me nowhere. I've read a few overviews of total functional programming, including Turner's "Total Functional Programming", and learned of other syntactically reasonable data type definitions that have to be rejected because the reintroduce bottom, but didn't find a discussion of types of this kind (which seem merely useless in the data case, but also seem like an enemy of productivity proofs in the codata case).

I'm pleased to announce the Jane Street Summer Project for 2009. The goal of the JSSP is to make functional programming languages into better practical tools for programming in the real world. To do that, we will fund students over the summer to work on open-source projects which aim at improving the practical utility of their favorite functional language.

The JSSP is a follow-on to last year's OCaml Summer Project. A key difference this year is that we are opening up the project to proposals in languages other than OCaml (although we expect to maintain a focus on OCaml projects.) There are also some changes to the funding structure that are particularly relevant for projects located in the US.

If you want to find out more, you can look at the JSSP blog and at the project FAQ

We're looking forward to a great and productive summer, and we hope some of you come along for the ride!