Type * and * -> * - Beginners - Haskell.org

newer
Product/tuple type vs. ...

Type * and * -> *

older
Recursion with a self-defined type

Galaxy Being

13 Mar 2021 13 Mar '21

1:18 a.m.

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

Attachments:

attachment.html (text/html — 1.7 KB)

Reply

Sign in to reply online Use email software

Show replies by date

Bob Ippolito

13 Mar 13 Mar

1:52 a.m.

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

Reply

Sign in to reply online Use email software

Matthew Low

2:58 a.m.

Thanks for the book recommendation! On Fri, Mar 12, 2021 at 11:52 PM Bob Ippolito 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 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

Reply

Sign in to reply online Use email software

Matthew Low

1:53 a.m.

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

Reply

Sign in to reply online Use email software

Erik Dominikus

14 Mar 14 Mar

6:41 a.m.

There's something fundamental I'm missing.

It is not necessarily true, but useful, to think that: - A *type is* a set of values. - A *kind* as a set of types. - The *kind* * is the set of all types. - The *kind* * -> * is the set of every function with domain * and codomain *. - The *type* T -> U is the set of every function with domain T and codomain U, if each of T and U is a type (a set of values). For example: - The type *Bool* is the set {False, True}. - The type *Maybe Bool* is the set {Nothing, Just False, Just True}. - *Maybe* is a function such that Maybe(T) = { Nothing } union { Just t | t in T }. - *Maybe* is not a type; *Maybe Bool* is a type. - *a -> a* is the set { \ x -> x }. Currying and application can happen at both the value level and the type level: - The kind of *Either* is ** -> * -> **. - The kind of *Either a* is ** -> **, if the kind of *a* is ***. - The kind of *Either a b* is ***, if the kind of *a* is *** and the kind of *b* is ***. - The type of *Just* is *a -> Maybe a*. - The type of *Just x* is *Maybe a*, if the type of *x* is *a*.

Why is it giving two separate treatments?

If anyone knows of a really thorough and definitive *and *understandable

It is to show the various ways one *can* implement/represent/realize/concretize/encode/model a mathematical construction in Haskell. You *can* (do type-level programming in Haskell, use all features of C++, eat spaghetti with a straw, etc.), but the real question has always been: *should* you? treatment of Haskell types, I'd appreciate it. If you mean Haskell 98, then the Haskell 98 Report [1] (especially Chapter 4) seems "thorough and definitive", but I don't know whether you will find it "understandable". If you mean the latest Haskell as implemented by GHC, I don't know. [1] https://www.haskell.org/onlinereport/

Reply

Sign in to reply online Use email software

Galaxy Being

16 Mar 16 Mar

3:12 p.m.

This is great stuff. I thank everybody. On Sun, Mar 14, 2021 at 5:42 AM Erik Dominikus wrote:

...
There's something fundamental I'm missing.

It is not necessarily true, but useful, to think that:

- A *type is* a set of values. - A *kind* as a set of types. - The *kind* * is the set of all types. - The *kind* * -> * is the set of every function with domain * and codomain *. - The *type* T -> U is the set of every function with domain T and codomain U, if each of T and U is a type (a set of values).

For example:

- The type *Bool* is the set {False, True}. - The type *Maybe Bool* is the set {Nothing, Just False, Just True}. - *Maybe* is a function such that Maybe(T) = { Nothing } union { Just t | t in T }. - *Maybe* is not a type; *Maybe Bool* is a type. - *a -> a* is the set { \ x -> x }.

Currying and application can happen at both the value level and the type level:

- The kind of *Either* is ** -> * -> **. - The kind of *Either a* is ** -> **, if the kind of *a* is ***. - The kind of *Either a b* is ***, if the kind of *a* is *** and the kind of *b* is ***. - The type of *Just* is *a -> Maybe a*. - The type of *Just x* is *Maybe a*, if the type of *x* is *a*.

...
Why is it giving two separate treatments?

It is to show the various ways one *can* implement/represent/realize/concretize/encode/model a mathematical construction in Haskell.

You *can* (do type-level programming in Haskell, use all features of C++, eat spaghetti with a straw, etc.), but the real question has always been: *should* you?

...
If anyone knows of a really thorough and definitive *and *understandable treatment of Haskell types, I'd appreciate it.

If you mean Haskell 98, then the Haskell 98 Report [1] (especially Chapter 4) seems "thorough and definitive", but I don't know whether you will find it "understandable".

If you mean the latest Haskell as implemented by GHC, I don't know.

[1] https://www.haskell.org/onlinereport/ _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Reply

Sign in to reply online Use email software

1526

Age (days ago)

1529

Last active (days ago)

Download

5 comments

4 participants

tags

participants (4)

Bob Ippolito
Erik Dominikus
Galaxy Being
Matthew Low