[Haskell-cafe] question about "singletons"
TP
paratribulations at free.fr
Sat Jun 1 21:18:25 CEST 2013
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
--
More information about the Haskell-Cafe
mailing list