[Haskell-cafe] question about "singletons"

[TP]

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
--