Hi TP, You bring up a few interesting points in your email. (A note to those who have visited this playground before: to keep things sane, let's just pretend that the kind # doesn't exist. Of course, if you don't know about kind #, then you're a step ahead of the rest of us! While you're at it, forget about the kind `Constraint` also.) * 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 *. 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`. (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.]) When I am programming with promoted data constructors, I often find the following definition useful:
data Proxy a = P
With PolyKinds, the type constructor Proxy has kind `forall k. k -> *`. So, if we need to quickly make a value associated with the type 'Zero, we can just use `Proxy 'Zero`. Because Proxy is kind-polymorphic, this works just fine. 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. We also have the nice maxim that every type that appears to the right of a :: must be of kind *. * Singletons are a useful mechanism for type-level programming. But, there is more to singletons than just defining `Sing` as you have. Instead, you should import the definitions from GHC.TypeLits, which comes with singleton definitions for the built-in Nat and Symbol kinds. One drawback of the built-in Nat and Symbol kinds is that they are not recursively defined; you can't pattern-match on them. So, if you want your own Nat, you can define a singleton like this:
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! * 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 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! Richard -----Original Message----- From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of TP Sent: 31 May 2013 13:58 To: haskell-cafe@haskell.org Subject: [Haskell-cafe] question about "singletons" Hi all, Following a discussion on Haskell Cafe some time ago (1), Roman C. wrote: """ On the other hand, the type 'Succ 'Zero has kind 'Nat and doesn't have any inhabitants — only types of kind * do. """ Indeed, this is what seems to occur in the following example: ----------------------- {-# LANGUAGE DataKinds #-} data Nat = Zero | Succ Nat deriving ( Show, Eq, Ord ) main = do let one = undefined :: 'Succ 'Zero print one ----------------------- We obtain an error (ghc 7.6.2): ----------------------- Kind mis-match Expected kind `OpenKind', but `Succ Zero' has kind `Nat' In an expression type signature: Succ Zero In the expression: undefined :: Succ Zero In an equation for `one': one = undefined :: Succ Zero ----------------------- (note that the error is slightly different in the HEAD version of GHC (2)). Is it related to the sentence "As bottom is an inhabitant of every type (though with some caveats concerning types of unboxed kind), bottoms can be used wherever a value of that type would be. " found at address (3)? Here we have a non-* kind, such that bottom would not be an inhabitant of ('Succ 'Zero). Why is this so? This seems to be an assumed choice (4), but I would like to understand the reason for this design, which makes necessary to use singletons, as explained at (4). Now, if I use a singleton to make my example work, I obtain an error when trying to make the type (Sing a) an instance of Show: ----------------------- {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE StandaloneDeriving #-} data Nat = Zero | Succ Nat deriving ( Show, Eq, Ord ) data Sing :: a -> * deriving instance Show (Sing a) main = do let one = undefined :: Sing ('Succ 'Zero) print one ----------------------- The error is simply: ----------------------- test_noinhabitant_corrected.hs: Void showsPrec ----------------------- Why? Thanks, TP References: ---------- (1): https://groups.google.com/forum/?fromgroups#!topic/haskell-cafe/AltmX5iCFi8 (2): ----------------------- Expected a type, but ‛Succ Zero’ has kind ‛Nat’ In an expression type signature: Succ Zero In the expression: undefined :: Succ Zero In an equation for ‛one’: one = undefined :: Succ Zero ----------------------- (3): http://www.haskell.org/haskellwiki/Bottom (4): http://hackage.haskell.org/trac/ghc/wiki/TypeNats/Basics """ Both numeric and symbol literal types are empty---they have no inhabitants. However, they may be used as parameters to other type constructors, which makes them useful. """ """ A singleton type is simply a type that has only one interesting inhabitant. """ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe