Thanks Richard for your detailed answer. Please find my reply below (note I have rearranged some of your paragraphs). Richard Eisenberg wrote:
* Types at kind other than * do not have any inhabitants -- in fact, some people would hesitate to call type-like things at kind other than * types! (Though, I will call these things types because there's just not another good moniker. Type-level data? Type indices? Type constructors? All are somehow lacking.) Let's start with a more familiar example: Maybe. To form an inhabited type, we must apply Maybe to something. So, we can have values of type (Maybe Int) and values of type (Maybe Bool), but not values of plain old type (Maybe). That's because Maybe has kind (* -> *), not kind *. Another way to say this is what I said above: Maybe requires something (something at kind *, specifically) to become a proper, inhabited type. And, even though we say `undefined` exists at all types, that's a bit of a simplification. `undefined` exists at all types _of kind *_. The full type of `undefined` is `forall (a :: *). a`. Thus, we can't have `undefined` at Maybe, because Maybe is not of kind *. [...] (When I first wandered down this road, I was confused by this too. Part of the confusion was somehow deciding that * had some vague association with * as used on the command line -- a notation that could expand to something else. This is totally, completely, and in every way False. In at least one other programming language [Coq], what Haskell spells * is spelled `Type`. [Well, almost.]) [...] Why have the restriction that kinds other than * are uninhabited? Well, for one, (->) would be a strange beast indeed if other types could be inhabited. What would be the kind of (->)? I don't want to think about it.
In other words, bottom can be an inhabitant of a concrete type, not a type constructor, which I can understand. But a type of kind Nat is a concrete type, so why bottom cannot be an inhabitant of this type?
We also have the nice maxim that every type that appears to the right of a :: must be of kind *.
This is a rule set into Haskell, but why not a type of kind Nat, which is a concrete type?
This argument extends directly to where we have types derived from promoted data constructors. The type 'Zero has kind Nat, not *, so 'Zero is uninhabitable, even by `undefined`.
I can understand that if indeed the definition of undefined is `forall (a :: *). a` (see above), undefined is not suitable to represent ”bottom” for a type of kind Nat. But I don't see why there cannot be a bottom in a type of kind Nat; isn't it more a limitation related to the Haskell definition of "undefined" that prevents "undefined" to be used to mean "bottom" in Haskell for a type of kind different from `*`?
data Proxy a = P [...] data SNat :: Nat -> * where SZero :: SNat 'Zero SSucc :: SNat n -> SNat ('Succ n)
Now, you can have values that are tightly associated with types. Yay!
Thanks for these definitions, which I have recorded in my notes.
* Why did you get that error with `show`? Because the `Sing` type you defined is uninhabited -- not because it has a funny kind, but because it has no constructors. So, when a `Show` instance is derived, the `show` method just fails -- GHC knows `show` at type `Sing` cannot be called because there are no `Sing`s. Then, when you subvert this logic by using `undefined`, the derived `show` method doesn't quite know what to do with itself.
I think I understand what you say, but I am not sure to understand the reason. For example, consider the trivial examples in part (1) of Post Scriptum below. We have a concrete type Foo clearly of kind `*`, so bottom (undefined in Haskell) is an inhabitant of Foo. Why should I be compelled to add another inhabitant (a data constructor) to get bottom printed? Bottom existence is independent from other inhabitants, isn't it?
I hope this helps! I do have to say I'm impressed, TP, by your intrepid path of discovery down this road. You're asking all the right questions!
Thanks Richard. I am discovering things in Haskell every day. In the last weeks, I have especially been amazed by all the extensions in GHC compared to Haskell 2010 standard. In fact, there are two things: Haskell, and GHC (I don't know Hugs at all). A textbook on GHC is perhaps missing, using advanced extensions and comparing with pure Haskell. I did not follow type or category theory lectures at all, I am an electrical engineer in France interested in Physics during my leasure time. To make some complicated calculations, I need a Computer Algebra System with certain features that does not exist yet. Rather than adapting an existing CAS to my needs (Maxima, Axiom, Sympy, etc.), I thought that it was a good occasion to learn a language as OCaml or Haskell (and so to code in a clearer way than in Python for "serious" programs, through strong typing). I began with OCaml, but switched rapidly to Haskell (for reasons that seems derisory to you: mainly the syntax closer to Python that I know well, the possibility to print values at data level automatically by deriving Show instances, and the GREAT wiki of Haskell). I don't regret my decision: it seems to me that people behind GHC are very smart, with GHC I feel that we have a good compromise between type theory research (where I am often lost, even if I am interested in it) and practical programming. Concerning our previous exchanges, in particular the possibility to have a list of `Tensor order` in a list at type level to mean the independent variables on which a function (in practice, another Tensor) is depending, I think I am not enough mature to use this approach. With an heterogeneous list at data level, I know that I will be able to add and remove independent variables from the lists during the calculations (for example, to solve equations - things are not clear in my head at this time). With a list at type level, it seems to me that things are "frozen", as with a tuple. For the time being, I will go on like that, and will look behind at some time, for sure. Thanks, TP PS: (1): The code: -- data Foo deriving Show main = do let bottom = undefined :: Foo print bottom -- yields: -- Can't make a derived instance of `Show Foo': `Foo' must have at least one data constructor Possible fix: use a standalone deriving declaration instead In the data declaration for `Foo' -- Now, if we use standalone deriving instead: -- {-# LANGUAGE StandaloneDeriving #-} data Foo deriving instance Show Foo main = do let bottom = undefined :: Foo print bottom -- The error is then obtained at runtime instead of compilation time, this is the same as in my original post: -- test_show_without_data_constructor_deriving.hs: Void showsPrec --