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
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!
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
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
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:
---
{-#
...@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
