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. """
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
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 --
On Jun 1, 2013, at 8:18 PM, TP wrote:
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?
There are three explanations I can think of here: - What would the inhabitants of 'Zero be, for example? Not Zero, because Zero is of type Nat, not of type 'Zero. So, something else would have to be in type 'Zero… but what? The only thing I can think of is bottom. If a type's only inhabitant is bottom, then a term of that type is inherently uninteresting, as it can be only one thing, and that thing is inherently uninteresting, as I elaborate below. - One of the interesting details of Haskell is that (->) is just another type constructor. It's a little more baked in than, say, Maybe, but the syntax of the language treats (->) as the same as Maybe. Specifically, (->) has a kind, and it is (* -> * -> *). That is, (->) takes two concrete types and produces a third concrete type. This is as we expect. (Again, ignore strange things like the kind # here.) This "ordinariness" of (->) is why, for example, we can define a Monad instance for ((->) r), which is of kind (* -> *), as Monads must be. If expressions of types of non-* kinds could be allowed, we would have to do something much stranger with the kind of (->) to be able to pass such expressions between functions. Pure kind polymorphism wouldn't quite work, because we want to prohibit "non-concrete" types (as TP has used the term "concrete") such as Maybe, being on either side of an arrow. - The type system of Haskell is based on theoretical work that resolutely assumes that types of non-* kind are uninhabited. While it is possible to stretch imagination to allow types like 'Zero to be inhabited, the designers of Haskell would have a lot of work to do to prove that the new language is actually type-safe.
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 `*`?
I hope I've addressed this above. Technically, yes, we could have a different definition of undefined, but it would fly in the face of a lot of theory about type-safe programming languages. This is not to say that such a thing is impossible, but just perhaps imprudent.
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?
Bottom is inherently uninteresting, because you never see bottom in running code, and you can never know where bottom is lurking (other than after your program has crashed). Technically, bottom should have this definition (which is perfectly valid Haskell):
bottom :: a bottom = bottom
In other words, bottom is infinite recursion -- a term that never finishes evaluating. Let's say a show method tried to print its argument and its argument is bottom. Well, that method would have to examine its argument and would immediately fall into an infinite loop. Bottom is a little like Medusa when you have no mirrors around. Once you look at it, it's too late. In Haskell, we don't usually use bottom in this way; we use undefined. undefined masquerades as bottom, but instead of forcing a running program into an infinite loop, looking at undefined causes a running program to instantly terminate. This is generally much nicer than an infinite loop, but this niceness is simply a convenience that the compiler gives us. From a theoretical point of view, a hung program is much cleaner. To recover the consistency of the theory, Haskell provides no way to recover from a discovery of undefined in a running program. (GHC has implemented an exception that allows exception-handling code, written in the IO monad, to catch a use of undefined, but I would be highly suspicious of code that used this feature.) So, all of this is to say that undefined is entirely uninteresting, as your program can never know when it encounters one without dying.
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).
These are fine reasons to choose a language, especially if you're just starting out. In the end, programming is a practical pursuit, and these are very practical reasons. It can be easy for us theorists to overlook this very important point. Richard
Thanks Richard, now I have my answers. Richard Eisenberg wrote:
- The type system of Haskell is based on theoretical work that resolutely assumes that types of non-* kind are uninhabited. While it is possible to stretch imagination to allow types like 'Zero to be inhabited, the designers of Haskell would have a lot of work to do to prove that the new language is actually type-safe. [...] Technically, yes, we could have a different definition of undefined, but it would fly in the face of a lot of theory about type-safe programming languages. This is not to say that such a thing is impossible, but just perhaps imprudent.
Ok, this is a convincing reason to admit that non-* kinded types must be uninhabited, even by undefined.
Bottom is inherently uninteresting, because you never see bottom in running code, and you can never know where bottom is lurking (other than after your program has crashed). [...] So, all of this is to say that undefined is entirely uninteresting, as your program can never know when it encounters one without dying.
Ok: Haskell refuses to show "undefined" for a type of kind * if it has not another inhabitant, because the type is deemed uninteresting.
Technically, bottom should have this definition (which is perfectly valid Haskell):
bottom :: a bottom = bottom
In other words, bottom is infinite recursion -- a term that never finishes evaluating. Let's say a show method tried to print its argument and its argument is bottom. Well, that method would have to examine its argument and would immediately fall into an infinite loop. Bottom is a little like Medusa when you have no mirrors around. Once you look at it, it's too late.
In Haskell, we don't usually use bottom in this way; we use undefined. undefined masquerades as bottom, but instead of forcing a running program into an infinite loop, looking at undefined causes a running program to instantly terminate. This is generally much nicer than an infinite loop, but this niceness is simply a convenience that the compiler gives us. From a theoretical point of view, a hung program is much cleaner. To recover the consistency of the theory, Haskell provides no way to recover from a discovery of undefined in a running program. (GHC has implemented an exception that allows exception-handling code, written in the IO monad, to catch a use of undefined, but I would be highly suspicious of code that used this feature.)
Interesting, I will remember that. Thanks TP
participants (2)
-
Richard Eisenberg -
TP