It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 494
- ACT Study Group 5
- Azimuth Math Review 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 1
- Strategy 110
- Azimuth Project 1.1K

Options

*Dissecting a Haskell type and its data constructors.*

Note: Talk 1.* is a series of mini-talks which is leading towards the concept of functors in Haskell.

```
data Identity a = MkId a
```

"MkId 45" is a *value*, thought of as an "isomorphic copy" of 45. Think of this simply as a formal term. Using pattern matching, the term can be deconstructed, to extract the stored value, 45.

"MkId int" is a *data constructor*. (aka a value constructor.) This is a function, plain and simple, that maps the integer x to the value "MkId x".

"MkId a" is a polymorphic data constructor, with respect to the type variable a. Think of this as the function which maps each Haskell type a to the data constructor "MkId a". In other words, it is a family of per-type data constructors, parameterized by the type variable a.

Let's digress to another type constructor:

```
data Citrus = Lemon | Lime | Orange
```

Lemon is a data constructor that takes zero arguments. So it stands for a constant value. Similarly for Lime and Orange.

Citrus is a freshly defined type, which is defined by three data constructors. The only way to create a value of type Citrus is through one of its data constructors. The type itself can be thought of as being equal to the set of all values of that type.

(This is the *meaning* behind the statement that Citrus is an enumeration consisting of the constants Lemon, Lime and Orange.)

Now suppose we had:

```
SillyIdentity a = MkId a | OtherConstructor a
```

Now this polymorphic "type SillyIdentity a" is given by two polymorphic data constructors, "MkId a", and "OtherConstructor a".

"SillyIdentity int" is a particular type, which consists of all values of the form "MkId x" or "OtherConstructor x", for integers.

Recall that these values are thought of as formal terms, which can be deconstructed to obtain both the constructor type (MkId/OtherConstructor), and the value encapsulated in the term.

This means that all values are tagged with their constructor information. So, just by looking at a value, we can always reconstruct exactly how it was constructed.

Now let's return to the object at hand:

```
data Identity a = MkId a
```

By now it's pretty clear what "Identity int" means. For this type, there just happens to be a single data constructor.

"Identity int" is a specific type.

"Identity a" is a *polymorphic data type*, with respect to the type variable "a". It's a family of specific types, parameterized by "a".

Abstracting, we can can say that "Identity" means the function which maps each type "a" to the type "Identity a."

"Identity" is a *polymorphic type constructor.*

There's more to the story than that, however, as "Identity" operates not just on the types in Haskell, but also on the functions that go between types. But this is a story for another day, we will talk about how "Identity" works as a *functor*.

<END-TALK/OPEN-DISCUSSION>

hello world×