5 ms·

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

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.

lifthrasiir 5y ago
It is equivalent to the following: type 'a list = Cons of 'a * 'a list | Tail ...but with a fancy syntax for Cons and Tail.
- cassepipe 5y ago
  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 ?
  - kripke 5y ago
    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, []))))`.
maweki 5y ago
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 []
- cassepipe 5y ago
  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 ?
  - willmorrison 5y ago
    Here is the Wikipedia page: https://en.m.wikipedia.org/wiki/Cons https://en.m.wikipedia.org/wiki/Cons
  - gpderetta 5y ago
    Cons comes from Lisp: https://en.wikipedia.org/wiki/Cons 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).
  - maweki 5y ago
    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,[])))
bmitc 5y ago
`|` 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 `[]`.
dan-robertson 5y ago
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.
- cassepipe 5y ago
  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 ?
  - dan-robertson 5y ago
    I think that is made up syntax from the article but maybe I’m wrong.
  - yawaramin 5y ago
    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.

lifthrasiir 5y ago

It is equivalent to the following: type 'a list = Cons of 'a * 'a list | Tail ...but with a fancy syntax for Cons and Tail.

cassepipe 5y ago
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 ?
- kripke 5y ago
  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, []))))`.

maweki 5y ago

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

cassepipe 5y ago
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 ?
- willmorrison 5y ago
  Here is the Wikipedia page: https://en.m.wikipedia.org/wiki/Cons https://en.m.wikipedia.org/wiki/Cons
- gpderetta 5y ago
  Cons comes from Lisp: https://en.wikipedia.org/wiki/Cons 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).
- maweki 5y ago
  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,[])))

bmitc 5y ago

`|` 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 `[]`.

dan-robertson 5y ago

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.

cassepipe 5y ago
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 ?
- dan-robertson 5y ago
  I think that is made up syntax from the article but maybe I’m wrong.
- yawaramin 5y ago
  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.