Re: [Haskell-cafe] question about singletons
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] question about singletons
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
Re: [Haskell-cafe] question about singletons
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
Re: [Haskell-cafe] question about singletons
On 6/1/13 3: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? The technical term is proper type. That is, types are used as a way of characterizing collections of values; but, all sorts of things can exist at the type level. For lack of a better name, we call everything at the type level a type, in order to distinguish them from things at the value level or kind level, etc. But in order to be a *proper* type, a type-level expression must serve to characterize a collection of values. Types of kind * are proper types, because they serve to characterize collections of values. Types of other kinds are not proper, since they do not characterize collections of values. Thus, we can't say: undefined :: (-) nor: undefined :: Maybe because (-) and Maybe are not proper types. It doesn't make sense to say that some value (like undefined) belongs to the collection of values characterized by them, since there is no such collection to belong to! The same sort of thing holds for datakinds. Types of kind 'Nat are not proper, in exactly the same way that types of kind *-* or *-*-* are not proper. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[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
Re: [Haskell-cafe] question about singletons
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-boun...@haskell.org
[mailto:haskell-cafe-boun...@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
