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 -- _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe