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
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
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 ev
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!
>
#x27;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,
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:
---
{-#
