Hacker News Reader

Comment by cassepipe | Hacker News Reader

Could someone please explain ? : type 'a list = 'a :: 'a list | []

The article says "::" is a Data Constructor. I can make sense of type 'a = Left of 'a | Right of 'a where Right and Left are the Data constructors but I don't see the link with the part I don't understand.

View on HN

The definition of list is:

  type 'a list = [] | (::) of 'a * 'a list

When you write a list like:

  [x; y; z]

This is syntactic sugar for:

  x::y::z::[]

Which is syntactic sugar for:

  (::) (x, (::) (y, (::) (z, [])))

One can imagine using more ordinary constructor names instead:

  type 'a list = Nil | Cons of 'a * 'a list

And then the above would be:

  Cons (x, Cons (y, Cons (z, Nil)))

In OCaml, data constructor names mar be either a capital letter followed by set or more capital/lower letters/underscores/apostrophes/digits, or one of the following:

  []
  ()
  true
  false
  (::)

Type directed constructor disambiguating means you can do funky things like:

  type 'a nonempty = (::) of 'a * 'a list

And write such a value just like you would a normal list.

Thanks for the detailed explanation. One more question though, when I write

    type 'a = 'a :: list 'a

It is syntactic sugar that allows me to get the * product type for free, right ?

I think that is made up syntax from the article but maybe I’m wrong.

That's actually invalid syntax. '::' can't be used infix in a type declaration. And type application is in reverse. So it's not list 'a but 'a list.

A list is either the empty list [] or

Two pieces of data (with the constructor ::) with 1 being the head of the list (type 'a) and one being the tail of the list (type 'a list, a recursive definition).

:: is an allowed identifier in oCaml. If that is not allowed, the typical names are Cons for :: and Nil for []

Thanks. I had not understood it could be recursive.

Do you know Cons' meaning ?

Also why does :: act as a separator... ? Is that something you ca do with any Data constructor, I mean can I write type 'a = 'a Cons of 'a | Nil of 'a ?

Here is the Wikipedia page: https://en.m.wikipedia.org/wiki/Cons

Cons comes from Lisp: https://en.wikipedia.org/wiki/Cons . In practice a cons cell is a list node represented as a pair of pointers, one pointing to the contained element, the other to the next node (or null, or another element for degenerate lists).

You would write something like List a = Cons a (List a) | Nil

As :: doesn't start with a letter, it's infix by default. But basically a binary constructor. If you want to create the List [1,2,3] in the prefix notation you might be used to: ::(1,::(2,::(3,[])))

It is equivalent to the following:

  type 'a list = Cons of 'a * 'a list | Tail

...but with a fancy syntax for Cons and Tail.

Ok. So in your example the construction action (placing two things next to each other IIUC) is done by the * product type Operator and Cons has no special meaning whereas if I had used ::, I actually get an the (::) name to refer to the left hand of the union and the construction action. Did I get that right ?

Sort of, I think?

`type 'a t = Cons of 'a * 'a t | Tail` is defining a type with a constructor `Cons` with two arguments and a constructor `Tail` with zero argument. You write values of type `'a t` as `Cons (a, b)` and `Tail`.

`type 'a u = (::) of 'a * 'a u | []` is defining a type with a constructor `(::)` with two arguments and a constructor `[]` with zero argument. You build values of type `'a u` as `(::) (a, b)` and `[]`.

The rest comes from the special syntax support in OCaml for the `(::)` and `[]` names. Namely, `a :: b` is parsed as `(::) (a, b)`, and `[a; b; ...; z]` is parsed as `a :: b :: ... :: z :: []`, and hence as `(::) (a, (::) (b, (::) (..., (::) (z, []))))`.

`|` is read as "or". `::` is syntax for what Lisp and Scheme call `cons`, which places an element onto either a list or the empty list, `[]`. The syntax `'a` is a type variable, which means that `'a` can be any type but it must all be the same type everywhere `'a` appears.

So this type definition means that `'a list` is a list of elements of type `'a`, and it's defined by being something of type `'a` consed onto either another list of type `'a` OR the empty list, represented by `[]`.

Reply on news.ycombinator.com