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. Re: Type * and * -> * (Matthew Low)
----------------------------------------------------------------------
Message: 1
Date: Sat, 13 Mar 2021 00:58:21 -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=gtkxyfx4zmcq7r1f4asmkkm4t5zz_ur9ubkfloit-vvd...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
Thanks for the book recommendation!
On Fri, Mar 12, 2021 at 11:52 PM Bob Ippolito <b...@redivi.com> wrote:
> 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
>>
> _______________________________________________
> 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/20210313/acd43640/attachment-0001.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 6
*****************************************
