Send Beginners mailing list submissions to
beginners@haskell.org
To subscribe or unsubscribe via the World Wide Web, visit
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
beginners-requ...@haskell.org
You can reach the person managing the list at
beginners-ow...@haskell.org
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Type * and * -> * (Galaxy Being)
2. Re: Type * and * -> * (Bob Ippolito)
3. Re: Type * and * -> * (Matthew Low)
----------------------------------------------------------------------
Message: 1
Date: Sat, 13 Mar 2021 00:18:26 -0600
From: Galaxy Being <borg...@gmail.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: [Haskell-beginners] Type * and * -> *
Message-ID:
<CAFAhFSWz47u8SRKB7LLYixWucG5pmmxe0LR=ss7vzezwx2n...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
I found this interesting page <https://wiki.haskell.org/Peano_numbers> at
Wiki Haskell. Confusing, however, is how it first establishes
data Peano = Zero | Succ Peano
It says
Here Zero and Succ are values (constructors). Zero has type Peano,
and Succ has type Peano -> Peano.
but then it breaks down each member further a few lines later
data Zero
data Succ a
and then says
Zero has kind *, and Succ has kind * -> *. The natural numbers are
represented by types (of kind *) Zero, Succ Zero, Succ (Succ Zero) etc.
Why is it giving two separate treatments and what is meant by the * and *
-> * ? There's something fundamental I'm missing.
If anyone knows of a really thorough and definitive *and *understandable
treatment of Haskell types, I'd appreciate it.
LB
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20210313/f3d48623/attachment-0001.html>
------------------------------
Message: 2
Date: Fri, 12 Mar 2021 22:52:13 -0800
From: Bob Ippolito <b...@redivi.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Type * and * -> *
Message-ID:
<CACwMPm-N5n1s1gOFKcG8DTYTbq=ss31wi=vuaarjpsauv0h...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
The first definition is only used as an analogy, it’s a way to represent
Peano numbers as values.
The second definition is only related to the first in that it uses the same
concept. It is not a breakdown of the first one, it is a completely
separate (and incompatible) way to represent Peano numbers at the type
level (and only as types, notice there are no constructors). You can not
define both of these in the same module with the same names.
In Haskell a kind is (basically) the type of a type. In modern GHC to make
it even more clear (and to free up * for type operators) you can say Type
instead of *.
Zero has the kind Type (or *) because it has no arguments, just like Zero
has the type Peano because the constructor has no arguments.
Succ has the kind Type -> Type because you pass it a Type as an argument to
get a concrete Type. Maybe also has the kind Type -> Type, as does [].
Generally, beginner Haskell doesn’t use any of this type level programming.
If this is a topic of interest, I recommend this book:
https://thinkingwithtypes.com
On Fri, Mar 12, 2021 at 22:19 Galaxy Being <borg...@gmail.com> wrote:
> I found this interesting page <https://wiki.haskell.org/Peano_numbers> at
> Wiki Haskell. Confusing, however, is how it first establishes
>
> data Peano = Zero | Succ Peano
>
> It says
>
> Here Zero and Succ are values (constructors). Zero has type Peano,
> and Succ has type Peano -> Peano.
>
> but then it breaks down each member further a few lines later
>
> data Zero
> data Succ a
>
> and then says
>
> Zero has kind *, and Succ has kind * -> *. The natural numbers are
> represented by types (of kind *) Zero, Succ Zero, Succ (Succ Zero) etc.
>
> Why is it giving two separate treatments and what is meant by the * and *
> -> * ? There's something fundamental I'm missing.
>
> If anyone knows of a really thorough and definitive *and *understandable
> treatment of Haskell types, I'd appreciate it.
>
> LB
> _______________________________________________
> Beginners mailing list
> Beginners@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20210312/34683842/attachment-0001.html>
------------------------------
Message: 3
Date: Fri, 12 Mar 2021 23:53:19 -0700
From: Matthew Low <m...@ualberta.ca>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Type * and * -> *
Message-ID:
<CAC=gTKzm1DqfmgRtPp4rXsTSJXFvya20J3TOeP1NyxMBM3QW=w...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
I can only answer some of your questions.
To start, perhaps an analogy would help: Kinds are to types as types are to
values. So in regards to the title of the thread, "Type * and * -> *" is
confused in that * and * -> * are kinds, not types.
That might not exactly make sense, but leaving it aside for the moment, to
two treatments are at different levels - data and type level. I'll try to
be explicit as to what are type constructors and what are data constructors
by appending T to the type constructors:
data PeanoT = Zero | Succ PeanoT
In the first treatment, we define a type PeanoT. This is the type you would
use in function signatures, etc. At the term / values level, we can
construct values of type PeanoT through either the 'Zero' or 'Succ' data
constructors.
The second treatment encodes the Peano numbers at the type level, not value
level - note that both lines are type constructors (both lacking
corresponding data constructors):
data ZeroT
data SuccT a
I'm a little bit at my limit of type level programming in haskell, so I'm
not 100% sure about this, but in the second treatment, without any data
constructors, I don't think there is any way to actually construct a
run-time value with either of these types. You can only use them at the
type level.
Back to the analogy: In the first treatment, we can construct values of
type PeanoT through either `Zero :: PeanoT` or `Succ :: PeanoT -> PeanoT`,
data constructors of the given type. In the second treatment, we have two
types. But similar to how we have to provide a value of type PeanoT to Succ
to create the final PeanoT type, we have to provide a *type* to SuccT to
get a concrete type.
Now while there are a great many types, I believe at the kind level we only
really care if we have a concrete type ('ZeroT, of kind *), or a type
constructor that needs to be applied to concrete type to actually construct
the type (kind * -> *). For example,
data K3T a b
has kind * -> * -> * (you have to provide two concrete types for 'a' and
'b' to get out a concrete type).
I don't have any good references for formal type theory stuff, but I found
https://haskellbook.com/ to be the resource that got me over the various
failed attempts at learning haskell. It stops a bit short of type level
programming, but does a good job distinguishing between data constructors
and type constructors, and makes the analogy for how kinds arise when you
take that 'one level up'. Also its not free.
On Fri, Mar 12, 2021 at 11:18 PM Galaxy Being <borg...@gmail.com> wrote:
> I found this interesting page <https://wiki.haskell.org/Peano_numbers> at
> Wiki Haskell. Confusing, however, is how it first establishes
>
> data Peano = Zero | Succ Peano
>
> It says
>
> Here Zero and Succ are values (constructors). Zero has type Peano,
> and Succ has type Peano -> Peano.
>
> but then it breaks down each member further a few lines later
>
> data Zero
> data Succ a
>
> and then says
>
> Zero has kind *, and Succ has kind * -> *. The natural numbers are
> represented by types (of kind *) Zero, Succ Zero, Succ (Succ Zero) etc.
>
> Why is it giving two separate treatments and what is meant by the * and *
> -> * ? There's something fundamental I'm missing.
>
> If anyone knows of a really thorough and definitive *and *understandable
> treatment of Haskell types, I'd appreciate it.
>
> LB
> _______________________________________________
> Beginners mailing list
> Beginners@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20210312/89cd8add/attachment.html>
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 152, Issue 5
*****************************************
